Skip to content

Comment out jumping #2084

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Draft
Negabinary wants to merge 2 commits into
base: delete-axioms
Choose a base branch
from
Draft

Comment out jumping #2084

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
5f2d35f
Comment out jumping
Negabinary Jan 26, 2026
5a020d8
Comment out assistant
Negabinary Feb 6, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
10 changes: 5 additions & 5 deletions src/haz3lcore/ProbePerform.re
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -592,11 +592,11 @@ let go =
| Some(id) => toggle_statics(~syntax, id, info_map, z)
| None => z
}
| StepInto(sample, ap_id) =>
switch (step_into_sample(~syntax, ~sample, ~ap_id, info_map, z)) {
| Some(z) => z
| None => z
}
// | StepInto(sample, ap_id) =>
// switch (step_into_sample(~syntax, ~sample, ~ap_id, info_map, z)) {
// | Some(z) => z
// | None => z
// }
};

/* Check if id has either manual or ephermeral probe on it */
Expand Down
72 changes: 36 additions & 36 deletions src/haz3lcore/projectors/implementations/ProbeProj.re
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -526,9 +526,9 @@ let dropdown_id = (sample_id: int): string =>
"sample-dropdown-" ++ string_of_int(sample_id);

/* Step into handler for sample context menu */
let step_into_sample =
(~parent, ~sample: Sample.t, ~ap_id: Id.t): Ui_effect.t(unit) =>
parent(Probe(StepInto(sample, ap_id)));
// let step_into_sample =
// (~parent, ~sample: Sample.t, ~ap_id: Id.t): Ui_effect.t(unit) =>
// parent(Probe(StepInto(sample, ap_id)));

/* Context actions for a sample (Pin/Unpin, Step Into, etc.) */
let sample_context_actions =
Expand Down Expand Up @@ -557,26 +557,26 @@ let sample_context_actions =
span(~attrs=[Attr.classes(["shortcut"])], [text("P")]),
],
),
/* Step Into action */
div(
~attrs=[
Attr.classes(["action-item", "step-into-action"]),
Attr.on_pointerdown(_
/* Stop propagation to prevent parent wrapper's Focus action
from moving cursor back to the probe after we jump */
=>
Effect.Many([
Effect.Stop_propagation,
step_into_sample(~parent, ~sample, ~ap_id),
])
),
],
[
div(~attrs=[Attr.classes(["step-into-icon"])], []),
text("Step into"),
span(~attrs=[Attr.classes(["shortcut"])], [text("Enter")]),
],
),
// /* Step Into action */
// div(
// ~attrs=[
// Attr.classes(["action-item", "step-into-action"]),
// Attr.on_pointerdown(_
// /* Stop propagation to prevent parent wrapper's Focus action
// from moving cursor back to the probe after we jump */
// =>
// Effect.Many([
// Effect.Stop_propagation,
// step_into_sample(~parent, ~sample, ~ap_id),
// ])
// ),
// ],
// [
// div(~attrs=[Attr.classes(["step-into-icon"])], []),
// text("Step into"),
// span(~attrs=[Attr.classes(["shortcut"])], [text("Enter")]),
// ],
// ),
],
),
];
Expand Down Expand Up @@ -1014,19 +1014,19 @@ let key_handler =
print_endline("pin: no sample or ap_id");
Many([Stop_propagation, Prevent_default]);
}
| D("Enter") =>
/* Step into the indicated sample */
switch (indicated_sample(~ap_id, di), ap_id) {
| (Some(sample), Some(ap_id)) =>
Many([
Stop_propagation,
Prevent_default,
step_into_sample(~parent, ~sample, ~ap_id),
])
| _ =>
print_endline("step into: no sample or ap_id");
Many([Stop_propagation, Prevent_default]);
}
// | D("Enter") =>
// /* Step into the indicated sample */
// switch (indicated_sample(~ap_id, di), ap_id) {
// | (Some(sample), Some(ap_id)) =>
// Many([
// Stop_propagation,
// Prevent_default,
// step_into_sample(~parent, ~sample, ~ap_id),
// ])
// | _ =>
// print_endline("step into: no sample or ap_id");
// Many([Stop_propagation, Prevent_default]);
// }
| _ => Many([Stop_propagation])
};
};
Expand Down
6 changes: 3 additions & 3 deletions src/haz3lcore/zipper/action/Action.re
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,7 @@ type chunkiness =
[@deriving (show({with_path: false}), sexp, yojson, eq)]
type goal =
| Hole(Direction.t)
| TileId([@equal (_, _) => true] Id.t)
// | TileId([@equal (_, _) => true] Id.t)
| BindingSiteOfIndicatedVar;

[@deriving (show({with_path: false}), sexp, yojson, eq)]
Expand Down Expand Up @@ -87,8 +87,8 @@ type paste =
type probe =
| ToggleManual
| ToggleAuto
| ToggleStatics
| StepInto(Language.Sample.t, Id.t);
| ToggleStatics;
// | StepInto(Language.Sample.t, Id.t);

[@deriving (show({with_path: false}), sexp, yojson, eq)]
type t =
Expand Down
2 changes: 1 addition & 1 deletion src/haz3lcore/zipper/action/Move.re
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -143,7 +143,7 @@ let move_dispatch =
| Vertical(d) => vertical(~measured, ~col_target, d, z)
| Point(goal) => to_point(~measured, ~goal, z)
| Goal(Hole(d)) => to_next_grout(d, z)
| Goal(TileId(id)) => jump_to_id_indicated(z, id)
// | Goal(TileId(id)) => jump_to_id_indicated(z, id)
| Goal(BindingSiteOfIndicatedVar) =>
let* ci = Indicated.ci_of(z, statics);
let* binding_id = Language.Info.get_binding_site(ci);
Expand Down
52 changes: 26 additions & 26 deletions src/web/app/Page.re
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -113,7 +113,7 @@ module Update = {
(
~import_log,
~schedule_action,
~globals: Globals.Model.t,
~globals as _: Globals.Model.t,
action: Globals.Update.t,
model: Model.t,
) => {
Expand All @@ -137,31 +137,31 @@ module Update = {
settings,
},
};
| JumpToTile(id) =>
let jump =
Editors.Selection.jump_to_tile(
~settings=model.globals.settings,
id,
model.editors,
);
switch (jump) {
| None => model |> Updated.raise_invalid_action
| Some((action, selection)) =>
let* editors =
Editors.Update.update(
~globals,
~schedule_action=a => schedule_action(Editors(a)),
~send_assistant_insertion_info=
assistant_callback(~schedule_action, model),
action,
model.editors,
);
{
...model,
editors,
selection,
};
};
// | JumpToTile(id) =>
// let jump =
// Editors.Selection.jump_to_tile(
// ~settings=model.globals.settings,
// id,
// model.editors,
// );
// switch (jump) {
// | None => model |> Updated.raise_invalid_action
// | Some((action, selection)) =>
// let* editors =
// Editors.Update.update(
// ~globals,
// ~schedule_action=a => schedule_action(Editors(a)),
// ~send_assistant_insertion_info=
// assistant_callback(~schedule_action, model),
// action,
// model.editors,
// );
// {
// ...model,
// editors,
// selection,
// };
// };
| InitImportAll(file) =>
JsUtil.read_file(file, data =>
schedule_action(Globals(FinishImportAll(data)))
Expand Down
32 changes: 16 additions & 16 deletions src/web/app/editors/Editors.re
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -324,22 +324,22 @@ module Selection = {
};
};

let jump_to_tile =
(~settings, tile, model: Model.t): option((Update.t, t)) =>
switch (model) {
| Scratch(m) =>
ScratchMode.Selection.jump_to_tile(tile, m)
|> Option.map(((x, y)) => (Update.Scratch(x), Scratch(y)))
| Documentation(m) =>
ScratchMode.Selection.jump_to_tile(tile, m)
|> Option.map(((x, y)) => (Update.Scratch(x), Scratch(y)))
| Tutorial(m) =>
TutorialsMode.Selection.jump_to_tile(~settings, tile, m)
|> Option.map(((x, y)) => (Update.Tutorial(x), Tutorial(y)))
| Exercises(m) =>
ExercisesMode.Selection.jump_to_tile(~settings, tile, m)
|> Option.map(((x, y)) => (Update.Exercises(x), Exercises(y)))
};
// let jump_to_tile =
// (~settings, tile, model: Model.t): option((Update.t, t)) =>
// switch (model) {
// | Scratch(m) =>
// ScratchMode.Selection.jump_to_tile(tile, m)
// |> Option.map(((x, y)) => (Update.Scratch(x), Scratch(y)))
// | Documentation(m) =>
// ScratchMode.Selection.jump_to_tile(tile, m)
// |> Option.map(((x, y)) => (Update.Scratch(x), Scratch(y)))
// | Tutorial(m) =>
// TutorialsMode.Selection.jump_to_tile(~settings, tile, m)
// |> Option.map(((x, y)) => (Update.Tutorial(x), Tutorial(y)))
// | Exercises(m) =>
// ExercisesMode.Selection.jump_to_tile(~settings, tile, m)
// |> Option.map(((x, y)) => (Update.Exercises(x), Exercises(y)))
// };

let default_selection =
fun
Expand Down
21 changes: 10 additions & 11 deletions src/web/app/editors/cell/CellEditor.re
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -179,11 +179,10 @@ module Selection = {
|> Option.map(x => Update.ResultAction(x))
};
};

let jump_to_tile = (tile, model: Model.t): option((Update.t, t)) => {
CodeEditable.Selection.jump_to_tile(tile, model.editor)
|> Option.map(x => (Update.MainEditor(x), MainEditor));
};
// let jump_to_tile = (tile, model: Model.t): option((Update.t, t)) => {
// CodeEditable.Selection.jump_to_tile(tile, model.editor)
// |> Option.map(x => (Update.MainEditor(x), MainEditor));
// };
};

module View = {
Expand Down Expand Up @@ -215,12 +214,12 @@ module View = {
},
~signal=
fun
| MakeActive(a) => signal(MakeActive(Result(a)))
| JumpTo(id) =>
Effect.Many([
signal(MakeActive(MainEditor)),
inject(MainEditor(Perform(Move(Goal(TileId(id)))))),
]),
| MakeActive(a) => signal(MakeActive(Result(a))),
// | JumpTo(id) =>
// Effect.Many([
// signal(MakeActive(MainEditor)),
// inject(MainEditor(Perform(Move(Goal(TileId(id)))))),
// ]),
~inject=a => inject(ResultAction(a)),
~selected={
switch (selected) {
Expand Down
15 changes: 7 additions & 8 deletions src/web/app/editors/code/CodeEditable.re
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -79,7 +79,7 @@ module Update = {
| Cut
| Reparse
| Introduce
| Probe(StepInto(_))
// | Probe(StepInto(_))
| Dump => true
| Project(_)
| Unselect(_)
Expand Down Expand Up @@ -189,13 +189,12 @@ module Selection = {
}
};
};

let jump_to_tile = (id: Id.t, model: Model.t): option(Update.t) => {
switch (TermData.root_tile(id, model.editor.syntax.term_data)) {
| Some(_) => Some(Perform(Move(Goal(TileId(id)))))
| None => None
};
};
// let jump_to_tile = (id: Id.t, model: Model.t): option(Update.t) => {
// switch (TermData.root_tile(id, model.editor.syntax.term_data)) {
// | Some(_) => Some(Perform(Move(Goal(TileId(id)))))
// | None => None
// };
// };
};

module View = {
Expand Down
29 changes: 14 additions & 15 deletions src/web/app/editors/mode/ExercisesMode.re
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -466,21 +466,20 @@ module Selection = {
| (Theorem(_), _) => None
};
};

let jump_to_tile =
(~settings, tile, model: Model.t): option((Update.t, t)) => {
let current = List.nth(model.exercises, model.current);
switch (current) {
| Implementation(e) =>
ExerciseMode.Selection.jump_to_tile(~settings, tile, e)
|> Option.map(((x, y)) => (Update.Exercise(x), Implementation(y)))
| Theorem(e) =>
TheoremExerciseMode.Selection.jump_to_tile(tile, e)
|> Option.map(((x, y)) =>
(Update.TheoremExercise(x), TheoremExercise(y))
)
};
};
// let jump_to_tile =
// (~settings, tile, model: Model.t): option((Update.t, t)) => {
// let current = List.nth(model.exercises, model.current);
// switch (current) {
// | Implementation(e) =>
// ExerciseMode.Selection.jump_to_tile(~settings, tile, e)
// |> Option.map(((x, y)) => (Update.Exercise(x), Implementation(y)))
// | Theorem(e) =>
// TheoremExerciseMode.Selection.jump_to_tile(tile, e)
// |> Option.map(((x, y)) =>
// (Update.TheoremExercise(x), TheoremExercise(y))
// )
// };
// };
};

module View = {
Expand Down
16 changes: 8 additions & 8 deletions src/web/app/editors/mode/TutorialsMode.re
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -315,14 +315,14 @@ module Selection = {
List.nth(model.exercises, model.current),
)
|> Option.map(a => Update.Tutorial(a));
let jump_to_tile =
(~settings, tile, model: Model.t): option((Update.t, t)) =>
TutorialMode.Selection.jump_to_tile(
~settings,
tile,
List.nth(model.exercises, model.current),
)
|> Option.map(((x, y)) => (Update.Tutorial(x), y));
// let jump_to_tile =
// (~settings, tile, model: Model.t): option((Update.t, t)) =>
// TutorialMode.Selection.jump_to_tile(
// ~settings,
// tile,
// List.nth(model.exercises, model.current),
// )
// |> Option.map(((x, y)) => (Update.Tutorial(x), y));
};

module View = {
Expand Down
6 changes: 3 additions & 3 deletions src/web/app/editors/result/EvalResult.re
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -366,8 +366,8 @@ module View = {
open WebUtil.Node;

type event =
| MakeActive(Selection.t)
| JumpTo(Id.t);
| MakeActive(Selection.t);
// | JumpTo(Id.t);

let error_msg = (err: ProgramResult.error) =>
switch (err) {
Expand Down Expand Up @@ -634,7 +634,7 @@ module View = {
[
CellCommon.report_footer_view([
TestView.test_summary(
~inject_jump=tile => signal(JumpTo(tile)),
// ~inject_jump=tile => signal(JumpTo(tile)),
~test_results,
),
]),
Expand Down
2 changes: 1 addition & 1 deletion src/web/app/explainthis/ExplainThis.re
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -105,7 +105,7 @@ let highlight =
Attr.on_mouseleave(_ =>
globals.inject_global(Set(ExplainThis(SetHighlight(UnsetHover))))
),
Attr.on_click(_ => globals.inject_global(JumpToTile(id))),
// Attr.on_click(_ => globals.inject_global(JumpToTile(id))),
];
(Node.span(~attrs, msg), mapping);
};
Expand Down
Loading