Skip to content

Commit 9c1cbd4

Browse files
NegabinaryNegabinary
committed
Retain highlight
1 parent 147f331 commit 9c1cbd4

7 files changed

Lines changed: 112 additions & 63 deletions

File tree

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -247,7 +247,7 @@ module View = {
247247
locked
248248
? _ => Ui_effect.Ignore
249249
: (action => inject(MainEditor(action))),
250-
~selected=selected == Some(MainEditor),
250+
~selected=selected == Some(MainEditor) ? Yes : No,
251251
~overlays=overlays(model.editor.editor),
252252
~dynamics=EvalResult.Model.dynamics(model.result),
253253
model.editor,

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

Lines changed: 68 additions & 47 deletions
Original file line numberDiff line numberDiff line change
@@ -229,7 +229,7 @@ module View = {
229229

230230
let deco =
231231
(
232-
~expand_selection=false,
232+
~expand_selection,
233233
~syntax: CachedSyntax.t,
234234
~globals: Globals.t,
235235
z: Zipper.t,
@@ -263,65 +263,86 @@ module View = {
263263
),
264264
];
265265

266+
type selected =
267+
| Yes
268+
| JustHighlight
269+
| No;
270+
266271
let view =
267272
(
268273
~globals: Globals.t,
269274
~signal: event => Ui_effect.t(unit),
270275
~inject: Update.t => Ui_effect.t(unit),
271-
~selected: bool,
276+
~selected: selected,
272277
~overlays: list(Node.t)=[],
273278
~dynamics: Language.Dynamics.Map.t,
274-
~expand_selection=?,
279+
~expand_selection=false,
275280
model: Model.t,
276281
) => {
277282
/* Sync document-level click listener for closing context menu */
278283
ContextMenuListener.sync(
279-
selected && Model.context_menu_is_open(model),
284+
selected == Yes && Model.context_menu_is_open(model),
280285
inject(ContextMenu(ContextMenu.Model.Close)),
281286
);
282287
let edit_decos =
283-
selected
284-
? deco(
285-
~expand_selection?,
288+
switch (selected) {
289+
| Yes =>
290+
deco(
291+
~expand_selection,
292+
~syntax=model.editor.syntax,
293+
~globals,
294+
model.editor.state.zipper,
295+
)
296+
@ [
297+
Arms.Refractors.all(
298+
~font_metrics=globals.font_metrics,
286299
~syntax=model.editor.syntax,
287-
~globals,
300+
~dynamics,
288301
model.editor.state.zipper,
289-
)
290-
@ [
291-
Arms.Refractors.all(
292-
~font_metrics=globals.font_metrics,
293-
~syntax=model.editor.syntax,
294-
~dynamics,
295-
model.editor.state.zipper,
296-
),
297-
]
298-
@ (
299-
switch (model.context_menu) {
300-
| Some(selected_index) => [
301-
/* Backdrop for scroll-close. Click handling is done via
302-
ContextMenuListener's document-level event listener. */
303-
Node.div(
304-
~attrs=[
305-
Attr.classes(["context-menu-backdrop"]),
306-
Attr.on_wheel(_ =>
307-
inject(ContextMenu(ContextMenu.Model.Close))
308-
),
309-
],
310-
[],
311-
),
312-
ContextMenu.view(
313-
~inject=a => inject(Perform(a)),
314-
~syntax=model.editor.syntax,
315-
~info_map=model.statics.info_map,
316-
~font_metrics=globals.font_metrics,
317-
~selected_index,
318-
model.editor.state.zipper,
319-
),
320-
]
321-
| None => []
322-
}
323-
)
324-
: [];
302+
),
303+
]
304+
@ (
305+
switch (model.context_menu) {
306+
| Some(selected_index) => [
307+
/* Backdrop for scroll-close. Click handling is done via
308+
ContextMenuListener's document-level event listener. */
309+
Node.div(
310+
~attrs=[
311+
Attr.classes(["context-menu-backdrop"]),
312+
Attr.on_wheel(_ =>
313+
inject(ContextMenu(ContextMenu.Model.Close))
314+
),
315+
],
316+
[],
317+
),
318+
ContextMenu.view(
319+
~inject=a => inject(Perform(a)),
320+
~syntax=model.editor.syntax,
321+
~info_map=model.statics.info_map,
322+
~font_metrics=globals.font_metrics,
323+
~selected_index,
324+
model.editor.state.zipper,
325+
),
326+
]
327+
| None => []
328+
}
329+
)
330+
| JustHighlight => [
331+
(
332+
expand_selection
333+
? Highlight.selection_expanded(
334+
~term_data=model.editor.syntax.term_data,
335+
)
336+
: Highlight.selection
337+
)(
338+
~measured=model.editor.syntax.measured,
339+
~shape_map=model.editor.syntax.shape_map,
340+
~font_metrics=globals.font_metrics,
341+
model.editor.state.zipper,
342+
),
343+
]
344+
| No => []
345+
};
325346
let zipper = model.editor.state.zipper;
326347
let refractor_data =
327348
RefractorView.mk_data(
@@ -336,7 +357,7 @@ module View = {
336357
~statics=model.statics.info_map,
337358
~dynamics,
338359
~sample_cursor=zipper.refractors.sample_cursor,
339-
~editor_active=selected,
360+
~editor_active=selected != No,
340361
);
341362
let visible = globals.visible_rows;
342363
let refractors_model =
@@ -361,7 +382,7 @@ module View = {
361382
~statics=model.statics.info_map,
362383
~dynamics,
363384
~sample_cursor=zipper.refractors.sample_cursor,
364-
~editor_active=selected,
385+
~editor_active=selected != No,
365386
),
366387
model.editor.syntax.projector_list,
367388
);
@@ -441,7 +462,7 @@ module View = {
441462
Node.div(
442463
~attrs=[
443464
Attr.classes(
444-
["cell-item", "code-editor"] @ (selected ? ["selected"] : []),
465+
["cell-item", "code-editor"] @ (selected != No ? ["selected"] : []),
445466
),
446467
Attr.on_contextmenu(evt =>
447468
switch (Pointer.Event.mk(evt)) {

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -464,7 +464,7 @@ module View = {
464464
~globals,
465465
~signal,
466466
~inject,
467-
~selected=selected == Some(Evaluation()),
467+
~selected=selected == Some(Evaluation()) ? Yes : No,
468468
~locked,
469469
model.result |> Calc.get_value,
470470
editor |> Calc.get_saved_exc(~print="result editor missing"),

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

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -329,8 +329,8 @@ module F = (Stepper: STEPPER) => {
329329
~inject=x => inject(PatternUpdate(x)),
330330
~selected=
331331
switch (focus) {
332-
| Some(Pattern ()) => true
333-
| _ => false
332+
| Some(Pattern ()) => Yes
333+
| _ => No
334334
},
335335
~dynamics=Dynamics.Map.empty,
336336
model.pattern,

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

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -397,9 +397,9 @@ module F =
397397
~inject=x => inject(ScrutUpdate(x)),
398398
~selected=
399399
switch (focus) {
400-
| Some(Scrut(_)) => true
400+
| Some(Scrut(_)) => Yes
401401
| Some(_)
402-
| None => false
402+
| None => No
403403
},
404404
~dynamics=Dynamics.Map.empty,
405405
model.scrut,

‎src/web/app/editors/stepper/MissingStep.re‎

Lines changed: 33 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -592,8 +592,8 @@ module View = {
592592
~inject=x => inject(RewriteEditorAction(x)),
593593
~selected=
594594
switch (selected) {
595-
| Some(RewriteEditor ()) => true
596-
| _ => false
595+
| Some(RewriteEditor ()) => Yes
596+
| _ => No
597597
},
598598
~dynamics=Dynamics.Map.empty,
599599
editor,
@@ -704,8 +704,8 @@ module View = {
704704
~inject=x => inject(WriteStepEditorAction(x)),
705705
~selected=
706706
switch (selected) {
707-
| Some(WriteStepEditor ()) => true
708-
| _ => false
707+
| Some(WriteStepEditor ()) => Yes
708+
| _ => No
709709
},
710710
~dynamics=Dynamics.Map.empty,
711711
editor,
@@ -779,6 +779,8 @@ module View = {
779779
];
780780
};
781781

782+
let text_arrow = (b: bool) => if (b) {"▲"} else {"▼"};
783+
782784
// I want to make a bunch of buttons here:
783785
// Evaluate [TODO], Rewrite, Axioms, Cases,
784786
let buttons =
@@ -833,14 +835,38 @@ module View = {
833835
? [
834836
proof_button(
835837
~callback=inject(ProposeWrittenStep),
836-
"Take Step ▼",
838+
"Take Step "
839+
++ text_arrow(
840+
switch (model.open_box) {
841+
| Model.WrittenStepOpen(_) => true
842+
| _ => false
843+
},
844+
),
837845
),
838846
]
839847
: []
840848
)
841849
@ [
842-
proof_button(~callback=inject(ProposeRewrite), "Algebra ▼"),
843-
proof_button(~callback=inject(ToggleAxioms), "Assumptions ▼"),
850+
proof_button(
851+
~callback=inject(ProposeRewrite),
852+
"Algebra "
853+
++ text_arrow(
854+
switch (model.open_box) {
855+
| Model.RewritesOpen(_) => true
856+
| _ => false
857+
},
858+
),
859+
),
860+
proof_button(
861+
~callback=inject(ToggleAxioms),
862+
"Assumptions "
863+
++ text_arrow(
864+
switch (model.open_box) {
865+
| Model.AxiomsOpen(_) => true
866+
| _ => false
867+
},
868+
),
869+
),
844870
proof_button(
845871
~callback=
846872
Ui_effect.Many([

‎src/web/app/editors/stepper/StepperBase.re‎

Lines changed: 5 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1071,9 +1071,11 @@ and Stepper: {
10711071
},
10721072
~inject=x => inject(EditorAction(x)),
10731073
~selected=
1074-
switch (focus) {
1075-
| Some(Here(_)) => true
1076-
| _ => false
1074+
switch (focus, model.step_kind) {
1075+
| (Some(Here(_)), _) => Yes
1076+
| (_, MissingStep({open_box: NoneOpen, _})) => No
1077+
| (_, MissingStep(_)) => JustHighlight
1078+
| _ => No
10771079
},
10781080
~selected_id=selected_exp |> Option.map(Exp.rep_id),
10791081
~overlays=

0 commit comments

Comments
 (0)