From ba8f398d69ad648dbf945ccbf2f3d059304dc3fc Mon Sep 17 00:00:00 2001 From: Alexander Bandukwala <7h3kk1d@gmail.com> Date: Mon, 4 Nov 2024 17:27:35 -0500 Subject: [PATCH] in progress --- src/haz3lcore/dune | 2 +- src/haz3lcore/tiles/Base.re | 3 +- src/haz3lcore/zipper/Projector.re | 1 + .../zipper/projectors/MarkdownProj.re | 118 ++++++++++++++++++ src/haz3lweb/view/ProjectorView.re | 4 +- 5 files changed, 125 insertions(+), 3 deletions(-) create mode 100644 src/haz3lcore/zipper/projectors/MarkdownProj.re diff --git a/src/haz3lcore/dune b/src/haz3lcore/dune index a0d9770816..c03139ea98 100644 --- a/src/haz3lcore/dune +++ b/src/haz3lcore/dune @@ -2,7 +2,7 @@ (library (name haz3lcore) - (libraries util sexplib unionFind uuidm virtual_dom yojson core) + (libraries util sexplib unionFind uuidm virtual_dom yojson core omd) (js_of_ocaml) (instrumentation (backend bisect_ppx)) diff --git a/src/haz3lcore/tiles/Base.re b/src/haz3lcore/tiles/Base.re index 8c127d83ba..c63accce6d 100644 --- a/src/haz3lcore/tiles/Base.re +++ b/src/haz3lcore/tiles/Base.re @@ -10,7 +10,8 @@ type kind = | Checkbox | Slider | SliderF - | TextArea; + | TextArea + | Markdown; [@deriving (show({with_path: false}), sexp, yojson)] type segment = list(piece) diff --git a/src/haz3lcore/zipper/Projector.re b/src/haz3lcore/zipper/Projector.re index 82b036b821..4112d45466 100644 --- a/src/haz3lcore/zipper/Projector.re +++ b/src/haz3lcore/zipper/Projector.re @@ -12,6 +12,7 @@ let to_module = (kind: Base.kind): (module Cooked) => | SliderF => (module Cook(SliderFProj.M)) | Checkbox => (module Cook(CheckboxProj.M)) | TextArea => (module Cook(TextAreaProj.M)) + | Markdown => (module Cook(MarkdownProj.M)) }; let shape = (p: Base.projector, info: info): shape => { diff --git a/src/haz3lcore/zipper/projectors/MarkdownProj.re b/src/haz3lcore/zipper/projectors/MarkdownProj.re new file mode 100644 index 0000000000..41f4fdccac --- /dev/null +++ b/src/haz3lcore/zipper/projectors/MarkdownProj.re @@ -0,0 +1,118 @@ +open Util; +open Virtual_dom.Vdom; +open ProjectorBase; + +let of_id = (id: Id.t) => + "id" ++ (id |> Id.to_string |> String.sub(_, 0, 8)); + +let of_mono = (syntax: Piece.t): option(string) => + switch (syntax) { + | Tile({label: [l], _}) => Some(StringUtil.unescape_linebreaks(l)) + | _ => None + }; + +let mk_mono = (sort: Sort.t, string: string): Piece.t => + string + |> StringUtil.escape_linebreaks + |> Form.mk_atomic(sort) + |> Piece.mk_tile(_, []); + +let get = (piece: Piece.t): string => + switch (piece |> of_mono) { + | None => failwith("TextArea: not string literal") + | Some(s) => s + }; + +let put = (s: string): Piece.t => s |> mk_mono(Exp); + +let put = (str: string): external_action => + SetSyntax(str |> Form.string_quote |> put); + +let is_last_pos = id => + Web.TextArea.caret_at_end(Web.TextArea.get(of_id(id))); +let is_first_pos = id => + Web.TextArea.caret_at_start(Web.TextArea.get(of_id(id))); + +let key_handler = (id, ~parent, evt) => { + open Effect; + let key = Key.mk(KeyDown, evt); + + switch (key.key) { + | D("ArrowRight" | "ArrowDown") when is_last_pos(id) => + JsUtil.get_elem_by_id(of_id(id))##blur; + Many([parent(Escape(Right)), Stop_propagation]); + | D("ArrowLeft" | "ArrowUp") when is_first_pos(id) => + JsUtil.get_elem_by_id(of_id(id))##blur; + Many([parent(Escape(Left)), Stop_propagation]); + /* Defer to parent editor undo for now */ + | D("z" | "Z" | "y" | "Y") when Key.ctrl_held(evt) || Key.meta_held(evt) => + Many([Prevent_default]) + | D("z" | "Z") + when Key.shift_held(evt) && (Key.ctrl_held(evt) || Key.meta_held(evt)) => + Many([Prevent_default]) + | D("\"") => + /* Hide quotes from both the textarea and parent editor */ + Many([Prevent_default, Stop_propagation]) + | _ => Stop_propagation + }; +}; + +let safe_html_to_node = (html_string: string): Node.t => + Node.div(~attrs=[Attr.create("innerHTML", html_string)], []); +let textarea = + (id, ~parent: external_action => Ui_effect.t(unit), text: string) => { + let foo = Omd.of_string(text); + let bar = Omd.to_html(foo); + // Node.innerHtml(bar); + let foo = safe_html_to_node(bar); + let foo = + Node.inner_html( + ~attrs=[Attr.id(of_id(id))], + ~this_html_is_sanitized_and_is_totally_safe_trust_me=bar, // ;) + ~tag="div", + ); + foo(); +}; + +let view = (_, ~info, ~local as _, ~parent) => { + let text = info.syntax |> get |> Form.strip_quotes; + Node.div( + ~attrs=[Attr.classes(["wrapper"])], + [ + Node.div( + ~attrs=[Attr.classes(["cols", "code"])], + [Node.text("ยท")] @ [textarea(info.id, ~parent, text)], + ), + ], + ); +}; + +module M: Projector = { + [@deriving (show({with_path: false}), sexp, yojson)] + type model = unit; + [@deriving (show({with_path: false}), sexp, yojson)] + type action = unit; + let init = (); + let can_project = _ => true; //TODO(andrew): restrict somehow + let can_focus = true; + let placeholder = (_, info) => { + let str = Form.strip_quotes(get(info.syntax)); + Block({ + row: StringUtil.num_lines(str), + /* +2 for left and right padding */ + col: 2 + StringUtil.max_line_width(str), + }); + }; + let update = (model, _) => model; + let view = view; + let focus = ((id: Id.t, d: option(Direction.t))) => { + JsUtil.get_elem_by_id(of_id(id))##focus; + switch (d) { + | None => () + | Some(Left) => + Web.TextArea.set_caret_to_start(Web.TextArea.get(of_id(id))) + | Some(Right) => + Web.TextArea.set_caret_to_end(Web.TextArea.get(of_id(id))) + }; + }; +}; diff --git a/src/haz3lweb/view/ProjectorView.re b/src/haz3lweb/view/ProjectorView.re index 1669ff136d..706061823e 100644 --- a/src/haz3lweb/view/ProjectorView.re +++ b/src/haz3lweb/view/ProjectorView.re @@ -20,6 +20,7 @@ let name = (p: kind): string => | Slider => "slider" | SliderF => "sliderf" | TextArea => "text" + | Markdown => "markdown" }; /* This must be updated and kept 1-to-1 with the above @@ -33,6 +34,7 @@ let of_name = (p: string): kind => | "slider" => Slider | "sliderf" => SliderF | "text" => TextArea + | "markdown" => Markdown | _ => failwith("Unknown projector kind") }; @@ -214,7 +216,7 @@ module Panel = { | Exp(Float) | Pat(Float) => [SliderF] | Exp(String) - | Pat(String) => [TextArea] + | Pat(String) => [TextArea, Markdown] | _ => [] } )