Write out steps

src/language/CoreSettings.re

@@ -16,6 +16,7 @@ module Evaluation = {
     show_settings: bool,
     show_hidden_steps: bool,
     enable_proof: bool,
+    write_out_steps: bool,
   };
 
   let init = {
@@ -31,6 +32,7 @@ module Evaluation = {
     show_settings: false,
     show_hidden_steps: false,
     enable_proof: false,
+    write_out_steps: false,
   };
 };
 

src/web/Settings.re

@@ -38,6 +38,7 @@ module Model = {
         stepper_history: false,
         show_settings: false,
         show_hidden_steps: false,
+        write_out_steps: false,
         enable_proof: false,
       },
     },
@@ -103,6 +104,7 @@ module Update = {
     | ShowLookups
     | ShowFilters
     | ShowSettings
+    | WriteOutSteps
     | ShowHiddenSteps;
 
   [@deriving (show({with_path: false}), sexp, yojson)]
@@ -240,6 +242,10 @@ module Update = {
               ...evaluation,
               show_hidden_steps: !evaluation.show_hidden_steps,
             }
+          | WriteOutSteps => {
+              ...evaluation,
+              write_out_steps: !evaluation.write_out_steps,
+            }
           };
         {
           ...settings,

src/web/app/editors/cell/CellEditor.re

@@ -247,7 +247,7 @@ module View = {
             locked
               ? _ => Ui_effect.Ignore
               : (action => inject(MainEditor(action))),
-          ~selected=selected == Some(MainEditor),
+          ~selected=selected == Some(MainEditor) ? Yes : No,
           ~overlays=overlays(model.editor.editor),
           ~dynamics=EvalResult.Model.dynamics(model.result),
           model.editor,

src/web/app/editors/code/CodeEditable.re

@@ -229,7 +229,7 @@ module View = {
 
   let deco =
       (
-        ~expand_selection=false,
+        ~expand_selection,
         ~syntax: CachedSyntax.t,
         ~globals: Globals.t,
         z: Zipper.t,
@@ -263,65 +263,86 @@ module View = {
     ),
   ];
 
+  type selected =
+    | Yes
+    | JustHighlight
+    | No;
+
   let view =
       (
         ~globals: Globals.t,
         ~signal: event => Ui_effect.t(unit),
         ~inject: Update.t => Ui_effect.t(unit),
-        ~selected: bool,
+        ~selected: selected,
         ~overlays: list(Node.t)=[],
         ~dynamics: Language.Dynamics.Map.t,
-        ~expand_selection=?,
+        ~expand_selection=false,
         model: Model.t,
       ) => {
     /* Sync document-level click listener for closing context menu */
     ContextMenuListener.sync(
-      selected && Model.context_menu_is_open(model),
+      selected == Yes && Model.context_menu_is_open(model),
       inject(ContextMenu(ContextMenu.Model.Close)),
     );
     let edit_decos =
-      selected
-        ? deco(
-            ~expand_selection?,
+      switch (selected) {
+      | Yes =>
+        deco(
+          ~expand_selection,
+          ~syntax=model.editor.syntax,
+          ~globals,
+          model.editor.state.zipper,
+        )
+        @ [
+          Arms.Refractors.all(
+            ~font_metrics=globals.font_metrics,
             ~syntax=model.editor.syntax,
-            ~globals,
+            ~dynamics,
             model.editor.state.zipper,
-          )
-          @ [
-            Arms.Refractors.all(
-              ~font_metrics=globals.font_metrics,
-              ~syntax=model.editor.syntax,
-              ~dynamics,
-              model.editor.state.zipper,
-            ),
-          ]
-          @ (
-            switch (model.context_menu) {
-            | Some(selected_index) => [
-                /* Backdrop for scroll-close. Click handling is done via
-                   ContextMenuListener's document-level event listener. */
-                Node.div(
-                  ~attrs=[
-                    Attr.classes(["context-menu-backdrop"]),
-                    Attr.on_wheel(_ =>
-                      inject(ContextMenu(ContextMenu.Model.Close))
-                    ),
-                  ],
-                  [],
-                ),
-                ContextMenu.view(
-                  ~inject=a => inject(Perform(a)),
-                  ~syntax=model.editor.syntax,
-                  ~info_map=model.statics.info_map,
-                  ~font_metrics=globals.font_metrics,
-                  ~selected_index,
-                  model.editor.state.zipper,
-                ),
-              ]
-            | None => []
-            }
-          )
-        : [];
+          ),
+        ]
+        @ (
+          switch (model.context_menu) {
+          | Some(selected_index) => [
+              /* Backdrop for scroll-close. Click handling is done via
+                 ContextMenuListener's document-level event listener. */
+              Node.div(
+                ~attrs=[
+                  Attr.classes(["context-menu-backdrop"]),
+                  Attr.on_wheel(_ =>
+                    inject(ContextMenu(ContextMenu.Model.Close))
+                  ),
+                ],
+                [],
+              ),
+              ContextMenu.view(
+                ~inject=a => inject(Perform(a)),
+                ~syntax=model.editor.syntax,
+                ~info_map=model.statics.info_map,
+                ~font_metrics=globals.font_metrics,
+                ~selected_index,
+                model.editor.state.zipper,
+              ),
+            ]
+          | None => []
+          }
+        )
+      | JustHighlight => [
+          (
+            expand_selection
+              ? Highlight.selection_expanded(
+                  ~term_data=model.editor.syntax.term_data,
+                )
+              : Highlight.selection
+          )(
+            ~measured=model.editor.syntax.measured,
+            ~shape_map=model.editor.syntax.shape_map,
+            ~font_metrics=globals.font_metrics,
+            model.editor.state.zipper,
+          ),
+        ]
+      | No => []
+      };
     let zipper = model.editor.state.zipper;
     let refractor_data =
       RefractorView.mk_data(
@@ -336,7 +357,7 @@ module View = {
         ~statics=model.statics.info_map,
         ~dynamics,
         ~sample_cursor=zipper.refractors.sample_cursor,
-        ~editor_active=selected,
+        ~editor_active=selected != No,
       );
     let visible = globals.visible_rows;
     let refractors_model =
@@ -361,7 +382,7 @@ module View = {
           ~statics=model.statics.info_map,
           ~dynamics,
           ~sample_cursor=zipper.refractors.sample_cursor,
-          ~editor_active=selected,
+          ~editor_active=selected != No,
         ),
         model.editor.syntax.projector_list,
       );
@@ -441,7 +462,7 @@ module View = {
     Node.div(
       ~attrs=[
         Attr.classes(
-          ["cell-item", "code-editor"] @ (selected ? ["selected"] : []),
+          ["cell-item", "code-editor"] @ (selected != No ? ["selected"] : []),
         ),
         Attr.on_contextmenu(evt =>
           switch (Pointer.Event.mk(evt)) {

src/web/app/editors/result/EvalResult.re

@@ -464,7 +464,7 @@ module View = {
           ~globals,
           ~signal,
           ~inject,
-          ~selected=selected == Some(Evaluation()),
+          ~selected=selected == Some(Evaluation()) ? Yes : No,
           ~locked,
           model.result |> Calc.get_value,
           editor |> Calc.get_saved_exc(~print="result editor missing"),

src/web/app/editors/result/StepperEditor.re

@@ -84,6 +84,7 @@ module View = {
         ~font_metrics: FontMetrics.t,
         ~inject: Update.t => Ui_effect.t(unit),
         ~selected_id: option(Id.t),
+        ~write_out_steps: bool,
         signal: event => Ui_effect.t(unit),
         model: Model.t,
       ) => {
@@ -104,7 +105,6 @@ module View = {
              ),
            )
          );
-
     let taken_steps = (taken_steps: list(Id.t)) =>
       taken_steps
       |> List.filter_map(TermData.root_tile(_, syntax.term_data))
@@ -129,20 +129,25 @@ module View = {
          );
 
     taken_steps(model.taken_steps)
-    @ next_steps(model.next_steps, ~inject=x =>
-        {
-          open OptUtil.Syntax;
-          let+ range =
-            TermData.extreme_measures(
-              List.nth(model.next_steps, x),
-              model.editor.editor.syntax.term_data,
-              model.editor.editor.syntax.measured,
-            );
-          Some(List.nth(model.next_steps, x)) == selected_id
-            ? signal(TakeStep(x)) : inject(Select(PointToPoint(range)));
-        }
-        |> Option.value(~default=Ui_effect.Ignore)
-      )
+    @ (
+      write_out_steps
+        ? []
+        : next_steps(model.next_steps, ~inject=x =>
+            {
+              open OptUtil.Syntax;
+              let+ range =
+                TermData.extreme_measures(
+                  List.nth(model.next_steps, x),
+                  model.editor.editor.syntax.term_data,
+                  model.editor.editor.syntax.measured,
+                );
+              Some(List.nth(model.next_steps, x)) == selected_id
+                ? signal(TakeStep(x))
+                : inject(Select(PointToPoint(range)));
+            }
+            |> Option.value(~default=Ui_effect.Ignore)
+          )
+    )
     @ refl_steps(model.refls, ~inject=x =>
         {
           open OptUtil.Syntax;
@@ -189,6 +194,7 @@ module View = {
         @ deco(
             ~syntax=model.editor.editor.syntax,
             ~font_metrics=globals.font_metrics,
+            ~write_out_steps=globals.settings.core.evaluation.write_out_steps,
             ~inject,
             ~selected_id,
             signal,

src/web/app/editors/stepper/InductionCase.re

@@ -329,8 +329,8 @@ module F = (Stepper: STEPPER) => {
         ~inject=x => inject(PatternUpdate(x)),
         ~selected=
           switch (focus) {
-          | Some(Pattern ()) => true
-          | _ => false
+          | Some(Pattern ()) => Yes
+          | _ => No
           },
         ~dynamics=Dynamics.Map.empty,
         model.pattern,

src/web/app/editors/stepper/InductionStep.re

@@ -397,9 +397,9 @@ module F =
         ~inject=x => inject(ScrutUpdate(x)),
         ~selected=
           switch (focus) {
-          | Some(Scrut(_)) => true
+          | Some(Scrut(_)) => Yes
           | Some(_)
-          | None => false
+          | None => No
           },
         ~dynamics=Dynamics.Map.empty,
         model.scrut,