From 08c21d1de7f22a5b5fe5507dab25b8ed159e3c45 Mon Sep 17 00:00:00 2001 From: disconcision Date: Tue, 19 Nov 2024 23:02:16 -0500 Subject: [PATCH] live projectors view layer. minimal poc complete --- src/haz3lcore/Measured.re | 8 +++-- src/haz3lcore/zipper/Editor.re | 14 +++++---- src/haz3lcore/zipper/Printer.re | 2 +- src/haz3lcore/zipper/Projector.re | 4 +-- src/haz3lcore/zipper/ProjectorBase.re | 1 + src/haz3lcore/zipper/projectors/FoldProj.re | 18 ++++++++++-- src/haz3lweb/app/common/ProjectorView.re | 6 +++- src/haz3lweb/app/editors/cell/CellEditor.re | 28 +++++++++++++++++- src/haz3lweb/app/editors/code/Code.re | 22 +++++++++++--- src/haz3lweb/app/editors/code/CodeEditable.re | 5 +++- src/haz3lweb/app/editors/code/CodeViewable.re | 29 +++++++++++++++---- .../app/editors/code/CodeWithStatics.re | 26 +++++++++++++++-- .../app/editors/decoration/BackpackView.re | 4 ++- src/haz3lweb/app/editors/decoration/Deco.re | 6 +++- src/haz3lweb/app/editors/mode/ExerciseMode.re | 4 ++- src/haz3lweb/app/editors/result/EvalResult.re | 8 +++++ src/haz3lweb/app/editors/result/Stepper.re | 3 ++ .../app/editors/result/StepperEditor.re | 12 +++++++- src/haz3lweb/app/explainthis/ExplainThis.re | 5 ++++ 19 files changed, 171 insertions(+), 34 deletions(-) diff --git a/src/haz3lcore/Measured.re b/src/haz3lcore/Measured.re index 61dad8a831..d5b1305e4b 100644 --- a/src/haz3lcore/Measured.re +++ b/src/haz3lcore/Measured.re @@ -282,7 +282,8 @@ let last_of_token = (token: string, origin: Point.t): Point.t => row: origin.row + StringUtil.num_linebreaks(token), }; -let of_segment = (seg: Segment.t, info_map: Statics.Map.t): t => { +let of_segment = + (seg: Segment.t, info_map: Statics.Map.t, dyn_map: TestMap.t): t => { let is_indented = is_indented_map(seg); // recursive across seg's bidelimited containers @@ -353,8 +354,9 @@ let of_segment = (seg: Segment.t, info_map: Statics.Map.t): t => { let map = map |> add_g(g, {origin, last}); (contained_indent, last, map); | Projector(p) => - let token = - Projector.placeholder(p, Id.Map.find_opt(p.id, info_map)); + let ci = Id.Map.find_opt(p.id, info_map); + let dyn = TestMap.lookup(p.id, dyn_map); + let token = Projector.placeholder(p, ci, dyn); let last = last_of_token(token, origin); let map = extra_rows(token, origin, map); let map = add_pr(p, {origin, last}, map); diff --git a/src/haz3lcore/zipper/Editor.re b/src/haz3lcore/zipper/Editor.re index 819ae28bf3..baa8e45621 100644 --- a/src/haz3lcore/zipper/Editor.re +++ b/src/haz3lcore/zipper/Editor.re @@ -33,7 +33,7 @@ module CachedSyntax = { let yojson_of_t = _ => failwith("Editor.Meta.yojson_of_t"); let t_of_yojson = _ => failwith("Editor.Meta.t_of_yojson"); - let init = (z, info_map): t => { + let init = (z, info_map, dyn_map): t => { let segment = Zipper.unselect_and_zip(z); let MakeTerm.{term, terms, projectors} = MakeTerm.go(segment); { @@ -42,7 +42,7 @@ module CachedSyntax = { term_ranges: TermRanges.mk(segment), tiles: TileMap.mk(segment), holes: Segment.holes(segment), - measured: Measured.of_segment(segment, info_map), + measured: Measured.of_segment(segment, info_map, dyn_map), selection_ids: Selection.selection_ids(z.selection), term, terms, @@ -52,9 +52,9 @@ module CachedSyntax = { let mark_old: t => t = old => {...old, old: true}; - let calculate = (z: Zipper.t, info_map, old: t) => + let calculate = (z: Zipper.t, info_map, dyn_map, old: t) => old.old - ? init(z, info_map) + ? init(z, info_map, dyn_map) : {...old, selection_ids: Selection.selection_ids(z.selection)}; }; @@ -97,7 +97,7 @@ module Model = { col_target: None, }, history: History.empty, - syntax: CachedSyntax.init(zipper, Id.Map.empty), + syntax: CachedSyntax.init(zipper, Id.Map.empty, TestMap.empty), }; type persistent = PersistentZipper.t; @@ -241,6 +241,7 @@ module Update = { ~settings: CoreSettings.t, ~is_edited, new_statics, + dyn_map, {syntax, state, history}: Model.t, ) => { // 1. Recalculate the autocomplete buffer if necessary @@ -264,7 +265,8 @@ module Update = { // 2. Recalculate syntax cache let syntax = is_edited ? CachedSyntax.mark_old(syntax) : syntax; - let syntax = CachedSyntax.calculate(zipper, new_statics.info_map, syntax); + let syntax = + CachedSyntax.calculate(zipper, new_statics.info_map, dyn_map, syntax); // Recombine Model.{ diff --git a/src/haz3lcore/zipper/Printer.re b/src/haz3lcore/zipper/Printer.re index 1ab6b176f5..0c7c140f4d 100644 --- a/src/haz3lcore/zipper/Printer.re +++ b/src/haz3lcore/zipper/Printer.re @@ -58,7 +58,7 @@ let measured = z => z |> ProjectorPerform.Update.remove_all |> Zipper.seg_without_buffer - |> Measured.of_segment(_, Id.Map.empty); + |> Measured.of_segment(_, Id.Map.empty, TestMap.empty); let pretty_print = (~holes: option(string)=Some(""), z: Zipper.t): string => to_rows( diff --git a/src/haz3lcore/zipper/Projector.re b/src/haz3lcore/zipper/Projector.re index 82b036b821..f06b7e879a 100644 --- a/src/haz3lcore/zipper/Projector.re +++ b/src/haz3lcore/zipper/Projector.re @@ -25,8 +25,8 @@ let shape = (p: Base.projector, info: info): shape => { * in the zipper; a tile consisting of any number of whitespaces * is considered a placeholder. This could be made more principled. * Note that a placeholder retains the UUID of the underlying. */ -let placeholder = (p: Base.projector, ci: option(Info.t)): string => - switch (shape(p, {id: p.id, syntax: p.syntax, ci})) { +let placeholder = (p: Base.projector, ci: option(Info.t), dyn): string => + switch (shape(p, {id: p.id, syntax: p.syntax, ci, dyn})) { | Inline(width) => String.make(width, ' ') | Block({row, col}) => String.make(row - 1, '\n') ++ String.make(col, ' ') }; diff --git a/src/haz3lcore/zipper/ProjectorBase.re b/src/haz3lcore/zipper/ProjectorBase.re index 5abe811d76..0bba32d9fd 100644 --- a/src/haz3lcore/zipper/ProjectorBase.re +++ b/src/haz3lcore/zipper/ProjectorBase.re @@ -33,6 +33,7 @@ type info = { id: Id.t, syntax, ci: option(Info.t), + dyn: option(list(TestMap.instance_report)), }; /* To add a new projector: diff --git a/src/haz3lcore/zipper/projectors/FoldProj.re b/src/haz3lcore/zipper/projectors/FoldProj.re index 8f9665dea6..308714e69c 100644 --- a/src/haz3lcore/zipper/projectors/FoldProj.re +++ b/src/haz3lcore/zipper/projectors/FoldProj.re @@ -9,6 +9,17 @@ type t = { text: string, }; +/* Proof of concept value exposure. This isn't getting set right + after actions, only initially */ +let get_first_val = (rs: option(list(TestMap.instance_report))) => { + switch (rs) { + | Some(rs) => + List.map(((d: DHExp.t, _)) => d.term |> TermBase.Exp.show_term, rs) + |> String.concat(", ") + | _ => "Nein" + }; +}; + module M: Projector = { [@deriving (show({with_path: false}), sexp, yojson)] type model = t; @@ -20,9 +31,12 @@ module M: Projector = { let placeholder = (m, _) => Inline(m.text == "⋱" ? 2 : m.text |> String.length); let update = (m, _) => m; - let view = (m: model, ~info as _, ~local as _, ~parent) => + let view = (m: model, ~info, ~local as _, ~parent) => div( - ~attrs=[Attr.on_double_click(_ => parent(Remove))], + ~attrs=[ + Attr.on_double_click(_ => parent(Remove)), + Attr.title(get_first_val(info.dyn)), + ], [text(m.text)], ); let focus = _ => (); diff --git a/src/haz3lweb/app/common/ProjectorView.re b/src/haz3lweb/app/common/ProjectorView.re index 387ccc5cd7..3e3369f892 100644 --- a/src/haz3lweb/app/common/ProjectorView.re +++ b/src/haz3lweb/app/common/ProjectorView.re @@ -118,6 +118,7 @@ let setup_view = id: Id.t, ~cached_statics: CachedStatics.t, ~cached_syntax: Editor.CachedSyntax.t, + ~dyn_map, ~inject: Action.t => Ui_effect.t(unit), ~font_metrics, ~indication: option(Direction.t), @@ -126,7 +127,8 @@ let setup_view = let* p = Id.Map.find_opt(id, cached_syntax.projectors); let* syntax = Some(p.syntax); let ci = Id.Map.find_opt(id, cached_statics.info_map); - let info = {id, ci, syntax}; + let dyn = TestMap.lookup(id, dyn_map); + let info = {id, ci, dyn, syntax}; let+ measurement = Measured.find_pr_opt(p, cached_syntax.measured); let (module P) = to_module(p.kind); let parent = a => inject(Project(handle(id, a))); @@ -156,6 +158,7 @@ let all = z, ~cached_statics: CachedStatics.t, ~cached_syntax: Editor.CachedSyntax.t, + ~dyn_map, ~inject, ~font_metrics, ) => { @@ -172,6 +175,7 @@ let all = id, ~cached_statics, ~cached_syntax, + ~dyn_map, ~inject, ~font_metrics, ~indication, diff --git a/src/haz3lweb/app/editors/cell/CellEditor.re b/src/haz3lweb/app/editors/cell/CellEditor.re index f1fe88bc4b..a33753642b 100644 --- a/src/haz3lweb/app/editors/cell/CellEditor.re +++ b/src/haz3lweb/app/editors/cell/CellEditor.re @@ -56,7 +56,13 @@ module Update = { ) : Model.t => { let editor = - CodeEditable.Update.calculate(~settings, ~is_edited, ~stitch, editor); + CodeEditable.Update.calculate( + ~settings, + ~is_edited, + ~stitch, + ~dyn_map=TestMap.empty, //TODO(andrew): see below + editor, + ); let result = EvalResult.Update.calculate( ~settings, @@ -65,6 +71,20 @@ module Update = { editor |> CodeEditable.Model.get_statics, result, ); + //TODO(andrew): double-calcing editor... + let dyn_map = + switch (EvalResult.Model.make_test_report(result)) { + | Some(res) => res.test_map + | None => TestMap.empty + }; + let editor = + CodeEditable.Update.calculate( + ~settings, + ~is_edited, + ~stitch, + ~dyn_map, + editor, + ); {editor, result}; }; }; @@ -149,6 +169,11 @@ module View = { ~locked, model.result, ); + let dyn_map = + switch (EvalResult.Model.make_test_report(model.result)) { + | Some(res) => res.test_map + | None => TestMap.empty + }; div( ~attrs=[Attr.classes(["cell", locked ? "locked" : "unlocked"])], Option.to_list(caption) @@ -166,6 +191,7 @@ module View = { : (action => inject(MainEditor(action))), ~selected=selected == Some(MainEditor), ~overlays=overlays(model.editor.editor), + ~dyn_map, ~sort?, model.editor, ), diff --git a/src/haz3lweb/app/editors/code/Code.re b/src/haz3lweb/app/editors/code/Code.re index ee0cd2b564..10ba2801df 100644 --- a/src/haz3lweb/app/editors/code/Code.re +++ b/src/haz3lweb/app/editors/code/Code.re @@ -71,9 +71,15 @@ let of_secondary = } ); -let of_projector = (p, expected_sort, indent, info_map) => +let of_projector = (p, expected_sort, indent, info_map, dyn_map) => of_delim'(( - [Projector.placeholder(p, Id.Map.find_opt(p.id, info_map))], + [ + Projector.placeholder( + p, + Id.Map.find_opt(p.id, info_map), + TestMap.lookup(p.id, dyn_map), + ), + ], false, expected_sort, true, @@ -88,6 +94,7 @@ module Text = let map: Measured.t; let settings: Settings.Model.t; let info_map: Statics.Map.t; + let dyn_map: TestMap.t; }, ) => { let m = p => Measured.find_p(~msg="Text", p, M.map); @@ -118,7 +125,13 @@ module Text = | Secondary({content, _}) => of_secondary((content, M.settings.secondary_icons, m(p).last.col)) | Projector(p) => - of_projector(p, expected_sort, m(Projector(p)).origin.col, M.info_map) + of_projector( + p, + expected_sort, + m(Projector(p)).origin.col, + M.info_map, + M.dyn_map, + ) }; } and of_tile = (buffer_ids, expected_sort: Sort.t, t: Tile.t): list(Node.t) => { @@ -160,12 +173,13 @@ let rec holes = ); let simple_view = (~font_metrics, ~segment, ~settings: Settings.t): Node.t => { - let map = Measured.of_segment(segment, Id.Map.empty); + let map = Measured.of_segment(segment, Id.Map.empty, TestMap.empty); module Text = Text({ let map = map; let settings = settings; let info_map = Id.Map.empty; /* Assume this doesn't contain projectors */ + let dyn_map = TestMap.empty; /* Assume this doesn't contain projectors */ }); let holes = holes(~map, ~font_metrics, segment); div( diff --git a/src/haz3lweb/app/editors/code/CodeEditable.re b/src/haz3lweb/app/editors/code/CodeEditable.re index 9745fb3809..d2b7a10d1b 100644 --- a/src/haz3lweb/app/editors/code/CodeEditable.re +++ b/src/haz3lweb/app/editors/code/CodeEditable.re @@ -242,6 +242,7 @@ module View = { ~selected: bool, ~overlays: list(Node.t)=[], ~sort=?, + ~dyn_map, model: Model.t, ) => { let edit_decos = { @@ -250,6 +251,7 @@ module View = { let editor = model.editor; let globals = globals; let statics = model.statics; + let dynamics = dyn_map; }); Deco.editor(model.editor.state.zipper, selected); }; @@ -260,10 +262,11 @@ module View = { ~cached_syntax=model.editor.syntax, ~inject=x => inject(Perform(x)), ~font_metrics=globals.font_metrics, + ~dyn_map, ); let overlays = edit_decos @ overlays @ [projectors]; let code_view = - CodeWithStatics.View.view(~globals, ~overlays, ~sort?, model); + CodeWithStatics.View.view(~globals, ~overlays, ~dyn_map, ~sort?, model); let mousedown_overlay = selected && globals.mousedown ? [mousedown_overlay(~globals, ~inject=x => inject(Perform(x)))] diff --git a/src/haz3lweb/app/editors/code/CodeViewable.re b/src/haz3lweb/app/editors/code/CodeViewable.re index ab789bdce0..701a3026f1 100644 --- a/src/haz3lweb/app/editors/code/CodeViewable.re +++ b/src/haz3lweb/app/editors/code/CodeViewable.re @@ -13,6 +13,7 @@ let view = ~segment, ~holes, ~info_map, + ~dyn_map, ) : Node.t => { module Text = @@ -20,6 +21,7 @@ let view = let map = measured; let settings = globals.settings; let info_map = info_map; + let dyn_map = dyn_map; }); let code = Text.of_segment(buffer_ids, false, sort, segment); let holes = List.map(Code.of_hole(~measured, ~globals), holes); @@ -51,21 +53,36 @@ let view = // }; let view_segment = - (~globals: Globals.t, ~sort: Sort.t, ~info_map, segment: Segment.t) => { - let measured = Measured.of_segment(segment, info_map); + ( + ~globals: Globals.t, + ~sort: Sort.t, + ~info_map, + ~dyn_map, + segment: Segment.t, + ) => { + let measured = Measured.of_segment(segment, info_map, dyn_map); let buffer_ids = []; let holes = Segment.holes(segment); - view(~globals, ~sort, ~measured, ~buffer_ids, ~holes, ~segment, ~info_map); + view( + ~globals, + ~sort, + ~measured, + ~buffer_ids, + ~holes, + ~segment, + ~dyn_map, + ~info_map, + ); }; -let view_exp = (~globals: Globals.t, ~settings, exp: Exp.t) => { +let view_exp = (~dyn_map, ~globals: Globals.t, ~settings, exp: Exp.t) => { exp |> ExpToSegment.exp_to_segment(~settings) - |> view_segment(~globals, ~sort=Exp); + |> view_segment(~dyn_map, ~globals, ~sort=Exp); }; let view_typ = (~globals: Globals.t, ~settings, typ: Typ.t) => { typ |> ExpToSegment.typ_to_segment(~settings) - |> view_segment(~globals, ~sort=Typ); + |> view_segment(~dyn_map=TestMap.empty, ~globals, ~sort=Typ); }; diff --git a/src/haz3lweb/app/editors/code/CodeWithStatics.re b/src/haz3lweb/app/editors/code/CodeWithStatics.re index b183e3c861..b8ccb8e18b 100644 --- a/src/haz3lweb/app/editors/code/CodeWithStatics.re +++ b/src/haz3lweb/app/editors/code/CodeWithStatics.re @@ -52,11 +52,23 @@ module Update = { /* Calculates the statics for the editor. */ let calculate = - (~settings, ~is_edited, ~stitch, {editor, statics: _}: Model.t) + ( + ~settings, + ~is_edited, + ~stitch, + ~dyn_map, + {editor, statics: _}: Model.t, + ) : Model.t => { let statics = CachedStatics.init(~settings, ~stitch, editor.state.zipper); let editor = - Editor.Update.calculate(~settings, ~is_edited, statics, editor); + Editor.Update.calculate( + ~settings, + ~is_edited, + statics, + dyn_map, + editor, + ); {editor, statics}; }; }; @@ -66,7 +78,13 @@ module View = { type event; let view = - (~globals, ~overlays: list(Node.t)=[], ~sort=Sort.root, model: Model.t) => { + ( + ~globals, + ~overlays: list(Node.t)=[], + ~sort=Sort.root, + ~dyn_map, + model: Model.t, + ) => { let { statics: {info_map, _}, editor: @@ -86,6 +104,7 @@ module View = { ~segment, ~holes, ~info_map, + ~dyn_map, ); let statics_decos = { module Deco = @@ -93,6 +112,7 @@ module View = { let globals = globals; let editor = model.editor; let statics = model.statics; + let dynamics = dyn_map; }); Deco.statics(); }; diff --git a/src/haz3lweb/app/editors/decoration/BackpackView.re b/src/haz3lweb/app/editors/decoration/BackpackView.re index 1e8c93985e..d0f0ed3bca 100644 --- a/src/haz3lweb/app/editors/decoration/BackpackView.re +++ b/src/haz3lweb/app/editors/decoration/BackpackView.re @@ -4,7 +4,8 @@ open Haz3lcore; open Util; /* Assume this doesn't contain projectors */ -let measured_of = seg => Measured.of_segment(seg, Id.Map.empty); +let measured_of = seg => + Measured.of_segment(seg, Id.Map.empty, TestMap.empty); let text_view = (seg: Segment.t): list(Node.t) => { module Text = @@ -12,6 +13,7 @@ let text_view = (seg: Segment.t): list(Node.t) => { let map = measured_of(seg); let settings = Settings.Model.init; let info_map = Id.Map.empty; /* Assume this doesn't contain projectors */ + let dyn_map = TestMap.empty; /* Assume this doesn't contain projectors */ }); Text.of_segment([], true, Any, seg); }; diff --git a/src/haz3lweb/app/editors/decoration/Deco.re b/src/haz3lweb/app/editors/decoration/Deco.re index 56b019b6f0..d0a19f4e20 100644 --- a/src/haz3lweb/app/editors/decoration/Deco.re +++ b/src/haz3lweb/app/editors/decoration/Deco.re @@ -65,6 +65,7 @@ module HighlightSegment = M: { let measured: Measured.t; let info_map: Statics.Map.t; + let dyn_map: TestMap.t; let font_metrics: FontMetrics.t; }, ) => { @@ -122,7 +123,8 @@ module HighlightSegment = | None => failwith("Deco.of_projector: missing measurement") | Some(_m) => let ci = Id.Map.find_opt(p.id, M.info_map); - let token = Projector.placeholder(p, ci); + let dyn = TestMap.lookup(p.id, M.dyn_map); + let token = Projector.placeholder(p, ci, dyn); /* Handling this internal to ProjectorsView at the moment because the * commented-out strategy doesn't work well, since the inserted str8- * edged lines vertical edge placement doesn't account for whether @@ -182,6 +184,7 @@ module Deco = let globals: Globals.t; let editor: Editor.t; let statics: CachedStatics.t; + let dynamics: TestMap.t; }, ) => { let font_metrics = M.globals.font_metrics; @@ -218,6 +221,7 @@ module Deco = HighlightSegment({ let measured = M.editor.syntax.measured; let info_map = M.statics.info_map; + let dyn_map = M.dynamics; let font_metrics = font_metrics; }); diff --git a/src/haz3lweb/app/editors/mode/ExerciseMode.re b/src/haz3lweb/app/editors/mode/ExerciseMode.re index 0db58233ff..213f135bbd 100644 --- a/src/haz3lweb/app/editors/mode/ExerciseMode.re +++ b/src/haz3lweb/app/editors/mode/ExerciseMode.re @@ -191,7 +191,9 @@ module Update = { one of the editors is shown in two cells, so we arbitrarily choose which statics to take */ let editors: Exercise.p('a) = { - let calculate = Editor.Update.calculate(~settings, ~is_edited); + let dynamics = TestMap.empty; //TODO(andrew): dynamics for projs in exercise mode + let calculate = statics => + Editor.Update.calculate(~settings, statics, dynamics, ~is_edited); { title: model.editors.title, version: model.editors.version, diff --git a/src/haz3lweb/app/editors/result/EvalResult.re b/src/haz3lweb/app/editors/result/EvalResult.re index c8b59e2f3a..916bf92653 100644 --- a/src/haz3lweb/app/editors/result/EvalResult.re +++ b/src/haz3lweb/app/editors/result/EvalResult.re @@ -260,6 +260,7 @@ module Update = { ~settings, ~stitch=_ => exp, ~is_edited, + ~dyn_map=Haz3lcore.TestMap.empty, //TODO(andrew) editor, ) |> (x => (exp, x)) @@ -373,6 +374,7 @@ module View = { ~globals, ~selected, ~sort=Haz3lcore.Sort.root, + ~dyn_map=Haz3lcore.TestMap.empty, //TODO(andrew): this is just the result display, right? editor, ); let exn_view = @@ -528,6 +530,11 @@ module View = { // Just showing elaboration because evaluation is off: | EvalResults when globals.settings.core.elaborate => + let dyn_map = + switch (Model.test_results(model)) { + | Some(result) => result.test_map + | None => Haz3lcore.TestMap.empty + }; let result = [ text("Evaluation disabled, showing elaboration:"), switch (Model.get_elaboration(model)) { @@ -543,6 +550,7 @@ module View = { ~globals, ~sort=Exp, ~info_map=Haz3lcore.Id.Map.empty, + ~dyn_map, ) | None => text("No elaboration found") }, diff --git a/src/haz3lweb/app/editors/result/Stepper.re b/src/haz3lweb/app/editors/result/Stepper.re index e2abfc8af5..4a6fdee536 100644 --- a/src/haz3lweb/app/editors/result/Stepper.re +++ b/src/haz3lweb/app/editors/result/Stepper.re @@ -255,6 +255,7 @@ module Update = { CodeSelectable.Update.calculate( ~settings=settings |> Calc.get_value, ~is_edited=false, + ~dyn_map=TestMap.empty, ~stitch=x => x ), @@ -425,6 +426,7 @@ module View = { ~globals, ~overlays=[], ~selected=selection == Some(A(i + 1, ())), + ~dyn_map=TestMap.empty, ~inject= (x: StepperEditor.Update.t) => inject(StepperEditor(i + 1, x)), @@ -475,6 +477,7 @@ module View = { ~inject= (x: StepperEditor.Update.t) => inject(StepperEditor(current_n, x)), + ~dyn_map=TestMap.empty, ~signal= fun | TakeStep(x) => inject(Update.StepForward(x)) diff --git a/src/haz3lweb/app/editors/result/StepperEditor.re b/src/haz3lweb/app/editors/result/StepperEditor.re index b42b7bbc79..9e61b066eb 100644 --- a/src/haz3lweb/app/editors/result/StepperEditor.re +++ b/src/haz3lweb/app/editors/result/StepperEditor.re @@ -33,11 +33,18 @@ module Update = { ~settings, ~is_edited, ~stitch, + ~dyn_map, {editor, taken_steps, next_steps}: Model.t, ) : Model.t => { let editor = - CodeSelectable.Update.calculate(~settings, ~is_edited, ~stitch, editor); + CodeSelectable.Update.calculate( + ~settings, + ~is_edited, + ~stitch, + ~dyn_map, + editor, + ); {editor, taken_steps, next_steps}; }; }; @@ -62,6 +69,7 @@ module View = { ~signal: event => 'a, ~overlays=[], ~selected, + ~dyn_map, model: Model.t, ) => { let overlays = { @@ -70,6 +78,7 @@ module View = { let editor = model.editor.editor; let globals = globals; let statics = model.editor.statics; + let dynamics = dyn_map; }); overlays @ Deco.taken_steps(model.taken_steps) @@ -82,6 +91,7 @@ module View = { ~selected, ~globals, ~overlays, + ~dyn_map, model.editor, ); }; diff --git a/src/haz3lweb/app/explainthis/ExplainThis.re b/src/haz3lweb/app/explainthis/ExplainThis.re index 6d9422bef0..4823d1e430 100644 --- a/src/haz3lweb/app/explainthis/ExplainThis.re +++ b/src/haz3lweb/app/explainthis/ExplainThis.re @@ -236,6 +236,7 @@ let expander_deco = let editor = editor; let globals = globals; let statics = CachedStatics.empty; + let dynamics = TestMap.empty; }); switch (doc.expandable_id, List.length(options)) { | (None, _) @@ -278,6 +279,7 @@ let expander_deco = ~globals, ~sort=Exp, ~info_map=Id.Map.empty, + ~dyn_map=TestMap.empty, segment, ); let classes = @@ -496,12 +498,14 @@ let get_doc = editor, ); let statics = CachedStatics.empty; + let dynamics = TestMap.empty; let highlight_deco = { module Deco = Deco.Deco({ let editor = editor; let globals = {...globals, color_highlights: highlights}; let statics = statics; + let dynamics = dynamics; }); [Deco.color_highlights()]; }; @@ -509,6 +513,7 @@ let get_doc = CodeWithStatics.View.view( ~globals, ~overlays=highlight_deco @ [expander_deco], + ~dyn_map=dynamics, ~sort, {editor, statics}, );