diff --git a/src/haz3lcore/dynamics/Stepper.re b/src/haz3lcore/dynamics/Stepper.re index 00b4312412..8705caa9bc 100644 --- a/src/haz3lcore/dynamics/Stepper.re +++ b/src/haz3lcore/dynamics/Stepper.re @@ -14,7 +14,10 @@ type stepper_state = | StepTimeout(EvalObj.t); [@deriving (show({with_path: false}), sexp, yojson)] -type history = Aba.t((DHExp.t, Editor.t, EvaluatorState.t), step); +type a = (CachedStatics.statics, Editor.t, EvaluatorState.t); + +[@deriving (show({with_path: false}), sexp, yojson)] +type history = Aba.t(a, step); [@deriving (show({with_path: false}), sexp, yojson)] type t = { @@ -196,8 +199,8 @@ let should_hide_step = (~settings, x: step): (FilterAction.action, step) => }; let get_elab = ({history, _}: t): Elaborator.Elaboration.t => { - let (d, _, _) = Aba.last_a(history); - {d: d}; + let (cs: CachedStatics.statics, _, _) = Aba.last_a(history); + {d: cs.term}; }; let get_next_steps = s => s.next_options; @@ -212,12 +215,14 @@ let step_pending = (idx: int, stepper: t) => { {...stepper, stepper_state: StepPending(idx)}; }; -let rec evaluate_pending = (~settings, s: t) => { +let rec evaluate_pending = (~settings: CoreSettings.t, s: t) => { switch (s.stepper_state) { | StepperDone | StepTimeout(_) => s | StepperReady => - let next' = s.next_options |> List.map(should_hide_eval_obj(~settings)); + let next' = + s.next_options + |> List.map(should_hide_eval_obj(~settings=settings.evaluation)); let next'' = List.mapi((i, x) => (i, x), next'); switch ( List.find_opt(((_, (act, _))) => act == FilterAction.Eval, next'') @@ -228,7 +233,7 @@ let rec evaluate_pending = (~settings, s: t) => { }; | StepPending(i) => let eo = List.nth(s.next_options, i); - let (d, _, state) = Aba.hd(s.history); + let ({term: d, _}: CachedStatics.statics, _, state) = Aba.hd(s.history); let state_ref = ref(state); let d_loc' = ( @@ -250,8 +255,9 @@ let rec evaluate_pending = (~settings, s: t) => { }; let new_state = state_ref^; let editor = ExpToSegment.exp_to_editor(~inline=false, d'); + let statics = CachedStatics.statics_of_term(~settings, d', editor); { - history: s.history |> Aba.cons((d', editor, new_state), new_step), + history: s.history |> Aba.cons((statics, editor, new_state), new_step), stepper_state: StepperReady, next_options: decompose(d', new_state), } @@ -273,8 +279,9 @@ let rec evaluate_full = (~settings, s: t) => { let init = ({d}: Elaborator.Elaboration.t, ~settings) => { let state = EvaluatorState.init; let editor = ExpToSegment.exp_to_editor(~inline=false, d); + let statics = CachedStatics.statics_of_term(~settings, d, editor); { - history: Aba.singleton((d, editor, state)), + history: Aba.singleton((statics, editor, state)), next_options: decompose(d, state), stepper_state: StepperReady, } @@ -304,8 +311,8 @@ let step_backward = (~settings, s: t) => { { history: h', next_options: { - let (d, _, st) = Aba.hd(h'); - decompose(d, st); + let (cs, _, st) = Aba.hd(h'); + decompose(cs.term, st); }, stepper_state: StepperDone, }; @@ -356,8 +363,7 @@ let get_justification: step_kind => string = | UnOp(Meta(Unquote)) => failwith("INVALID STEP"); type step_info = { - hidden_history: - Aba.t((DHExp.t, Editor.t, EvaluatorState.t), (step, Id.t)), + hidden_history: Aba.t(a, (step, Id.t)), chosen_step: option(step), // The step that was taken next previous_step: option((step, Id.t)) // The step that will be displayed above this one (an Id in included because it may have changed since the step was taken) }; @@ -448,30 +454,33 @@ let (sexp_of_persistent, persistent_of_sexp) = ); let to_persistent_history = history => - Aba.map_a(((d, _, s)) => (d, s), history); + Aba.map_a((({term: d, _}, _, s): a) => (d, s), history); // Remove EvalObj.t objects from stepper to prevent problems when loading let to_persistent: t => persistent = ({history, _}) => {persistent_history: history |> to_persistent_history}; -let from_persistent_history = history => +let from_persistent_history = (~settings, history) => Aba.map_a( - ((d, s)) => (d, ExpToSegment.exp_to_editor(d, ~inline=false), s), + ((d, s)) => { + let editor = ExpToSegment.exp_to_editor(d, ~inline=false); + let statics = CachedStatics.statics_of_term(~settings, d, editor); + (statics, editor, s); + }, history, ); -let from_persistent: persistent => t = - ({persistent_history}) => { - let history = persistent_history |> from_persistent_history; - { - history, - next_options: { - let (d, _, state) = Aba.hd(history); - decompose(d, state); - }, - stepper_state: StepperDone, - }; +let from_persistent = (~settings, {persistent_history}) => { + let history = persistent_history |> from_persistent_history(~settings); + { + history, + next_options: { + let ({term: d, _}: CachedStatics.statics, _, state) = Aba.hd(history); + decompose(d, state); + }, + stepper_state: StepperDone, }; +}; type selection = int; diff --git a/src/haz3lcore/prog/CachedStatics.re b/src/haz3lcore/prog/CachedStatics.re index ba277463ea..92e2b429af 100644 --- a/src/haz3lcore/prog/CachedStatics.re +++ b/src/haz3lcore/prog/CachedStatics.re @@ -7,6 +7,14 @@ type statics = { error_ids: list(Id.t), }; +let statics_of_term = (~settings, term: UExp.t, editor: Editor.t): statics => { + let info_map = + Interface.Statics.mk_map_ctx(settings, Builtins.ctx_init, term); + let error_ids = + Statics.Map.error_ids(editor.state.meta.term_ranges, info_map); + {term, info_map, error_ids}; +}; + let empty_statics: statics = { term: UExp.{ids: [Id.invalid], copied: false, term: Tuple([])}, info_map: Id.Map.empty, diff --git a/src/haz3lcore/prog/ModelResult.re b/src/haz3lcore/prog/ModelResult.re index f2387ba583..b253f02ab6 100644 --- a/src/haz3lcore/prog/ModelResult.re +++ b/src/haz3lcore/prog/ModelResult.re @@ -49,8 +49,7 @@ let run_pending = (~settings: CoreSettings.t) => evaluation: Interface.evaluate(~settings, elab.d), }) | Evaluation(_) as e => e - | Stepper(s) => - Stepper(Stepper.evaluate_pending(~settings=settings.evaluation, s)); + | Stepper(s) => Stepper(Stepper.evaluate_pending(~settings, s)); let update_evaluation = ( @@ -134,10 +133,10 @@ let to_persistent: t => persistent = | Evaluation(_) => Evaluation | Stepper(s) => Stepper(Stepper.to_persistent(s)); -let of_persistent: persistent => t = +let of_persistent = (~settings) => fun | Evaluation => NoElab - | Stepper(s) => Stepper(Stepper.from_persistent(s)); + | Stepper(s) => Stepper(Stepper.from_persistent(~settings, s)); [@deriving (show({with_path: false}), sexp, yojson)] type selection = int; @@ -167,3 +166,25 @@ let put_selected_editor = (~selection: selection, mr: t, editor) => | Evaluation(_) => mr | Stepper(s) => Stepper(Stepper.put_selected_editor(~selection, s, editor)) }; + +let get_elaboration = mr => + switch (mr) { + | NoElab => None + | Evaluation({elab, _}) => Some(elab) + | Stepper(s) => Some(Stepper.get_elab(s)) + }; + +let perform = (~settings, idx, action, mr) => { + get_selected_editor(~selection=idx, mr) + |> Option.map(editor => + editor + |> Perform.go(~settings, action) + |> ( + fun + | Ok(editor) => editor + | Error(e) => raise(Action.Failure.Exception(e)) + ) + |> put_selected_editor(~selection=idx, mr) + ) + |> Option.value(~default=mr); +}; diff --git a/src/haz3lcore/statics/Statics.re b/src/haz3lcore/statics/Statics.re index 1cd72a6304..a71696696c 100644 --- a/src/haz3lcore/statics/Statics.re +++ b/src/haz3lcore/statics/Statics.re @@ -229,10 +229,10 @@ and uexp_to_info_map = let go_pat = upat_to_info_map(~ctx, ~ancestors); let atomic = self => add(~self, ~co_ctx=CoCtx.empty, m); switch (term) { - | Closure(_) => - failwith( - "TODO: implement closure type checking - see how dynamic type assignment does it", - ) + | Closure(_, e) => + // TODO: implement closure type checking properly - see how dynamic type assignment does it + let (e, m) = go(~mode, e, m); + add(~self=Just(e.ty), ~co_ctx=e.co_ctx, m); | MultiHole(tms) => let (co_ctxs, m) = multi(~ctx, ~ancestors, m, tms); add(~self=IsMulti, ~co_ctx=CoCtx.union(co_ctxs), m); diff --git a/src/haz3lcore/zipper/action/Action.re b/src/haz3lcore/zipper/action/Action.re index ca95a2031c..078b8697ee 100644 --- a/src/haz3lcore/zipper/action/Action.re +++ b/src/haz3lcore/zipper/action/Action.re @@ -71,6 +71,8 @@ module Failure = { | Cant_paste | Cant_undo | Cant_redo; + + exception Exception(t); }; module Result = { diff --git a/src/haz3lcore/zipper/action/Perform.re b/src/haz3lcore/zipper/action/Perform.re index 5a471105f4..68a0c1896a 100644 --- a/src/haz3lcore/zipper/action/Perform.re +++ b/src/haz3lcore/zipper/action/Perform.re @@ -208,23 +208,6 @@ let rec go_z = }; }; -// let paste_into_zip = (z: Zipper.t, str: string): option(Zipper.t) => { -// /* HACK(andrew): These two perform calls are a hack to -// deal with the fact that pasting something like "let a = b in" -// won't trigger the barfing of the "in"; to trigger this, we -// insert a space, and then we immediately delete it. */ -// let settings = CoreSettings.off; -// let* z = zipper_of_string(~zipper_init=z, str); -// switch (Perform.go_z(~settings, Insert(" "), z)) { -// | Error(_) => None -// | Ok(z) => -// switch (Perform.go_z(~settings, Destruct(Left), z)) { -// | Error(_) => None -// | Ok(z) => Some(z) -// } -// }; -// }; - let go = (~settings: CoreSettings.t, a: Action.t, ed: Editor.t) : Action.Result.t(Editor.t) => diff --git a/src/haz3lweb/Export.re b/src/haz3lweb/Export.re index 7bc711cc34..2fb01d2d85 100644 --- a/src/haz3lweb/Export.re +++ b/src/haz3lweb/Export.re @@ -22,8 +22,9 @@ type all_f22 = { let mk_all = (~instructor_mode, ~log) => { let settings = Store.Settings.export(); let explainThisModel = Store.ExplainThisModel.export(); - let scratch = Store.Scratch.export(); - let documentation = Store.Documentation.export(); + let scratch = Store.Scratch.export(~settings=Haz3lcore.CoreSettings.off); + let documentation = + Store.Documentation.export(~settings=Haz3lcore.CoreSettings.off); let exercise = Store.Exercise.export( ~specs=ExerciseSettings.exercises, @@ -53,7 +54,7 @@ let import_all = (data, ~specs) => { let settings = Store.Settings.import(all.settings); Store.ExplainThisModel.import(all.explainThisModel); let instructor_mode = settings.instructor_mode; - Store.Scratch.import(all.scratch); + Store.Scratch.import(~settings=settings.core, all.scratch); Store.Exercise.import(all.exercise, ~specs, ~instructor_mode); Log.import(all.log); }; diff --git a/src/haz3lweb/Model.re b/src/haz3lweb/Model.re index 058c4ae7b6..e4557589fb 100644 --- a/src/haz3lweb/Model.re +++ b/src/haz3lweb/Model.re @@ -57,21 +57,20 @@ let mk = (editors, results, statics) => { let blank = mk(Editors.Scratch(0, []), ModelResults.empty, CachedStatics.empty); -let load_editors = - (~mode: Settings.mode, ~instructor_mode: bool) - : (Editors.t, ModelResults.t) => - switch (mode) { +let load_editors = (~settings: Settings.t): (Editors.t, ModelResults.t) => + switch (settings.mode) { | Scratch => - let (idx, slides, results) = Store.Scratch.load(); + let (idx, slides, results) = Store.Scratch.load(~settings=settings.core); (Scratch(idx, slides), results); | Documentation => - let (name, slides, results) = Store.Documentation.load(); + let (name, slides, results) = + Store.Documentation.load(~settings=settings.core); (Documentation(name, slides), results); | Exercises => let (n, specs, exercise) = Store.Exercise.load( ~specs=ExerciseSettings.exercises, - ~instructor_mode, + ~instructor_mode=settings.instructor_mode, ); (Exercises(n, specs, exercise), ModelResults.empty); }; @@ -90,11 +89,7 @@ let save_editors = let load = (init_model: t): t => { let settings = Store.Settings.load(); let explainThisModel = Store.ExplainThisModel.load(); - let (editors, results) = - load_editors( - ~mode=settings.mode, - ~instructor_mode=settings.instructor_mode, - ); + let (editors, results) = load_editors(~settings); let ui_state = init_model.ui_state; let statics = Editors.mk_statics(~settings, editors); {editors, settings, results, statics, explainThisModel, ui_state}; @@ -114,10 +109,10 @@ let reset = (model: t): t => { /* Reset model to default, including in localstorage, but don't otherwise erase localstorage, allowing e.g. api keys to persist */ - ignore(Store.Settings.init()); + let settings = Store.Settings.init().core; ignore(Store.ExplainThisModel.init()); - ignore(Store.Scratch.init()); - ignore(Store.Documentation.init()); + ignore(Store.Scratch.init(~settings)); + ignore(Store.Documentation.init(~settings)); ignore(Store.Exercise.init(~instructor_mode=true)); let new_model = load(blank); { diff --git a/src/haz3lweb/Store.re b/src/haz3lweb/Store.re index 8156dd975d..0c4ac3fe23 100644 --- a/src/haz3lweb/Store.re +++ b/src/haz3lweb/Store.re @@ -121,14 +121,14 @@ module Scratch = { |> ModelResults.bindings, ); - let of_persistent = ((idx, slides, results): persistent) => { + let of_persistent = (~settings, (idx, slides, results): persistent) => { ( idx, List.map(ScratchSlide.unpersist, slides), results |> List.to_seq |> ModelResults.of_seq - |> ModelResults.map(ModelResult.of_persistent), + |> ModelResults.map(ModelResult.of_persistent(~settings)), ); }; @@ -144,23 +144,23 @@ module Scratch = { JsUtil.set_localstore(save_scratch_key, serialize(scratch)); }; - let init = () => { - let scratch = of_persistent(Init.startup.scratch); + let init = (~settings) => { + let scratch = of_persistent(~settings, Init.startup.scratch); save(scratch); scratch; }; - let load = () => + let load = (~settings) => switch (JsUtil.get_localstore(save_scratch_key)) { - | None => init() + | None => init(~settings) | Some(data) => - try(deserialize(data)) { - | _ => init() + try(deserialize(~settings, data)) { + | _ => init(~settings) } }; - let export = () => serialize(load()); - let import = data => save(deserialize(data)); + let export = (~settings) => serialize(load(~settings)); + let import = (~settings, data) => save(deserialize(~settings, data)); }; module Documentation = { @@ -186,14 +186,14 @@ module Documentation = { |> ModelResults.bindings, ); - let of_persistent = ((string, slides, results): persistent) => { + let of_persistent = (~settings, (string, slides, results): persistent) => { ( string, List.map(unpersist, slides), results |> List.to_seq |> ModelResults.of_seq - |> ModelResults.map(ModelResult.of_persistent), + |> ModelResults.map(ModelResult.of_persistent(~settings)), ); }; @@ -209,23 +209,23 @@ module Documentation = { JsUtil.set_localstore(save_documentation_key, serialize(slides)); }; - let init = () => { - let documentation = of_persistent(Init.startup.documentation); + let init = (~settings) => { + let documentation = of_persistent(~settings, Init.startup.documentation); save(documentation); documentation; }; - let load = () => + let load = (~settings) => switch (JsUtil.get_localstore(save_documentation_key)) { - | None => init() + | None => init(~settings) | Some(data) => - try(deserialize(data)) { - | _ => init() + try(deserialize(~settings, data)) { + | _ => init(~settings) } }; - let export = () => serialize(load()); - let import = data => save(deserialize(data)); + let export = (~settings) => serialize(load(~settings)); + let import = (~settings, data) => save(deserialize(~settings, data)); }; module Exercise = { diff --git a/src/haz3lweb/Update.re b/src/haz3lweb/Update.re index f2fe1739a6..dbeb8b65bd 100644 --- a/src/haz3lweb/Update.re +++ b/src/haz3lweb/Update.re @@ -212,10 +212,7 @@ let schedule_evaluation = (~schedule_action, model: Model.t): unit => /* Not sending stepper to worker for now bc closure perf */ let new_rs = model.results - |> ModelResults.update_elabs( - ~settings=model.settings.core.evaluation, - elabs, - ); + |> ModelResults.update_elabs(~settings=model.settings.core, elabs); let step_rs = ModelResults.to_step(new_rs); if (!ModelResults.is_empty(step_rs)) { let new_rs = @@ -303,8 +300,11 @@ let switch_scratch_slide = let export_persistent_data = () => { let data: PersistentData.t = { documentation: - Store.Documentation.load() |> Store.Documentation.to_persistent, - scratch: Store.Scratch.load() |> Store.Scratch.to_persistent, + Store.Documentation.load(~settings=CoreSettings.off) + |> Store.Documentation.to_persistent, + scratch: + Store.Scratch.load(~settings=CoreSettings.off) + |> Store.Scratch.to_persistent, settings: Store.Settings.load(), }; let contents = @@ -524,18 +524,6 @@ let rec apply = model.results |> ModelResults.find(key) |> ModelResult.step_forward(idx); - let _ = print_endline("Ouch"); - let _ = - print_endline( - Stepper.show_stepper_state( - ( - fun - | (Stepper(s): ModelResult.t) => s - | _ => failwith("") - )(r). - stepper_state, - ), - ); Ok({...model, results: model.results |> ModelResults.add(key, r)}); | StepperAction(key, StepBackward) => let r = @@ -553,9 +541,7 @@ let rec apply = Some( v |> Option.value(~default=NoElab: ModelResult.t) - |> ModelResult.toggle_stepper( - ~settings=model.settings.core.evaluation, - ), + |> ModelResult.toggle_stepper(~settings=model.settings.core), ) ), }) diff --git a/src/haz3lweb/view/Cell.re b/src/haz3lweb/view/Cell.re deleted file mode 100644 index 44abf92f13..0000000000 --- a/src/haz3lweb/view/Cell.re +++ /dev/null @@ -1,540 +0,0 @@ -open Haz3lcore; -open Virtual_dom.Vdom; -open Node; -open Util; - -let narrative_cell = (content: Node.t) => - div( - ~attr=Attr.class_("cell"), - [div(~attr=Attr.class_("cell-chapter"), [content])], - ); - -let simple_cell_item = (content: list(Node.t)) => - div(~attr=Attr.classes(["cell-item"]), content); - -let caption = (~rest: option(string)=?, bolded: string) => - div( - ~attr=Attr.many([Attr.classes(["cell-caption"])]), - [strong([text(bolded)])] @ (rest |> Option.map(text) |> Option.to_list), - ); - -let simple_cell_view = (items: list(t)) => - div(~attr=Attr.class_("cell"), items); - -let error_msg = (err: ProgramResult.error) => - switch (err) { - | EvaulatorError(err) => EvaluatorError.show(err) - | UnknownException(str) => str - | Timeout => "Evaluation timed out" - }; - -let status_of: ProgramResult.t => string = - fun - | ResultPending => "pending" - | ResultOk(_) => "ok" - | ResultFail(_) => "fail" - | Off(_) => "off"; - -let live_eval = - ( - ~select: Editors.Selection.cell => Ui_effect.t(unit), - ~inject: UpdateAction.t => Ui_effect.t(unit), - ~ui_state, - ~result_key: string, - ~settings: Settings.t, - ~selected, - ~locked, - result: ModelResult.eval_result, - ) => { - let editor = - switch (result.evaluation, result.previous) { - | (ResultOk(res), _) => res.editor - | (ResultPending, ResultOk(res)) => res.editor - | _ => result.elab.d |> ExpToSegment.exp_to_editor(~inline=false) - }; - let inject': CodeEditor.event => Ui_effect.t(unit) = - fun - | MouseUp => SetMeta(Mouseup) |> inject - | DragTo(point) => - PerformAction(Select(Resize(Goal(Point(point))))) |> inject - | MouseDown(point) => - Effect.Many([ - inject(SetMeta(Mousedown)), - select(Result(0)), - inject(PerformAction(Move(Goal(Point(point))))), - ]) - | JumpToBindingSiteOf(point) => - Effect.Many([ - inject(PerformAction(Move(Goal(Point(point))))), - select(Result(0)), - inject(PerformAction(Jump(BindingSiteOfIndicatedVar))), - ]) - | DoubleClick => PerformAction(Select(Tile(Current))) |> inject - | TripleClick => PerformAction(Select(Smart)) |> inject - | StepSelected(_) => Ui_effect.Ignore; - let code_view = - CodeEditor.view( - ~select=() => select(Result(0)), - ~inject=inject', - ~ui_state, - ~settings, - ~selected, - ~locked, - ~test_results=None, - ~highlights=None, - ~error_ids=[], - ~overlayer=None, - ~sort=Sort.root, - ~next_steps=[], - editor, - ); - let exn_view = - switch (result.evaluation) { - | ResultFail(err) => [ - div(~attr=Attr.classes(["error-msg"]), [text(error_msg(err))]), - ] - | _ => [] - }; - Node.( - div( - ~attr=Attr.classes(["cell-item", "cell-result"]), - exn_view - @ [ - div( - ~attr=Attr.classes(["status", status_of(result.evaluation)]), - [ - div(~attr=Attr.classes(["spinner"]), []), - div(~attr=Attr.classes(["eq"]), [text("≡")]), - ], - ), - div( - ~attr=Attr.classes(["result", status_of(result.evaluation)]), - [code_view], - ), - Widgets.toggle(~tooltip="Show Stepper", "s", false, _ => - inject(UpdateAction.ToggleStepper(result_key)) - ), - ], - ) - ); -}; - -let stepper_view = - ( - ~select: Editors.Selection.cell => Ui_effect.t(unit), - ~inject: UpdateAction.stepper_action => Ui_effect.t(unit), - ~inject_global: Update.t => Ui_effect.t(unit), - ~ui_state, - ~settings, - ~read_only: bool, - ~selected: option(int), - stepper: Stepper.t, - ) => { - let step_dh_code = - ( - ~next_steps, - ~selected: bool, - ~idx: int, - {previous_step: _, hidden_history, chosen_step: _}: Stepper.step_info, - ) => { - let (_, editor, _) = Aba.hd(hidden_history); - div( - ~attr=Attr.classes(["result"]), - [ - CodeEditor.view( - ~select=() => select(Result(idx)), - ~inject= - fun - | MouseUp => SetMeta(Mouseup) |> inject_global - | DragTo(point) => - PerformAction(Select(Resize(Goal(Point(point))))) - |> inject_global - | MouseDown(point) => - Effect.Many([ - inject_global(SetMeta(Mousedown)), - select(Result(idx)), - inject_global(PerformAction(Move(Goal(Point(point))))), - ]) - | JumpToBindingSiteOf(point) => - Effect.Many([ - inject_global(PerformAction(Move(Goal(Point(point))))), - select(Result(idx)), - inject_global( - PerformAction(Jump(BindingSiteOfIndicatedVar)), - ), - ]) - | DoubleClick => - PerformAction(Select(Tile(Current))) |> inject_global - | TripleClick => PerformAction(Select(Smart)) |> inject_global - | StepSelected(i) => StepForward(i) |> inject, - ~ui_state, - ~settings, - ~selected, - ~locked=read_only, - ~test_results=None, - ~highlights=None, - ~error_ids=[], - ~overlayer=None, - ~sort=Sort.root, - ~next_steps=List.map(snd, next_steps), - editor, - ), - ], - ); - }; - let history = - Stepper.get_history(~settings=settings.core.evaluation, stepper); - switch (history) { - | [] => [] - | [hd, ..._] => - let button_back = - Widgets.button_d( - Icons.undo, - inject(StepBackward), - ~disabled= - !Stepper.can_undo(~settings=settings.core.evaluation, stepper), - ~tooltip="Step Backwards", - ); - let button_hide_stepper = - Widgets.toggle(~tooltip="Show Stepper", "s", true, _ => - inject(HideStepper) - ); - let toggle_show_history = - Widgets.toggle( - ~tooltip="Show History", - "h", - settings.core.evaluation.stepper_history, - _ => - inject_global(Set(Evaluation(ShowRecord))) - ); - let eval_settings = - Widgets.button(Icons.gear, _ => - inject_global(Set(Evaluation(ShowSettings))) - ); - let current = - div( - ~attr=Attr.classes(["cell-item", "cell-result"]), - read_only - ? [ - div(~attr=Attr.class_("equiv"), [Node.text("≡")]), - step_dh_code( - ~next_steps=[], - ~idx=0, - ~selected=selected == Some(0), - hd, - ), - ] - : [ - div(~attr=Attr.class_("equiv"), [Node.text("≡")]), - step_dh_code( - ~next_steps= - List.mapi( - (i, x: EvaluatorStep.EvalObj.t) => - (i, x.d_loc |> DHExp.rep_id), - Stepper.get_next_steps(stepper), - ), - ~idx=0, - ~selected=selected == Some(0), - hd, - ), - button_back, - eval_settings, - toggle_show_history, - button_hide_stepper, - ], - ); - let dh_code_previous = step_dh_code; - let previous_step = - (~hidden: bool, ~idx, step: Stepper.step_info): list(Node.t) => { - [ - div( - ~attr= - Attr.classes( - ["cell-item", "cell-result"] @ (hidden ? ["hidden"] : []), - ), - [ - div(~attr=Attr.class_("equiv"), [Node.text("≡")]), - dh_code_previous( - ~next_steps=[], - ~selected=Some(idx) == selected, - ~idx, - step, - ), - div( - ~attr=Attr.classes(["stepper-justification"]), - step.chosen_step - |> Option.map((chosen_step: EvaluatorStep.step) => - chosen_step.knd |> Stepper.get_justification |> Node.text - ) - |> Option.to_list, - ), - ], - ), - ]; - }; - ( - ( - settings.core.evaluation.stepper_history - ? { - let steps: list((bool, Stepper.step_info)) = - List.map( - step => - [ - (false, step), - ...settings.core.evaluation.show_hidden_steps - ? Stepper.hidden_steps_of_info(step) - |> List.map(x => (true, x)) - : [], - ], - history, - ) - |> List.flatten; - List.mapi( - (idx, (hidden, step)) => - previous_step(~hidden, ~idx=idx + 1, step), - steps |> List.rev, - ) - |> List.flatten; - } - |> List.rev - |> List.tl - |> List.rev - : [] - ) - @ [current] - ) - @ ( - settings.core.evaluation.show_settings - ? SettingsModal.view(~inject=inject_global, settings.core.evaluation) - : [] - ); - }; -}; - -let footer = - ( - ~locked, - ~select, - ~inject, - ~ui_state: Model.ui_state, - ~settings: Settings.t, - ~result: ModelResult.t, - ~selected: option(int), - ~result_key, - ) => - switch (result) { - | _ when !settings.core.dynamics => [] - | NoElab => [] - | Evaluation(result) => [ - live_eval( - ~locked, - ~select, - ~inject, - ~ui_state, - ~settings, - ~result_key, - ~selected=selected == Some(0), - result, - ), - ] - | Stepper(s) => - stepper_view( - ~select, - ~inject= - stepper_action => - inject(UpdateAction.StepperAction(result_key, stepper_action)), - ~inject_global=inject, - ~settings, - ~ui_state, - ~read_only=false, - ~selected, - s, - ) - }; - -let editor_view = - ( - ~select: Editors.Selection.cell => Ui_effect.t(unit), - ~inject, - ~ui_state: Model.ui_state, - ~settings: Settings.t, - ~selected: option(Editors.Selection.cell), - ~locked=false, - ~caption: option(Node.t)=?, - ~test_results: option(TestResults.t), - ~footer: option(list(Node.t))=?, - ~highlights: option(ColorSteps.colorMap), - ~overlayer: option(Node.t)=None, - ~error_ids: list(Id.t), - ~sort=Sort.root, - editor: Editor.t, - ) => { - let inject: CodeEditor.event => Ui_effect.t(unit) = - if (locked) { - _ => Effect.(Many([Prevent_default, Stop_propagation])); - } else { - fun - | MouseUp => inject(Update.SetMeta(Mouseup)) - | DragTo(point) => - inject(Update.PerformAction(Select(Resize(Goal(Point(point)))))) - | MouseDown(point) => - Effect.Many([ - inject(Update.SetMeta(Mousedown)), - select(Editors.Selection.MainEditor), - inject(Update.PerformAction(Move(Goal(Point(point))))), - ]) - | JumpToBindingSiteOf(point) => - Effect.Many([ - select(Editors.Selection.MainEditor), - inject(Update.PerformAction(Move(Goal(Point(point))))), - inject(Update.PerformAction(Jump(BindingSiteOfIndicatedVar))), - ]) - | DoubleClick => Update.PerformAction(Select(Tile(Current))) |> inject - | TripleClick => Update.PerformAction(Select(Smart)) |> inject - | StepSelected(_) => Ui_effect.Ignore; - }; - div( - ~attr= - Attr.classes([ - "cell", - Option.is_some(selected) ? "selected" : "deselected", - locked ? "locked" : "unlocked", - ]), - Option.to_list(caption) - @ [ - CodeEditor.view( - ~select=() => select(Editors.Selection.MainEditor), - ~inject, - ~ui_state, - ~settings, - ~selected=selected == Some(MainEditor), - ~locked, - ~test_results, - ~highlights, - ~overlayer, - ~error_ids, - ~sort, - ~next_steps=[], - editor, - ), - ] - @ (footer |> Option.to_list |> List.concat), - ); -}; - -let report_footer_view = content => { - div(~attr=Attr.classes(["cell-item", "cell-report"]), content); -}; - -let test_report_footer_view = (~inject, ~test_results: option(TestResults.t)) => { - report_footer_view([TestView.test_summary(~inject, ~test_results)]); -}; - -let panel = (~classes=[], content, ~footer: option(t)) => { - simple_cell_view( - [div(~attr=Attr.classes(["cell-item", "panel"] @ classes), content)] - @ Option.to_list(footer), - ); -}; - -let title_cell = title => { - simple_cell_view([ - div( - ~attr=Attr.class_("title-cell"), - [div(~attr=Attr.class_("title-text"), [text(title)])], - ), - ]); -}; - -/* An editor view that is not selectable or editable, - * and does not show error holes or test results. - * Used in Docs to display the header example */ -let locked_no_statics = - ( - ~select, - ~inject, - ~ui_state, - ~segment, - ~highlights, - ~settings, - ~sort, - ~expander_deco, - ) => [ - editor_view( - ~locked=true, - ~selected=None, - ~highlights, - ~select, - ~inject, - ~ui_state, - ~settings, - ~footer=[], - ~test_results=None, - ~error_ids=[], - ~overlayer=Some(expander_deco), - ~sort, - segment |> Zipper.unzip |> Editor.init(~read_only=true), - ), -]; - -/* An editor view that is not selectable or editable, - * but does show static errors, test results, and live values. - * Used in Docs for examples */ -let locked = - ( - ~ui_state, - ~settings: Settings.t, - ~select, - ~inject, - ~target_id, - ~segment: Segment.t, - ) => { - let editor = segment |> Zipper.unzip |> Editor.init(~read_only=true); - let statics = - settings.core.statics - ? ScratchSlide.mk_statics(~settings, editor, Builtins.ctx_init) - : CachedStatics.empty_statics; - let elab = - settings.core.elaborate || settings.core.dynamics - ? Interface.elaborate( - ~settings=settings.core, - statics.info_map, - editor.state.meta.view_term, - ) - : DHExp.Bool(true) |> DHExp.fresh; - let elab: Elaborator.Elaboration.t = {d: elab}; - let result: ModelResult.t = - settings.core.dynamics - ? Evaluation({ - elab, - evaluation: Interface.evaluate(~settings=settings.core, elab.d), - previous: ResultPending, - }) - : NoElab; - let footer = - settings.core.elaborate || settings.core.dynamics - ? footer( - ~locked=true, - ~select, - ~inject, - ~settings, - ~ui_state, - ~result_key=target_id, - ~result, - ~selected=None, - ) - : []; - editor_view( - ~select, - ~locked=true, - ~selected=None, - ~highlights=None, - ~inject, - ~ui_state, - ~settings, - ~footer, - ~test_results=ModelResult.test_results(result), - ~error_ids=statics.error_ids, - editor, - ); -}; diff --git a/src/haz3lweb/view/CodeEditor.re b/src/haz3lweb/view/CodeEditor.re deleted file mode 100644 index b6afc23824..0000000000 --- a/src/haz3lweb/view/CodeEditor.re +++ /dev/null @@ -1,202 +0,0 @@ -open Js_of_ocaml; -open Haz3lcore; -open Virtual_dom.Vdom; -type editor_id = string; - -type event = - | MouseDown(Measured.Point.t) - | DragTo(Measured.Point.t) - | MouseUp - | DoubleClick - | TripleClick - | JumpToBindingSiteOf(Measured.Point.t) - | StepSelected(int); - -let get_goal = - ( - ~font_metrics: FontMetrics.t, - text_box: Js.t(Dom_html.element), - e: Js.t(Dom_html.mouseEvent), - ) => { - let rect = text_box##getBoundingClientRect; - let goal_x = float_of_int(e##.clientX); - let goal_y = float_of_int(e##.clientY); - Measured.Point.{ - row: Float.to_int((goal_y -. rect##.top) /. font_metrics.row_height), - col: - Float.( - to_int(round((goal_x -. rect##.left) /. font_metrics.col_width)) - ), - }; -}; - -let mousedown_overlay = (~inject, ~font_metrics) => - Node.div( - ~attr= - Attr.many( - Attr.[ - id("mousedown-overlay"), - on_mouseup(_ => inject(MouseUp)), - on_mousemove(e => { - let mouse_handler = - e##.target |> Js.Opt.get(_, _ => failwith("no target")); - let text_box = - JsUtil.get_child_with_class( - mouse_handler##.parentNode - |> Js.Opt.get(_, _ => failwith("")) - |> Js.Unsafe.coerce, - "code-container", - ) - |> Option.get; - let goal = get_goal(~font_metrics, text_box, e); - inject(DragTo(goal)); - }), - ], - ), - [], - ); - -let mousedown_handler = (~inject: event => 'a, ~font_metrics, evt) => { - let goal = - get_goal( - ~font_metrics, - evt##.currentTarget - |> Js.Opt.get(_, _ => failwith("")) - |> JsUtil.get_child_with_class(_, "code-container") - |> Option.get, - evt, - ); - switch (JsUtil.ctrl_held(evt), JsUtil.num_clicks(evt)) { - | (true, _) => inject(JumpToBindingSiteOf(goal)) - | (false, 1) => inject(MouseDown(goal)) - | (false, 2) => inject(DoubleClick) - | (false, 3 | _) => inject(TripleClick) - }; -}; - -let test_status_icon_view = - (~font_metrics, insts, ms: Measured.Shards.t): option(Node.t) => - switch (ms) { - | [(_, {origin: _, last}), ..._] => - let status = insts |> TestMap.joint_status |> TestStatus.to_string; - let pos = DecUtil.abs_position(~font_metrics, last); - Some( - Node.div( - ~attr=Attr.many([Attr.classes(["test-result", status]), pos]), - [], - ), - ); - | _ => None - }; - -let test_result_layer = - (~font_metrics, ~measured: Measured.t, test_results: TestResults.t) - : list(Node.t) => - List.filter_map( - ((id, insts)) => - switch (Id.Map.find_opt(id, measured.tiles)) { - | Some(ms) => test_status_icon_view(~font_metrics, insts, ms) - | None => None - }, - test_results.test_map, - ); - -let deco = - ( - ~font_metrics, - ~show_backpack_targets, - ~selected, - ~error_ids, - ~test_results: option(TestResults.t), - ~highlights: option(ColorSteps.colorMap), - ~next_steps: list(Id.t), - ~inject, - { - state: { - zipper, - meta: {term_ranges, segment, measured, terms, tiles, _}, - _, - }, - _, - }: Editor.t, - ) => { - module Deco = - Deco.Deco({ - let map = measured; - let terms = terms; - let term_ranges = term_ranges; - let tiles = tiles; - let font_metrics = font_metrics; - let show_backpack_targets = show_backpack_targets; - let error_ids = error_ids; - let next_steps = next_steps; - }); - let inject = i => inject(StepSelected(i)); - let decos = - (selected ? Deco.all(zipper, segment) : Deco.err_holes(zipper)) - @ Deco.next_steps(zipper, ~inject); - let decos = - switch (test_results) { - | None => decos - | Some(test_results) => - decos @ test_result_layer(~font_metrics, ~measured, test_results) // TODO move into decos - }; - switch (highlights) { - | Some(colorMap) => - decos @ Deco.color_highlights(ColorSteps.to_list(colorMap)) - | _ => decos - }; -}; - -let view = - ( - ~select as _: unit => Ui_effect.t(unit), - ~inject: event => Ui_effect.t(unit), - ~ui_state as - {font_metrics, show_backpack_targets, mousedown, _}: Model.ui_state, - ~settings: Settings.t, - ~selected: bool=true, - ~locked=false, - ~test_results: option(TestResults.t), - ~highlights: option(ColorSteps.colorMap), - ~overlayer: option(Node.t)=None, - ~error_ids: list(Id.t), - ~sort=Sort.root, - ~next_steps, - editor: Editor.t, - ) => { - let code_text_view = Code.view(~sort, ~font_metrics, ~settings, editor); - let deco_view = - deco( - ~font_metrics, - ~show_backpack_targets, - ~selected, - ~error_ids, - ~test_results, - ~highlights, - ~next_steps, - ~inject, - editor, - ); - let code_view = - Node.div( - ~attr=Attr.many([Attr.classes(["code-container"])]), - [code_text_view] @ deco_view @ Option.to_list(overlayer), - ); - let mousedown_overlay = - selected && mousedown ? [mousedown_overlay(~inject, ~font_metrics)] : []; - let on_mousedown = - locked - ? _ => - Virtual_dom.Vdom.Effect.(Many([Prevent_default, Stop_propagation])) - : mousedown_handler(~inject, ~font_metrics); - - Node.div( - ~attr= - Attr.many([ - Attr.classes(["cell-item"]), - Attr.on_mousedown(on_mousedown), - ]), - mousedown_overlay @ [code_view], - ); -}; diff --git a/src/haz3lweb/view/Deco.re b/src/haz3lweb/view/Deco.re index 08f6e112e7..2348d5a3bf 100644 --- a/src/haz3lweb/view/Deco.re +++ b/src/haz3lweb/view/Deco.re @@ -2,25 +2,21 @@ open Virtual_dom.Vdom; open Util; open Haz3lcore; -module Deco = - ( - M: { - let font_metrics: FontMetrics.t; - let map: Measured.t; - let show_backpack_targets: bool; - let terms: TermMap.t; - let term_ranges: TermRanges.t; - let error_ids: list(Id.t); - let tiles: TileMap.t; - let next_steps: list(Id.t); - }, - ) => { - let font_metrics = M.font_metrics; +module Deco = (M: { + let ui_state: Model.ui_state; + let editor: Editor.t; + }) => { + let font_metrics = M.ui_state.font_metrics; + let map = M.editor.state.meta.measured; + let show_backpack_targets = M.ui_state.show_backpack_targets; + let terms = M.editor.state.meta.terms; + let term_ranges = M.editor.state.meta.term_ranges; + let tiles = M.editor.state.meta.tiles; - let tile = id => Id.Map.find(id, M.tiles); + let tile = id => Id.Map.find(id, tiles); let caret = (z: Zipper.t): list(Node.t) => { - let origin = Zipper.caret_point(M.map, z); + let origin = Zipper.caret_point(map, z); let shape = Zipper.caret_direction(z); let side = switch (Indicated.piece(z)) { @@ -46,11 +42,11 @@ module Deco = switch (p) { | Tile(t) => sel_of_tile(~start_shape, t) | Grout(g) => [ - Some(sel_shard_svg(~start_shape, Measured.find_g(g, M.map), p)), + Some(sel_shard_svg(~start_shape, Measured.find_g(g, map), p)), ] | Secondary(w) when Secondary.is_linebreak(w) => [None] | Secondary(w) => [ - Some(sel_shard_svg(~start_shape, Measured.find_w(w, M.map), p)), + Some(sel_shard_svg(~start_shape, Measured.find_w(w, map), p)), ] }; let start_shape = @@ -62,7 +58,7 @@ module Deco = } and sel_of_tile = (~start_shape, t: Tile.t): list(option(shard_data)) => { let tile_shards = - Measured.find_shards(t, M.map) + Measured.find_shards(t, map) |> List.filter(((i, _)) => List.mem(i, t.shards)) |> List.map(((index, measurement)) => [ @@ -120,12 +116,12 @@ module Deco = }; let range: option((Measured.Point.t, Measured.Point.t)) = { // if (Piece.has_ends(p)) { - let id = Id.Map.find(Piece.id(p), M.terms) |> Any.rep_id; - switch (TermRanges.find_opt(id, M.term_ranges)) { + let id = Id.Map.find(Piece.id(p), terms) |> Any.rep_id; + switch (TermRanges.find_opt(id, term_ranges)) { | None => None | Some((p_l, p_r)) => - let l = Measured.find_p(p_l, M.map).origin; - let r = Measured.find_p(p_r, M.map).last; + let l = Measured.find_p(p_l, map).origin; + let r = Measured.find_p(p_r, map).last; Some((l, r)); }; }; @@ -138,7 +134,7 @@ module Deco = | None => [] | Some(range) => let tiles = - Id.Map.find(Piece.id(p), M.terms) + Id.Map.find(Piece.id(p), terms) |> Any.ids /* NOTE(andrew): dark_ids were originally filtered here. * Leaving this comment in place in case issues in the @@ -146,11 +142,11 @@ module Deco = * |> List.filter(id => id >= 0)*/ |> List.map(id => { let t = tile(id); - (id, t.mold, Measured.find_shards(t, M.map)); + (id, t.mold, Measured.find_shards(t, map)); }); PieceDec.indicated( ~font_metrics, - ~rows=M.map.rows, + ~rows=map.rows, ~caret=(Piece.id(p), index), ~tiles, range, @@ -179,10 +175,10 @@ module Deco = switch (Siblings.neighbors((l, r))) { | (None, None) => failwith("impossible") | (_, Some(p)) => - let m = Measured.find_p(p, M.map); + let m = Measured.find_p(p, map); Measured.{origin: m.origin, last: m.origin}; | (Some(p), _) => - let m = Measured.find_p(p, M.map); + let m = Measured.find_p(p, map); Measured.{origin: m.last, last: m.last}; }; let profile = @@ -210,15 +206,11 @@ module Deco = }; let backpack = (z: Zipper.t): list(Node.t) => [ - BackpackView.view( - ~font_metrics, - ~origin=Zipper.caret_point(M.map, z), - z, - ), + BackpackView.view(~font_metrics, ~origin=Zipper.caret_point(map, z), z), ]; let targets' = (backpack, seg) => { - M.show_backpack_targets && Backpack.restricted(backpack) + show_backpack_targets && Backpack.restricted(backpack) ? targets(backpack, seg) : []; }; @@ -228,20 +220,20 @@ module Deco = deco: ((Measured.Point.t, Measured.Point.t, SvgUtil.Path.t)) => Node.t, ) => { - let (p_l, p_r) = TermRanges.find(id, M.term_ranges); - let l = Measured.find_p(p_l, M.map).origin; - let r = Measured.find_p(p_r, M.map).last; + let (p_l, p_r) = TermRanges.find(id, term_ranges); + let l = Measured.find_p(p_l, map).origin; + let r = Measured.find_p(p_r, map).last; open SvgUtil.Path; let r_edge = ListUtil.range(~lo=l.row, r.row + 1) |> List.concat_map(i => { - let row = Measured.Rows.find(i, M.map.rows); + let row = Measured.Rows.find(i, map.rows); [h(~x=i == r.row ? r.col : row.max_col), v_(~dy=1)]; }); let l_edge = ListUtil.range(~lo=l.row, r.row + 1) |> List.rev_map(i => { - let row = Measured.Rows.find(i, M.map.rows); + let row = Measured.Rows.find(i, map.rows); [h(~x=i == l.row ? l.col : row.indent), v_(~dy=-1)]; }) |> List.concat; @@ -279,16 +271,16 @@ module Deco = }; // faster info_map traversal - let err_holes = (_z: Zipper.t) => - List.map(term_highlight(~clss=["err-hole"]), M.error_ids); + let err_holes = error_ids => + List.map(term_highlight(~clss=["err-hole"]), error_ids); - let next_steps = (_z: Zipper.t, ~inject) => { - let tiles = List.filter_map(TileMap.find_opt(_, M.tiles), M.next_steps); + let next_steps = (next_steps, ~inject) => { + let tiles = List.filter_map(TileMap.find_opt(_, tiles), next_steps); List.mapi( (i, t: Tile.t) => { let id = Tile.id(t); let mold = t.mold; - let shards = Measured.find_shards(t, M.map); + let shards = Measured.find_shards(t, map); PieceDec.next_step_shards_indicated( ~font_metrics, ~caret=(Id.invalid, 0), @@ -301,13 +293,36 @@ module Deco = |> List.flatten; }; - let all = (zipper, sel_seg) => + let taken_step = taken_step => { + let tiles = + List.filter_map( + TileMap.find_opt(_, tiles), + taken_step |> Option.to_list, + ); + List.map( + (t: Tile.t) => { + let id = Tile.id(t); + let mold = t.mold; + let shards = Measured.find_shards(t, map); + PieceDec.taken_step_shards_indicated( + ~font_metrics, + ~caret=(Id.invalid, 0), + (id, mold, shards), + ); + }, + tiles, + ) + |> List.flatten; + }; + + let statics = eh => err_holes(eh); + + let editor = (zipper, sel_seg) => List.concat([ caret(zipper), indicated_piece_deco(zipper), selected_pieces(zipper), backpack(zipper), targets'(zipper.backpack, sel_seg), - err_holes(zipper), ]); }; diff --git a/src/haz3lweb/view/ExerciseMode.re b/src/haz3lweb/view/ExerciseMode.re index 04ad4130d5..fe5e927d7a 100644 --- a/src/haz3lweb/view/ExerciseMode.re +++ b/src/haz3lweb/view/ExerciseMode.re @@ -2,6 +2,8 @@ open Haz3lcore; open Virtual_dom.Vdom; open Node; +type model = Exercise.stitched(CellEditor.model); + type vis_marked('a) = | InstructorOnly(unit => 'a) | Always('a); @@ -20,7 +22,7 @@ let render_cells = (settings: Settings.t, v: list(vis_marked(Node.t))) => { let view = ( ~select, - ~inject, + ~inject_global, ~ui_state: Model.ui_state, ~selection: option((Exercise.pos, Editors.Selection.cell)), ~settings: Settings.t, @@ -55,27 +57,53 @@ let view = ~editor: Editor.t, ~caption: string, ~subcaption: option(string)=?, - ~footer=?, ~di: Exercise.DynamicsItem.t, - this_pos, + ~result_kind=CellResult.View.NoResults, + this_pos: Exercise.pos, ) => { - Cell.editor_view( + CellEditor.view( ~select=s => select((this_pos, s)), ~selected= switch (selection) { | Some((pos, s)) when pos == this_pos => Some(s) | _ => None }, - ~error_ids= - Statics.Map.error_ids(editor.state.meta.term_ranges, di.info_map), - ~inject, + ~inject= + fun + | ResultAction(StepperEditorAction(_, a)) + | MainEditor(a) => inject_global(UpdateAction.PerformAction(a)) + | ResultAction(StepperAction(a)) => + inject_global( + UpdateAction.StepperAction( + Exercise.key_for_statics(this_pos), + a, + ), + ) + | ResultAction(ToggleStepper) => + inject_global( + UpdateAction.ToggleStepper(Exercise.key_for_statics(this_pos)), + ), + ~inject_global, ~ui_state, ~settings, ~highlights, + ~result_kind, ~caption=Cell.caption(caption, ~rest=?subcaption), - ~test_results=ModelResult.test_results(di.result), - ~footer?, - editor, + { + editor: { + editor, + statics: { + term: di.term, + info_map: di.info_map, + error_ids: + Statics.Map.error_ids( + editor.state.meta.term_ranges, + di.info_map, + ), + }, + }, + result: di.result, + }, ); }; @@ -136,7 +164,7 @@ let view = switch (specific_ctx) { | None => Node.div([text("No context available")]) // TODO show exercise configuration error | Some(specific_ctx) => - CtxInspector.ctx_view(~inject, specific_ctx) + CtxInspector.ctx_view(~inject=inject_global, specific_ctx) }; }; }; @@ -160,13 +188,7 @@ let view = ~subcaption=": Your Tests vs. Correct Implementation", ~editor=eds.your_tests.tests, ~di=test_validation, - ~footer=[ - Grading.TestValidationReport.view( - ~inject, - grading_report.test_validation_report, - grading_report.point_distribution.test_validation, - ), - ], + ~result_kind=TestResults, ), ); @@ -189,7 +211,7 @@ let view = let mutation_testing_view = Always( Grading.MutationTestingReport.view( - ~inject, + ~inject=inject_global, grading_report.mutation_testing_report, grading_report.point_distribution.mutation_testing, ), @@ -202,17 +224,7 @@ let view = ~caption="Your Implementation", ~editor=eds.your_impl, ~di=user_impl, - ~footer= - Cell.footer( - ~locked=false, - ~settings, - ~select=s => select((YourImpl, s)), - ~inject, - ~ui_state, - ~selected=None, - ~result=user_impl.result, - ~result_key=Exercise.user_impl_key, - ), + ~result_kind=EvalResults, ), ); }; @@ -229,12 +241,7 @@ let view = ": Your Tests (code synchronized with Test Validation cell above) vs. Your Implementation", ~editor=eds.your_tests.tests, ~di=user_tests, - ~footer=[ - Cell.test_report_footer_view( - ~inject, - ~test_results=ModelResult.test_results(user_tests.result), - ), - ], + ~result_kind=TestResults, ), ); @@ -252,7 +259,7 @@ let view = let impl_grading_view = Always( Grading.ImplGradingReport.view( - ~inject, + ~inject=inject_global, ~report=grading_report.impl_grading_report, ~syntax_report=grading_report.syntax_report, ~max_points=grading_report.point_distribution.impl_grading, diff --git a/src/haz3lweb/view/ExplainThis.re b/src/haz3lweb/view/ExplainThis.re index 1fd597d85a..1b2480bbeb 100644 --- a/src/haz3lweb/view/ExplainThis.re +++ b/src/haz3lweb/view/ExplainThis.re @@ -209,21 +209,16 @@ let expander_deco = ~docs: ExplainThisModel.t, ~settings: Settings.t, ~inject, - ~ui_state as {font_metrics, _}: Model.ui_state, + ~ui_state as {font_metrics, _} as ui_state: Model.ui_state, ~options: list((ExplainThisForm.form_id, Segment.t)), ~group: ExplainThisForm.group, ~doc: ExplainThisForm.form, + editor, ) => { module Deco = Deco.Deco({ - let font_metrics = font_metrics; - let map = Measured.of_segment(doc.syntactic_form); - let show_backpack_targets = false; - let (_term, terms) = MakeTerm.go(doc.syntactic_form); - let term_ranges = TermRanges.mk(doc.syntactic_form); - let tiles = TileMap.mk(doc.syntactic_form); - let error_ids = []; - let next_steps = []; + let editor = editor; + let ui_state = ui_state; }); switch (doc.expandable_id, List.length(options)) { | (None, _) @@ -331,7 +326,6 @@ let expander_deco = let example_view = ( - ~select, ~inject, ~ui_state, ~settings: Settings.t, @@ -346,7 +340,7 @@ let example_view = div( ~attr=Attr.id("examples"), List.mapi( - (idx, {term, message, sub_id, _}: ExplainThisForm.example) => { + (_, {term, message, sub_id, _}: ExplainThisForm.example) => { let feedback = settings.explainThis.show_feedback ? [ @@ -362,13 +356,49 @@ let example_view = div( ~attr=clss(["example"]), [ - Cell.locked( - ~segment=term, - ~target_id="example" ++ string_of_int(idx), + CellEditor.view( + ~select=_ => Ui_effect.Ignore, + ~inject=_ => Ui_effect.Ignore, + ~inject_global=_ => Ui_effect.Ignore, ~ui_state, ~settings, - ~select, - ~inject, + ~highlights=None, + ~selected=None, + ~caption=None, + ~locked=true, + { + let editor = + Editor.init(~read_only=true, Zipper.unzip(term)); + let (term, _) = + MakeTerm.from_zip_for_sem(editor.state.zipper); + let statics = + CachedStatics.statics_of_term( + ~settings=settings.core, + term, + editor, + ); + let result: ModelResult.t = + settings.core.dynamics + ? Evaluation({ + elab: { + d: term, + }, + evaluation: + Interface.evaluate( + ~settings=settings.core, + term, + ), + previous: ResultPending, + }) + : NoElab; + { + editor: { + editor, + statics, + }, + result, + }; + }, ), div( ~attr=clss(["explanation"]), @@ -474,6 +504,8 @@ let get_doc = |> List.to_seq |> Id.Map.of_seq |> Option.some; + let editor = + Editor.init(~read_only=true, doc.syntactic_form |> Zipper.unzip); let expander_deco = expander_deco( ~docs, @@ -483,21 +515,30 @@ let get_doc = ~options, ~group, ~doc, + editor, ); + let highlight_deco = + switch (highlights) { + | Some(highlights) => + module Deco = + Deco.Deco({ + let editor = editor; + let ui_state = ui_state; + }); + Deco.color_highlights(ColorSteps.to_list(highlights)); + | None => [] + }; + let statics = CachedStatics.empty_statics; let syntactic_form_view = - Cell.locked_no_statics( - ~select=_ => Ui_effect.Ignore, - ~inject, + ReadOnlyEditor.view( ~ui_state, - ~segment=doc.syntactic_form, - ~highlights, ~settings, + ~overlays=highlight_deco @ [expander_deco], ~sort, - ~expander_deco, + {editor, statics}, ); let example_view = example_view( - ~select=_ => Ui_effect.Ignore, ~inject, ~ui_state, ~settings, @@ -506,7 +547,7 @@ let get_doc = ~examples=doc.examples, ~model=docs, ); - (syntactic_form_view, ([explanation], color_map), example_view); + ([syntactic_form_view], ([explanation], color_map), example_view); | Colorings => let (_, color_map) = mk_translation(~inject=None, explanation_msg); ([], ([], color_map), []); diff --git a/src/haz3lweb/view/Page.re b/src/haz3lweb/view/Page.re index 42bfe45b61..b55bd517a5 100644 --- a/src/haz3lweb/view/Page.re +++ b/src/haz3lweb/view/Page.re @@ -65,6 +65,11 @@ let main_view = ~inject: UpdateAction.t => Ui_effect.t(unit), {settings, editors, explainThisModel, results, statics, ui_state, _}: Model.t, ) => { + let _ = + switch (ui_state.active_editor) { + | Some(ae) => print_endline("SELECTED: " ++ Editors.Selection.show(ae)) + | None => print_endline("NO ACTIVE EDITOR") + }; let cursor_info = Editors.get_cursor_info( ~selection=ui_state.active_editor, @@ -160,7 +165,7 @@ let main_view = inject( UpdateAction.MakeActive(Editors.Selection.Exercises(pos, sel)), ), - ~inject, + ~inject_global=inject, ~ui_state, ~settings, ~selection, diff --git a/src/haz3lweb/view/ScratchMode.re b/src/haz3lweb/view/ScratchMode.re index ed7a88eb15..a7ca37aec0 100644 --- a/src/haz3lweb/view/ScratchMode.re +++ b/src/haz3lweb/view/ScratchMode.re @@ -3,50 +3,41 @@ open Haz3lcore; let view = ( ~select, - ~inject, + ~inject: UpdateAction.t => Ui_effect.t(unit), ~ui_state: Model.ui_state, ~settings: Settings.t, ~highlights, ~results: ModelResults.t, ~result_key, - ~statics as {error_ids, _}: CachedStatics.statics, + ~statics: CachedStatics.statics, ~selected, editor: Editor.t, ) => { - let result = ModelResults.lookup(results, result_key); - let test_results = Util.OptUtil.and_then(ModelResult.test_results, result); - let footer = - settings.core.elaborate || settings.core.dynamics - ? result - |> Option.map(result => - Cell.footer( - ~locked=false, - ~settings, - ~select, - ~inject, - ~ui_state, - ~result, - ~selected= - switch (selected) { - | Some(Editors.Selection.Result(i)) => Some(i) - | _ => None - }, - ~result_key, - ) - ) - : None; + let result = ModelResults.lookup(results, result_key) |> Option.get; [ - Cell.editor_view( + CellEditor.view( ~select, - ~inject, + ~inject= + fun + | MainEditor(a) => inject(PerformAction(a)) + | ResultAction(StepperAction(a)) => + inject(StepperAction(result_key, a)) + | ResultAction(ToggleStepper) => inject(ToggleStepper(result_key)) + | ResultAction(StepperEditorAction(_, a)) => + inject(PerformAction(a)), + ~inject_global=inject, ~ui_state, ~settings, - ~error_ids, - ~test_results, - ~footer?, ~highlights, ~selected, - editor, + ~locked=false, + { + editor: { + editor, + statics, + }, + result, + }, ), ]; }; diff --git a/src/haz3lweb/view/dec/PieceDec.re b/src/haz3lweb/view/dec/PieceDec.re index 70aadb02a6..f8d5499517 100644 --- a/src/haz3lweb/view/dec/PieceDec.re +++ b/src/haz3lweb/view/dec/PieceDec.re @@ -128,7 +128,12 @@ let next_step_indicated = ~shapes, ~path_cls, ~base_cls, - ~attr=[Attr.on_mousedown(_ => {inject()})], + ~attr=[ + Attr.on_mousedown(_ => { + print_endline("CLICK!"); + inject(); + }), + ], measurement, ); }; @@ -154,6 +159,37 @@ let next_step_shards_indicated = shards, ); +let taken_step_indicated = + ( + ~font_metrics, + ~has_caret, + ~shapes, + ~sort, + ~measurement: Measured.measurement, + ) + : t => { + let path_cls = + ["tile-path", "raised", Sort.to_string(sort)] + @ (has_caret ? ["indicated-caret"] : ["indicated"]); + let base_cls = ["tile-taken-step"]; + simple_shard(~font_metrics, ~shapes, ~path_cls, ~base_cls, measurement); +}; + +let taken_step_shards_indicated = + (~font_metrics: FontMetrics.t, ~caret: (Id.t, int), (id, mold, shards)) + : list(t) => + List.map( + ((index, measurement)) => + taken_step_indicated( + ~font_metrics, + ~has_caret=caret == (id, index), + ~shapes=Mold.nib_shapes(~index, mold), + ~sort=mold.out, + ~measurement, + ), + shards, + ); + let shadowfudge = Path.cmdfudge(~y=DecUtil.shadow_adj); let shards_of_tiles = tiles => diff --git a/src/haz3lweb/view/editor/Cell.re b/src/haz3lweb/view/editor/Cell.re new file mode 100644 index 0000000000..c4834291b9 --- /dev/null +++ b/src/haz3lweb/view/editor/Cell.re @@ -0,0 +1,45 @@ +open Haz3lcore; +open Virtual_dom.Vdom; +open Node; + +let narrative_cell = (content: Node.t) => + div( + ~attr=Attr.class_("cell"), + [div(~attr=Attr.class_("cell-chapter"), [content])], + ); + +let simple_cell_item = (content: list(Node.t)) => + div(~attr=Attr.classes(["cell-item"]), content); + +let caption = (~rest: option(string)=?, bolded: string) => + div( + ~attr=Attr.many([Attr.classes(["cell-caption"])]), + [strong([text(bolded)])] @ (rest |> Option.map(text) |> Option.to_list), + ); + +let simple_cell_view = (items: list(t)) => + div(~attr=Attr.class_("cell"), items); + +let report_footer_view = content => { + div(~attr=Attr.classes(["cell-item", "cell-report"]), content); +}; + +let test_report_footer_view = (~inject, ~test_results: option(TestResults.t)) => { + report_footer_view([TestView.test_summary(~inject, ~test_results)]); +}; + +let panel = (~classes=[], content, ~footer: option(t)) => { + simple_cell_view( + [div(~attr=Attr.classes(["cell-item", "panel"] @ classes), content)] + @ Option.to_list(footer), + ); +}; + +let title_cell = title => { + simple_cell_view([ + div( + ~attr=Attr.class_("title-cell"), + [div(~attr=Attr.class_("title-text"), [text(title)])], + ), + ]); +}; diff --git a/src/haz3lweb/view/editor/CellEditor.re b/src/haz3lweb/view/editor/CellEditor.re new file mode 100644 index 0000000000..858828c345 --- /dev/null +++ b/src/haz3lweb/view/editor/CellEditor.re @@ -0,0 +1,83 @@ +open Haz3lcore; +open Virtual_dom.Vdom; +open Node; + +type model = { + editor: CodeEditor.model, + result: ModelResult.t, +}; + +type action = + | MainEditor(CodeEditor.action) + | ResultAction(CellResult.action); + +let update = ReadOnlyEditor.update; + +let calculate = ReadOnlyEditor.calculate; + +type event = CodeEditor.event; + +let view = + ( + ~select: Editors.Selection.cell => Ui_effect.t(unit), + ~inject, + ~inject_global, + ~ui_state: Model.ui_state, + ~settings: Settings.t, + ~highlights: option(ColorSteps.colorMap), + ~selected: option(Editors.Selection.cell), + ~caption: option(Node.t)=?, + ~sort=?, + ~result_kind=?, + ~locked=false, + model, + ) => { + let (footer, overlays) = + CellResult.view( + ~signal= + fun + | MakeActive(a) => select(a) + | MouseUp => inject_global(Update.SetMeta(Mouseup)) + | MouseDown => inject_global(Update.SetMeta(Mousedown)), + ~inject=a => inject(ResultAction(a)), + ~inject_global, + ~ui_state, + ~settings, + ~selected=selected == Some(Result(0)), + ~result_kind?, + ~locked, + model.result, + ); + div( + ~attr= + Attr.classes([ + "cell", + Option.is_some(selected) ? "selected" : "deselected", + locked ? "locked" : "unlocked", + ]), + Option.to_list(caption) + @ [ + CodeEditor.view( + ~signal= + locked + ? _ => Ui_effect.Ignore + : fun + | MouseUp => inject_global(Update.SetMeta(Mouseup)) + | MouseDown => inject_global(Update.SetMeta(Mousedown)) + | MakeActive => select(Editors.Selection.MainEditor), + ~inject= + locked + ? _ => Ui_effect.Ignore + : (action => inject_global(PerformAction(action))), + ~ui_state, + ~settings, + ~selected=selected == Some(MainEditor), + ~highlights, + ~overlays=overlays(model.editor.editor), + ~sort?, + model.editor, + ), + ] + @ footer, + ); +}; diff --git a/src/haz3lweb/view/editor/CellResult.re b/src/haz3lweb/view/editor/CellResult.re new file mode 100644 index 0000000000..e3f8fa716d --- /dev/null +++ b/src/haz3lweb/view/editor/CellResult.re @@ -0,0 +1,435 @@ +open Haz3lcore; +open Virtual_dom.Vdom; +open Sexplib.Std; +open Node; +open Util; + +type model = ModelResult.t; + +[@deriving (show({with_path: false}), sexp, yojson)] +type action = + | StepperEditorAction(int, Action.t) + | StepperAction(UpdateAction.stepper_action) + | ToggleStepper; + +let update = (~settings: CoreSettings.t, action, model) => + switch (action) { + | StepperEditorAction(idx, action) => + ModelResult.perform(~settings, idx, action, model) + | StepperAction(stepper_action) => + switch (stepper_action) { + | UpdateAction.StepForward(idx) => ModelResult.step_forward(idx, model) + | UpdateAction.StepBackward => + ModelResult.step_backward(~settings=settings.evaluation, model) + | UpdateAction.HideStepper => ModelResult.toggle_stepper(~settings, model) + } + | ToggleStepper => ModelResult.toggle_stepper(~settings, model) + }; + +module View = { + type event = + | MakeActive(Editors.Selection.cell) + | MouseUp + | MouseDown; + + let error_msg = (err: ProgramResult.error) => + switch (err) { + | EvaulatorError(err) => EvaluatorError.show(err) + | UnknownException(str) => str + | Timeout => "Evaluation timed out" + }; + + let status_of: ProgramResult.t => string = + fun + | ResultPending => "pending" + | ResultOk(_) => "ok" + | ResultFail(_) => "fail" + | Off(_) => "off"; + + let stepper_view = + ( + ~signal as _: event => Ui_effect.t(unit), + ~inject: action => Ui_effect.t(unit), + ~inject_global: Update.t => Ui_effect.t(unit), + ~ui_state, + ~settings: Settings.t, + ~read_only: bool, + stepper: Stepper.t, + ) => { + let history = + Stepper.get_history(~settings=settings.core.evaluation, stepper); + switch (history) { + | [] => [] + | [hd, ..._] => + let button_back = + Widgets.button_d( + Icons.undo, + inject(StepperAction(StepBackward)), + ~disabled= + !Stepper.can_undo(~settings=settings.core.evaluation, stepper), + ~tooltip="Step Backwards", + ); + let button_hide_stepper = + Widgets.toggle(~tooltip="Show Stepper", "s", true, _ => + inject(StepperAction(HideStepper)) + ); + let toggle_show_history = + Widgets.toggle( + ~tooltip="Show History", + "h", + settings.core.evaluation.stepper_history, + _ => + inject_global(Set(Evaluation(ShowRecord))) + ); + let eval_settings = + Widgets.button(Icons.gear, _ => + inject_global(Set(Evaluation(ShowSettings))) + ); + let (statics, editor, _) = hd.hidden_history |> Aba.hd; + let current_model: StepperEditor.Steppable.model = { + editor: { + editor, + statics, + }, + next_steps: + List.map( + (option: EvaluatorStep.EvalObj.t) => option.d_loc |> Exp.rep_id, + stepper.next_options, + ), + }; + let current = + div( + ~attr=Attr.classes(["cell-item", "cell-result"]), + read_only + ? [ + div(~attr=Attr.class_("equiv"), [Node.text("≡")]), + StepperEditor.Steppable.view( + // TODO: Maybe get rid of this signal? + ~signal= + (TakeStep(x)) => inject(StepperAction(StepForward(x))), + ~ui_state, + ~settings, + ~overlays=[], + current_model, + ), + ] + : [ + div(~attr=Attr.class_("equiv"), [Node.text("≡")]), + StepperEditor.Steppable.view( + ~signal= + (TakeStep(x)) => inject(StepperAction(StepForward(x))), + ~ui_state, + ~settings, + ~overlays=[], + current_model, + ), + button_back, + eval_settings, + toggle_show_history, + button_hide_stepper, + ], + ); + let previous_step = + (~hidden: bool, ~idx as _, step: Stepper.step_info): list(Node.t) => { + let (statics, editor, _) = hd.hidden_history |> Aba.hd; + let _ = "One" |> print_endline; + let model: StepperEditor.Stepped.model = { + editor: { + editor, + statics, + }, + step: step.chosen_step |> Option.get, // TODO[Matt]: refactor away Option.get + step_id: (step.chosen_step |> Option.get).d_loc |> Exp.rep_id, + }; + let _ = "Two" |> print_endline; + [ + div( + ~attr= + Attr.classes( + ["cell-item", "cell-result"] @ (hidden ? ["hidden"] : []), + ), + [ + div(~attr=Attr.class_("equiv"), [Node.text("≡")]), + StepperEditor.Stepped.view( + ~ui_state, + ~settings, + ~overlays=[], + model, + ), + div( + ~attr=Attr.classes(["stepper-justification"]), + step.chosen_step + |> Option.map((chosen_step: EvaluatorStep.step) => + chosen_step.knd |> Stepper.get_justification |> Node.text + ) + |> Option.to_list, + ), + ], + ), + ]; + }; + ( + ( + settings.core.evaluation.stepper_history + ? { + let steps: list((bool, Stepper.step_info)) = + List.map( + step => + [ + (false, step), + ...settings.core.evaluation.show_hidden_steps + ? Stepper.hidden_steps_of_info(step) + |> List.map(x => (true, x)) + : [], + ], + history, + ) + |> List.flatten + |> List.rev + |> List.tl + |> List.rev; + List.mapi( + (idx, (hidden, step)) => + previous_step(~hidden, ~idx=idx + 1, step), + steps |> List.rev, + ) + |> List.flatten; + } + : [] + ) + @ [current] + ) + @ ( + settings.core.evaluation.show_settings + ? SettingsModal.view( + ~inject=inject_global, + settings.core.evaluation, + ) + : [] + ); + }; + }; + + let live_eval = + ( + ~signal: event => Ui_effect.t(unit), + ~inject: action => Ui_effect.t(unit), + ~ui_state, + ~settings: Settings.t, + ~selected, + ~locked, + result: ModelResult.eval_result, + ) => { + let editor = + switch (result.evaluation, result.previous) { + | (ResultOk(res), _) => res.editor + | (ResultPending, ResultOk(res)) => res.editor + | _ => result.elab.d |> ExpToSegment.exp_to_editor(~inline=false) + }; + let code_view = + CodeEditor.view( + ~signal= + fun + | MakeActive => signal(MakeActive(MainEditor)) + | MouseUp => signal(MouseUp) + | MouseDown => signal(MouseDown), + ~inject=a => inject(StepperEditorAction(0, a)), + ~ui_state, + ~settings, + ~selected, + ~highlights=None, + ~sort=Sort.root, + {editor, statics: CachedStatics.empty_statics}, + ); + let exn_view = + switch (result.evaluation) { + | ResultFail(err) => [ + div(~attr=Attr.classes(["error-msg"]), [text(error_msg(err))]), + ] + | _ => [] + }; + Node.( + div( + ~attr=Attr.classes(["cell-item", "cell-result"]), + exn_view + @ [ + div( + ~attr=Attr.classes(["status", status_of(result.evaluation)]), + [ + div(~attr=Attr.classes(["spinner"]), []), + div(~attr=Attr.classes(["eq"]), [text("≡")]), + ], + ), + div( + ~attr=Attr.classes(["result", status_of(result.evaluation)]), + [code_view], + ), + ] + @ ( + locked + ? [] + : [ + Widgets.toggle(~tooltip="Show Stepper", "s", false, _ => + inject(ToggleStepper) + ), + ] + ), + ) + ); + }; + + let footer = + ( + ~signal, + ~inject, + ~inject_global, + ~ui_state: Model.ui_state, + ~settings: Settings.t, + ~result: ModelResult.t, + ~selected: option(int), + ~locked, + ) => + switch (result) { + | _ when !settings.core.dynamics => [] + | NoElab => [] + | Evaluation(result) => [ + live_eval( + ~signal, + ~inject, + ~ui_state, + ~settings, + ~selected=selected == Some(0), + ~locked, + result, + ), + ] + | Stepper(s) => + stepper_view( + ~signal, + ~inject, + ~inject_global, + ~settings, + ~ui_state, + ~read_only=locked, + s, + ) + }; + + let test_status_icon_view = + (~font_metrics, insts, ms: Measured.Shards.t): option(Node.t) => + switch (ms) { + | [(_, {origin: _, last}), ..._] => + let status = insts |> TestMap.joint_status |> TestStatus.to_string; + let pos = DecUtil.abs_position(~font_metrics, last); + Some( + Node.div( + ~attr=Attr.many([Attr.classes(["test-result", status]), pos]), + [], + ), + ); + | _ => None + }; + + let test_result_layer = + (~font_metrics, ~measured: Measured.t, test_results: TestResults.t) + : list(Node.t) => + List.filter_map( + ((id, insts)) => + switch (Id.Map.find_opt(id, measured.tiles)) { + | Some(ms) => test_status_icon_view(~font_metrics, insts, ms) + | None => None + }, + test_results.test_map, + ); + + type result_kind = + | NoResults + | TestResults + | EvalResults; + + let view = + ( + ~signal: event => Ui_effect.t(unit), + ~inject: action => Ui_effect.t(unit), + ~inject_global: UpdateAction.t => Ui_effect.t(unit), + ~ui_state: Model.ui_state, + ~settings: Settings.t, + ~selected: bool, + ~result_kind=EvalResults, + ~locked: bool, + model: model, + ) => + switch (result_kind) { + // Normal case: + | EvalResults when settings.core.dynamics => + let result = + footer( + ~signal, + ~inject, + ~inject_global, + ~ui_state: Model.ui_state, + ~settings, + ~result=model, + ~selected=selected ? Some(0) : None, + ~locked, + ); + let test_overlay = (editor: Editor.t) => + switch (ModelResult.test_results(model)) { + | Some(result) => + test_result_layer( + ~font_metrics=ui_state.font_metrics, + ~measured=editor.state.meta.measured, + result, + ) + | None => [] + }; + (result, test_overlay); + + // Just showing elaboration because evaluation is off: + | EvalResults when settings.core.elaborate => + let result = [ + text("Evaluation disabled, showing elaboration:"), + switch (ModelResult.get_elaboration(model)) { + | Some(elab) => + ReadOnlyEditor.view( + ~ui_state, + ~settings, + { + editor: elab.d |> ExpToSegment.exp_to_editor(~inline=false), + statics: CachedStatics.empty_statics, + }: CodeEditor.model, + ) + | None => text("No elaboration found") + }, + ]; + (result, (_ => [])); + + // Not showing any results: + | EvalResults + | NoResults => ([], (_ => [])) + + // Just showing test results (school mode) + | TestResults => + let test_results = ModelResult.test_results(model); + let test_overlay = (editor: Editor.t) => + switch (ModelResult.test_results(model)) { + | Some(result) => + test_result_layer( + ~font_metrics=ui_state.font_metrics, + ~measured=editor.state.meta.measured, + result, + ) + | None => [] + }; + ( + [ + Cell.report_footer_view([ + TestView.test_summary(~inject=inject_global, ~test_results), + ]), + ], + test_overlay, + ); + }; +}; + +let view = View.view; diff --git a/src/haz3lweb/view/editor/CodeEditor.re b/src/haz3lweb/view/editor/CodeEditor.re new file mode 100644 index 0000000000..6fb319321a --- /dev/null +++ b/src/haz3lweb/view/editor/CodeEditor.re @@ -0,0 +1,149 @@ +open Js_of_ocaml; +open Haz3lcore; +open Virtual_dom.Vdom; +type editor_id = string; + +type model = ReadOnlyEditor.model; + +type action = ReadOnlyEditor.action; + +let update = ReadOnlyEditor.update; + +let calculate = ReadOnlyEditor.calculate; + +type event = + | MakeActive + | MouseUp + | MouseDown; + +module View = { + let get_goal = + ( + ~font_metrics: FontMetrics.t, + text_box: Js.t(Dom_html.element), + e: Js.t(Dom_html.mouseEvent), + ) => { + let rect = text_box##getBoundingClientRect; + let goal_x = float_of_int(e##.clientX); + let goal_y = float_of_int(e##.clientY); + Measured.Point.{ + row: Float.to_int((goal_y -. rect##.top) /. font_metrics.row_height), + col: + Float.( + to_int(round((goal_x -. rect##.left) /. font_metrics.col_width)) + ), + }; + }; + + let mousedown_overlay = (~signal, ~inject, ~font_metrics) => + Node.div( + ~attr= + Attr.many( + Attr.[ + id("mousedown-overlay"), + on_mouseup(_ => signal(MouseUp)), + on_mousemove(e => { + let mouse_handler = + e##.target |> Js.Opt.get(_, _ => failwith("no target")); + let text_box = + JsUtil.get_child_with_class( + mouse_handler##.parentNode + |> Js.Opt.get(_, _ => failwith("")) + |> Js.Unsafe.coerce, + "code-container", + ) + |> Option.get; + let goal = get_goal(~font_metrics, text_box, e); + inject(Action.Select(Resize(Goal(Point(goal))))); + }), + ], + ), + [], + ); + + let mousedown_handler = (~signal, ~inject, ~font_metrics, evt) => { + let goal = + get_goal( + ~font_metrics, + evt##.currentTarget + |> Js.Opt.get(_, _ => failwith("")) + |> JsUtil.get_child_with_class(_, "code-container") + |> Option.get, + evt, + ); + switch (JsUtil.ctrl_held(evt), JsUtil.num_clicks(evt)) { + | (true, _) => + Effect.Many([ + signal(MakeActive), + inject(Action.Move(Goal(Point(goal)))), + inject(Action.Jump(BindingSiteOfIndicatedVar)), + ]) + | (false, 1) => + Effect.Many([ + signal(MouseDown), + signal(MakeActive), + inject(Action.Move(Goal(Point(goal)))), + ]) + | (false, 2) => inject(Action.Select(Tile(Current))) + | (false, 3 | _) => inject(Action.Select(Smart)) + }; + }; + + let view = + ( + ~signal: event => Ui_effect.t(unit), + ~inject: action => Ui_effect.t(unit), + ~ui_state: Model.ui_state, + ~settings: Settings.t, + ~selected: bool, + ~highlights: option(ColorSteps.colorMap), + ~overlays: list(Node.t)=[], + ~sort=?, + model: model, + ) => { + let edit_decos = { + module Deco = + Deco.Deco({ + let editor = model.editor; + let ui_state = ui_state; + }); + Deco.editor(model.editor.state.zipper, model.editor.state.meta.segment) + @ ( + switch (highlights) { + | Some(colorMap) => + Deco.color_highlights(ColorSteps.to_list(colorMap)) + | _ => [] + } + ); + }; + let overlays = edit_decos @ overlays; + let code_view = + ReadOnlyEditor.view(~ui_state, ~settings, ~overlays, ~sort?, model); + let mousedown_overlay = + selected && ui_state.mousedown + ? [ + mousedown_overlay( + ~signal, + ~inject, + ~font_metrics=ui_state.font_metrics, + ), + ] + : []; + let on_mousedown = + mousedown_handler( + ~signal, + ~inject, + ~font_metrics=ui_state.font_metrics, + ); + Node.div( + ~attr= + Attr.many([ + Attr.classes(["cell-item"]), + Attr.on_mousedown(on_mousedown), + ]), + mousedown_overlay @ [code_view], + ); + }; +}; + +let view = View.view; diff --git a/src/haz3lweb/view/editor/ReadOnlyEditor.re b/src/haz3lweb/view/editor/ReadOnlyEditor.re new file mode 100644 index 0000000000..6129af4d56 --- /dev/null +++ b/src/haz3lweb/view/editor/ReadOnlyEditor.re @@ -0,0 +1,64 @@ +open Virtual_dom.Vdom; +open Util.Result.Syntax; +open Haz3lcore; + +type model = { + // Update: + editor: Editor.t, + // Calculate: + statics: CachedStatics.statics, +}; + +type action = Action.t; + +let update = (~settings, action, model) => { + let+ editor = Perform.go(~settings, action, model.editor); + {editor, statics: model.statics}; +}; + +let calculate = (~settings, ~stitch, {editor, statics} as model) => { + let term = MakeTerm.from_zip_for_sem(editor.state.zipper) |> fst |> stitch; + if (Exp.fast_equal(term, statics.term)) { + model; + } else { + { + editor, + statics: CachedStatics.statics_of_term(~settings, term, editor), + }; + }; +}; + +// There are no events for a read-only editor +type event; + +// read-only editors cannot be selected +type selection; + +let view = + ( + ~ui_state: Model.ui_state, + ~settings, + ~overlays: list(Node.t)=[], + ~sort=Sort.root, + model: model, + ) => { + let code_text_view = + Code.view( + ~sort, + ~font_metrics=ui_state.font_metrics, + ~settings, + model.editor, + ); + let statics_decos = { + module Deco = + Deco.Deco({ + let ui_state = ui_state; + let editor = model.editor; + }); + Deco.statics(model.statics.error_ids); + }; + Node.div( + ~attr=Attr.many([Attr.classes(["code-container"])]), + [code_text_view] @ statics_decos @ overlays, + ); +}; diff --git a/src/haz3lweb/view/editor/StepperEditor.re b/src/haz3lweb/view/editor/StepperEditor.re new file mode 100644 index 0000000000..a120b17a71 --- /dev/null +++ b/src/haz3lweb/view/editor/StepperEditor.re @@ -0,0 +1,60 @@ +open Haz3lcore; + +module Stepped = { + type model = { + editor: ReadOnlyEditor.model, + step: EvaluatorStep.step, + step_id: Id.t, + }; + + type action = ReadOnlyEditor.action; + + type event = ReadOnlyEditor.event; + + type selection = ReadOnlyEditor.selection; + + let view = + (~ui_state: Model.ui_state, ~settings, ~overlays=[], model: model) => { + let overlays = { + module Deco = + Deco.Deco({ + let editor = model.editor.editor; + let ui_state = ui_state; + }); + overlays @ Deco.taken_step(Some(model.step_id)); + }; + ReadOnlyEditor.view(~ui_state, ~settings, ~overlays, model.editor); + }; +}; + +module Steppable = { + type model = { + editor: CodeEditor.model, + next_steps: list(Id.t), + }; + + type action = CodeEditor.action; + + type event = + | TakeStep(int); + + let view = + ( + ~signal: event => Ui_effect.t(unit), + ~ui_state: Model.ui_state, + ~settings, + ~overlays=[], + model: model, + ) => { + let overlays = { + module Deco = + Deco.Deco({ + let editor = model.editor.editor; + let ui_state = ui_state; + }); + overlays + @ Deco.next_steps(model.next_steps, ~inject=x => signal(TakeStep(x))); + }; + ReadOnlyEditor.view(~ui_state, ~settings, ~overlays, model.editor); + }; +};