From d64e739a86f4c5aa72c412223e887c537888eef8 Mon Sep 17 00:00:00 2001 From: disconcision Date: Sun, 15 Dec 2024 22:12:41 -0500 Subject: [PATCH] projectors live cleanup --- src/haz3lcore/statics/MakeTerm.re | 21 +- src/haz3lcore/statics/Statics.re | 2 +- src/haz3lcore/tiles/Piece.re | 10 - src/haz3lcore/zipper/projectors/ProbeProj.re | 36 +-- src/haz3lweb/app/explainthis/Example.re | 2 - src/haz3lweb/app/inspector/ProjectorPanel.re | 111 +++---- src/haz3lweb/www/style.css | 3 +- src/haz3lweb/www/style/editor.css | 4 +- src/haz3lweb/www/style/projectors-panel.css | 29 -- src/haz3lweb/www/style/projectors.css | 310 ------------------- src/util/JsUtil.re | 8 +- src/util/ListUtil.re | 2 +- 12 files changed, 60 insertions(+), 478 deletions(-) delete mode 100644 src/haz3lweb/www/style/projectors-panel.css delete mode 100644 src/haz3lweb/www/style/projectors.css diff --git a/src/haz3lcore/statics/MakeTerm.re b/src/haz3lcore/statics/MakeTerm.re index 38c00f5951..85e5b069c6 100644 --- a/src/haz3lcore/statics/MakeTerm.re +++ b/src/haz3lcore/statics/MakeTerm.re @@ -123,16 +123,9 @@ let return = (wrap, ids, tm) => { let projectors: ref(Id.Map.t(Piece.projector)) = ref(Id.Map.empty); /* Strip a projector from a segment and log it in the map */ -let log_projectors = (seg: Segment.t): Segment.t => - List.map( - fun - | Piece.Projector(pr) => { - projectors := Id.Map.add(pr.id, pr, projectors^); - Piece.Projector(pr); - } - | x => x, - seg, - ); +let log_projector = (pr: Base.projector): unit => { + projectors := Id.Map.add(pr.id, pr, projectors^); +}; let parse_sum_term: UTyp.t => ConstructorMap.variant(UTyp.t) = fun @@ -367,7 +360,7 @@ and pat_term: unsorted => (UPat.term, list(Id.t)) = { | ([t], []) when t != " " && !Form.is_explicit_hole(t) => Invalid(t) | (["(", ")"], [Pat(body)]) => Parens(body) - | (label, [Pat(body)]) when is_probe_wrap(label) => Parens(body) + | (label, [Pat(body)]) when is_probe_wrap(label) => body.term | (["[", "]"], [Pat(body)]) => switch (body) { | {term: Tuple(ps), _} => ListLit(ps) @@ -428,7 +421,7 @@ and typ_term: unsorted => (UTyp.term, list(Id.t)) = { | (["String"], []) => String | ([t], []) when Form.is_typ_var(t) => Var(t) | (["(", ")"], [Typ(body)]) => Parens(body) - | (label, [Typ(body)]) when is_probe_wrap(label) => Parens(body) + | (label, [Typ(body)]) when is_probe_wrap(label) => body.term | (["[", "]"], [Typ(body)]) => List(body) | ([t], []) when t != " " && !Form.is_explicit_hole(t) => Unknown(Hole(Invalid(t))) @@ -538,12 +531,12 @@ and rul = (unsorted: unsorted): Rul.t => { and unsorted = (skel: Skel.t, seg: Segment.t): unsorted => { /* Remove projectors. We do this here as opposed to removing * them in an external call to save a whole-syntax pass. */ - let _ = log_projectors(seg); let tile_kids = (p: Piece.t): list(Term.Any.t) => switch (p) { | Secondary(_) | Grout(_) => [] - | Projector({syntax, id: _, _}) => + | Projector({syntax, id: _, _} as pr) => + let _ = log_projector(pr); let sort = Piece.sort(syntax) |> fst; [go_s(sort, Segment.skel([syntax]), [syntax])]; | Tile({mold, shards, children, _}) => diff --git a/src/haz3lcore/statics/Statics.re b/src/haz3lcore/statics/Statics.re index f20e3f8e57..9d9abde74b 100644 --- a/src/haz3lcore/statics/Statics.re +++ b/src/haz3lcore/statics/Statics.re @@ -26,7 +26,7 @@ itself is dedicated to the piping necessary to (A) introduce and (B) propagate the necessary information through the syntax tree. - */ + */ module Info = Info; diff --git a/src/haz3lcore/tiles/Piece.re b/src/haz3lcore/tiles/Piece.re index 96b02e1004..fc6207a979 100644 --- a/src/haz3lcore/tiles/Piece.re +++ b/src/haz3lcore/tiles/Piece.re @@ -186,13 +186,3 @@ let is_term = (p: t) => | Secondary(_) => false // debatable | _ => false }; - -let mk_tile_id: (Id.t, Form.t, list(list(t))) => t = - (id, form, children) => - Tile({ - id, - label: form.label, - mold: form.mold, - shards: List.mapi((i, _) => i, form.label), - children, - }); diff --git a/src/haz3lcore/zipper/projectors/ProbeProj.re b/src/haz3lcore/zipper/projectors/ProbeProj.re index e846755dfb..0ce589301d 100644 --- a/src/haz3lcore/zipper/projectors/ProbeProj.re +++ b/src/haz3lcore/zipper/projectors/ProbeProj.re @@ -4,25 +4,6 @@ open Virtual_dom.Vdom; open Node; open Js_of_ocaml; -//let _ = Zipper.base_point; //not cyclical -//let _ = Editor.show; //cyclical - -/* Plan for extended dynamics: - in principle we could track: - - prev 'stack frame': id of prev expr that began execution? - - env (or just the part of the env that's relevant to the current expr) - aka the co-ctx - - */ - -/* Plan for selectable (editable as well maybe): - - selectable: - create own mini version of editor, use it as model - update fn updates model after applying mini editor action - hopefully can use same actions - */ - [@deriving (show({with_path: false}), sexp, yojson)] type t = { [@default "⋱"] @@ -96,22 +77,15 @@ let get_goal = (utility: utility, e: Js.t(Dom_html.mouseEvent)) => let resizable_val = (~resizable=false, model, utility, local, pi: Dynamics.Probe.Info.t) => { let val_pointerdown = (e: Js.t(Dom_html.pointerEvent)) => { - // print_endline("pointerdown"); let target = e##.target |> Js.Opt.get(_, _ => failwith("no target")); JsUtil.setPointerCapture(target, e##.pointerId) |> ignore; mousedown := Some(target); - // if (last_target^ == [target] && !Js.to_bool(e##.shiftKey)) { - // env_cursor := []; - // last_target := []; - // } else { env_cursor := Probe.env_stack(pi.stack); last_target := [target]; - // }; Effect.Ignore; }; let val_pointerup = (e: Js.t(Dom_html.pointerEvent)) => { - // print_endline("pointerup"); switch (mousedown^) { | Some(target) => JsUtil.releasePointerCapture(target, e##.pointerId) |> ignore @@ -128,10 +102,7 @@ let resizable_val = /* Ideally we could just use hasPointerCapture... */ let goal = get_goal(utility, e); local(ChangeLength(goal.col)); - // print_endline("mousemove: resizing"); - | _ => - // print_endline("mousemove: not resizing"); - Effect.Ignore + | _ => Effect.Ignore }; div( @@ -145,10 +116,7 @@ let resizable_val = Attr.on_pointerup(val_pointerup), Attr.on_mousemove(val_mousemove), ], - [ - seg_view(utility, model.len, pi.value), - //, text(stack(pi.stack)) - ], + [seg_view(utility, model.len, pi.value)], ); }; diff --git a/src/haz3lweb/app/explainthis/Example.re b/src/haz3lweb/app/explainthis/Example.re index 3941063a23..9408167cf6 100644 --- a/src/haz3lweb/app/explainthis/Example.re +++ b/src/haz3lweb/app/explainthis/Example.re @@ -22,8 +22,6 @@ let int = n => mk_monotile(Form.mk_atomic(Exp, n)); let exp = v => mk_monotile(Form.mk_atomic(Exp, v)); let pat = v => mk_monotile(Form.mk_atomic(Pat, v)); let mk_parens_exp = mk_tile(Form.get("parens_exp")); -let mk_probe = (e: list(Piece.t)) => - mk_tile(Form.mk(Form.ii, ["@@", "@@"], Mold.mk_op(Exp, [Exp])), [e]); let mk_fun = mk_tile(Form.get("fun_")); let mk_fun_ancestor = mk_ancestor(Form.get("fun_")); let mk_parens_ancestor = mk_ancestor(Form.get("parens_exp")); diff --git a/src/haz3lweb/app/inspector/ProjectorPanel.re b/src/haz3lweb/app/inspector/ProjectorPanel.re index f52e1a4864..271363b4fe 100644 --- a/src/haz3lweb/app/inspector/ProjectorPanel.re +++ b/src/haz3lweb/app/inspector/ProjectorPanel.re @@ -5,12 +5,7 @@ open Projector; open Util.OptUtil.Syntax; open Util.Web; -/* The projector selection panel on the right of the bottom bar */ -let option_view = (_name, n) => - option([ - //~attrs=n == name ? [Attr.create("selected", "selected")] : [], - text(n), - ]); +// The projector selection panel on the right of the bottom bar /* Decide which projectors are applicable based on the cursor info. * This is slightly inside-out as elsewhere it depends on the underlying @@ -100,74 +95,56 @@ let might_project: Cursor.cursor(Editors.Update.t) => bool = } }; -let currently_selected = editor => - option_view( - switch (kind(editor)) { - | None => "fold" - | Some(k) => ProjectorView.name(k) - }, - ); - -let currently_selected_str = (editor, _): string => - switch (kind(editor)) { - | None => "fold" - | Some(k) => ProjectorView.name(k) - }; +let lift = (str, strs) => List.cons(str, List.filter((!=)(str), strs)); -let currently_selected_str_opt = (editor, _): option(string) => - switch (kind(editor)) { - | None => None - | Some(k) => Some(ProjectorView.name(k)) +/* The string names of all projectors applicable to the currently + * indicated syntax, with the currently applied projection (if any) + * lifted to the top of the list */ +let applicable_projector_strings = (cursor: Cursor.cursor(Editors.Update.t)) => { + let strs = + applicable_projectors(cursor.info) |> List.map(ProjectorView.name); + switch (kind(cursor.editor)) { + | None => strs + | Some(k) => lift(ProjectorView.name(k), strs) }; +}; -let view = (~inject, cursor: Cursor.cursor(Editors.Update.t)) => { - let applicable_projectors = applicable_projectors(cursor.info); - let should_show = might_project(cursor) && applicable_projectors != []; - //TODO(andrew): cleanup - // print_endline("currentrly: " ++ currently_selected_str(cursor.editor, ())); - let applicable_projector_strings = - (might_project(cursor) ? applicable_projectors : [Fold]) - |> List.map(ProjectorView.name); +/* A selection input for contetually applicable projectors */ +let select_view = + ( + ~inject: Action.project => Ui_effect.t(unit), + cursor: Cursor.cursor(Editors.Update.t), + ) => { let applicable_projector_strings = - switch (currently_selected_str_opt(cursor.editor, ())) { - | None => applicable_projector_strings - | Some(guy) => - List.cons( - guy, - List.filter(x => x != guy, applicable_projector_strings), - ) - }; + might_project(cursor) ? applicable_projector_strings(cursor) : []; let value = - switch (kind(cursor.editor)) { - | Some(k) => ProjectorView.name(k) - | None => - applicable_projector_strings - //|> List.map(currently_selected_str(cursor.editor)) - |> List.hd + switch (applicable_projector_strings) { + | [] => "" + | [hd, ..._] => hd }; - // print_endline("value: " ++ value); - let select_view = - Node.select( - ~attrs=[ - Attr.on_change((_, name) => - inject(Action.SetIndicated(ProjectorView.of_name(name))) - ), - Attr.string_property("value", value), - ], - applicable_projector_strings - |> List.map(option_view("garbageTODO(andrew)")), - //|> List.map(currently_selected(cursor.editor)), - ); - let toggle_view = - toggle_view( - ~inject, - cursor.info, - id(cursor.editor), - kind(cursor.editor) != None, - might_project(cursor), - ); + Node.select( + ~attrs=[ + Attr.on_change((_, name) => + inject(SetIndicated(ProjectorView.of_name(name))) + ), + Attr.string_property("value", value), + ], + applicable_projector_strings |> List.map(n => option([text(n)])), + ); +}; + +let toggle_view = (~inject, cursor: Cursor.cursor(Editors.Update.t)) => + toggle_view( + ~inject, + cursor.info, + id(cursor.editor), + kind(cursor.editor) != None, + might_project(cursor), + ); + +let view = (~inject, cursor: Cursor.cursor(Editors.Update.t)) => { div( ~attrs=[Attr.id("projectors")], - (should_show ? [select_view] : []) @ [toggle_view], + [select_view(~inject, cursor)] @ [toggle_view(~inject, cursor)], ); }; diff --git a/src/haz3lweb/www/style.css b/src/haz3lweb/www/style.css index d70e70a422..e38e08bfab 100644 --- a/src/haz3lweb/www/style.css +++ b/src/haz3lweb/www/style.css @@ -3,11 +3,10 @@ @import "style/animations.css"; @import "style/loading.css"; @import "style/editor.css"; -@import "style/projectors.css"; +@import "style/projectors/base.css"; @import "style/nut-menu.css"; @import "style/cursor-inspector.css"; @import "style/type-display.css"; -@import "style/projectors-panel.css"; @import "style/explainthis.css"; @import "style/exercise-mode.css"; @import "style/cell.css"; diff --git a/src/haz3lweb/www/style/editor.css b/src/haz3lweb/www/style/editor.css index a01b275992..767fa6196e 100644 --- a/src/haz3lweb/www/style/editor.css +++ b/src/haz3lweb/www/style/editor.css @@ -21,7 +21,9 @@ /* This is a hack to compensating for default linebreak handling * preventing a trailing linebreak in code editors from leaving a * trailing blank line, as per https://stackoverflow.com/questions/43492826/. -* The mysterious chracter below is a zero-width space */ +* The mysterious chracter below is a zero-width space, used here +* to avoid inserting an extraneous whitespace context for inline +* syntax views, e.g. type views in the cursor inspector */ .code-text:after { content: "​"; } diff --git a/src/haz3lweb/www/style/projectors-panel.css b/src/haz3lweb/www/style/projectors-panel.css deleted file mode 100644 index 77c184bf59..0000000000 --- a/src/haz3lweb/www/style/projectors-panel.css +++ /dev/null @@ -1,29 +0,0 @@ -/* PROJECTORS PANEL */ - -#projectors { - display: flex; - gap: 0.75em; - align-items: center; - padding-left: 0.75em; - padding-right: 0.75em; - white-space: nowrap; - border-radius: 1.1em 0 0 0; - outline: 0.3px solid var(--BR2); -} - -#projectors img { - width: 0.7em; -} - -#projectors option { - font-size: 1em; -} - -#projectors .toggle-switch { - display: flex; - align-items: center; -} - -#projectors .toggle-switch.inactive { - opacity: 40%; -} diff --git a/src/haz3lweb/www/style/projectors.css b/src/haz3lweb/www/style/projectors.css deleted file mode 100644 index bfcfa12cee..0000000000 --- a/src/haz3lweb/www/style/projectors.css +++ /dev/null @@ -1,310 +0,0 @@ -/* PROJECTORS */ - -/* Turn off caret when a block projector is focused */ -#caret:has(~ .projectors .projector.block *:focus) { - display: none; -} - -/* Default projector styles */ - -.projector { - position: absolute; - display: flex; - justify-content: center; - align-items: center; - color: var(--BR2); -} -.projector > *:not(svg) { - z-index: var(--projector-z); -} -.projector > svg { - z-index: var(--projector-backing-z); - fill: var(--shard_projector); -} -.projector.block > svg { - stroke-width: 0.5px; - stroke: var(--BR2); -} -.projector.indicated > svg { - fill: var(--shard-caret-exp); -} -.projector > svg > path { - vector-effect: non-scaling-stroke; -} -.projector.block.selected > svg > path { - vector-effect: non-scaling-stroke; - stroke: var(--Y3); -} -.projector.selected > svg, -.projector.selected.indicated > svg, -.projector.block.selected.indicated > svg { - fill: var(--shard-selected); -} - -/* PROJECTOR: FOLD */ - -.projector.fold:hover, -.projector.indicated.fold { - color: --var(BLACK); -} -.projector.fold { - cursor: pointer; - font-family: var(--code-font); -} - -.result .projector.fold { - cursor: default; -} - -/* PROJECTOR: INFO */ - -.projector.type .type { - color: var(--token-typ); -} -.projector.type { - cursor: pointer; -} -.projector.type .info { - display: flex; -} -.projector.type:hover { - color: var(--BLACK); -} - -/* PROJECTOR: CHECKBOX */ - -.projector.check input { - margin: 0; - filter: sepia(1); - cursor: pointer; - outline: none; -} -.projector.check:not(.indicated):not(:hover) > svg { - fill: var(--NONE); -} - -/* PROJECTOR: SLIDERS (INT & FLOAT) */ - -.projector.slider input, -.projector.sliderf input { - margin: 0; - filter: sepia(1); - cursor: pointer; - outline: none; - width: 90%; -} -.projector.slider:not(.indicated):not(:hover) > svg, -.projector.sliderf:not(.indicated):not(:hover) > svg { - fill: var(--NONE); -} - -/* PROJECTOR: TEXTAREA */ - -.projector.text { - cursor: default; -} - -.projector.text .wrapper { - height: 100%; - width: 100%; - border-radius: 0.1em; -} - -.projector.text.indicated .cols, -.projector.text:has(textarea:focus) .cols { - color: var(--R1); -} - -.projector.text.indicated > svg { - fill: var(--textarea-indicated); -} - -.projector.text .cols { - height: 100%; - margin-left: 2px; - margin-right: 2px; - display: flex; - border-radius: 0 0.1em 0.1em 0.1em; - color: var(--SAND); - background: repeating-linear-gradient( - var(--NONE), - var(--NONE) 1.41em, - var(--textarea-h-stripe) 1.41em, - var(--textarea-h-stripe) 1.47em /* line-height */ - ); -} - -.projector.text.selected .cols { - background: repeating-linear-gradient( - var(--NONE), - var(--NONE) 1.41em, - var(--textarea-h-strip-selected) 1.41em, - var(--textarea-h-strip-selected) 1.47em /* line-height */ - ); -} -.projector.text.selected > svg { - z-index: 9; -} - -.projector.text textarea { - outline: none; - resize: none; - width: 100%; - caret-color: var(--caret-color); - padding: 0; - margin: 0; - margin-left: -2px; - line-height: var(--line-height); - font-family: var(--code-font); - font-size: inherit; - border: none; - color: var(--textarea-text); - background: none; - box-shadow: inset 1px 0 0 var(--textarea-v-stripe); - overflow: hidden; /* hack: scrolls in chrome without this? */ -} - -.projector.text textarea::selection { - color: var(--BLACK); - background-color: var(--shard-selected); -} - -/* Probe */ - -.projector.probe { - font-family: var(--code-font); - font-size: var(--base-font-size); - color: var(--STONE); -} - -.projector.probe .main { - display: flex; - flex-direction: row; - gap: 0.4em; - cursor: pointer; - align-items: center; -} - -@keyframes rotate { - to { - transform: rotate(360deg); - } -} - -.projector.probe .live-offside:empty + * .icon { - /* opacity: 30%; */ - animation: rotate 5s linear infinite; -} - -.projector.probe > svg { - fill: #c7e6c6; - filter: drop-shadow(0.7px 0.7px 0px green); -} - -.projector.probe.indicated > svg { - fill: var(--G0); - /* fill: #a4d7a2; */ -} - -.projector.probe .num-closures { - position: absolute; - right: -0.5em; - top: -0.3em; - transform-origin: top right; - scale: 0.6; - color: oklch(1 0 0); - font-family: var(--ui-font); - display: flex; - justify-content: center; - background-color: var(--G0); - border-radius: 2em; - font-size: 0.7em; - padding: 0.3em; - min-width: 1em; - z-index: var(--code-emblems-z); -} -.projector.probe.selected .num-closures { - background-color: var(--Y1); -} - -.projector.probe .live-offside { - display: flex; - flex-direction: row; - position: absolute; - left: 10em; - gap: 0.15em; -} - -.projector.probe .live-offside:empty { - display: none; -} - -.projector.probe .val-resize { - cursor: pointer; -} - -.projector.probe .val-resize .code-text { - background-color: #c7e6c6; - border-radius: 0.4em 0.1em 0.1em 0.1em; - filter: drop-shadow(0.7px 0.7px 0px green); -} -.projector.probe .closure:first-child .val-resize:hover .code-text { - cursor: col-resize; -} -.projector.probe .val-resize.cursor .code-text { - outline: 1.6px solid var(--G0); - outline-style: dotted; - filter: none; - opacity: 100%; -} - -.projector.probe .val-resize .code-text { - opacity: 40%; -} -.projector.probe .val-resize:not(.cursor) .code-text .token { - filter: saturate(0); -} -/* .projector.probe .val-resize.cursor .code-text { - opacity: 80%; -} */ -.projector.probe.indicated .val-resize .code-text { - opacity: 60%; -} -.projector.probe.indicated .main { - color: white; -} -.projector.probe.indicated .val-resize.cursor .code-text { - opacity: 100%; - /* outline: 1px solid var(--GB1); */ - outline: 2.8px solid oklch(0.7 0.15 150.31); -} -.projector.probe.indicated .closure:hover .live-env { - display: block; -} -.projector.probe.indicated .closure.cursor .live-env:empty { - display: none; -} -/* .projector.probe .closure:hover .live-env { - display: block; -} */ -.projector.probe .closure:hover .live-env:empty { - display: none; -} - -.projector.probe .live-env { - background-color: var(--T3); - border-radius: 0 0.2em 0.2em 0.2em; - padding: 0.2em; - display: none; - position: absolute; - top: 1.5em; - z-index: var(--code-hovers-z); -} - -.projector.probe .live-env .live-env-entry { - display: flex; - flex-direction: row; - gap: 0.3em; - align-items: baseline; - color: var(--GB0); -} diff --git a/src/util/JsUtil.re b/src/util/JsUtil.re index 4002e92596..e84c34b69e 100644 --- a/src/util/JsUtil.re +++ b/src/util/JsUtil.re @@ -205,13 +205,7 @@ let releasePointerCapture = (e: Js.t(Dom_html.element), pointerId: int) => [|Js.Unsafe.inject(pointerId)|], ); -// let hasPointerCapture = (e: Js.t(Dom_html.element), pointerId: int): bool => -// Js.Unsafe.meth_call( -// e, -// "hasPointerCapture", -// [|Js.Unsafe.inject(pointerId)|], -// ); - +// TODO: Figure out why this doesn't work // let on_pointermove = // (handler: Js.t(Dom_html.pointerEvent) => Effect.t(unit)): Attr.t => // Virtual_dom.Vdom.Attr.property("onpointermove", Js.Unsafe.inject(handler)); diff --git a/src/util/ListUtil.re b/src/util/ListUtil.re index e6a5c6a6c5..300d280b3b 100644 --- a/src/util/ListUtil.re +++ b/src/util/ListUtil.re @@ -593,7 +593,7 @@ let minimum = (f: 'a => int, xs: list('a)): option('a) => }; /* Given two lists, return their maximum common suffix */ -let max_common_suffix = (a: list('a), b: list('a)) => { +let max_common_suffix = (a: list('a), b: list('a)): list('a) => { let rec loop = (a, b, acc) => switch (a, b) { | ([], _)