Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
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
8 changes: 8 additions & 0 deletions src/haz3lcore/zipper/Refractors.re
Original file line number Diff line number Diff line change
Expand Up @@ -74,6 +74,14 @@ let init = {
let persist = (refractors: t): string =>
refractors.manuals |> RefractorList.sexp_of_t |> Sexplib.Sexp.to_string;

/* Prepares refractors for serialization by resetting non-persistable state.
* Only `manuals` is persisted - see state location docs at top of file.
* Used by both sexp serialization (persist) and show serialization (Exercise export). */
let for_serialization = (refractors: t): t => {
...init,
manuals: refractors.manuals,
};

/* Refractors store a simplified `entry` type in Zipper.Refractor.Map
* (just kind + model), avoiding redundant id/syntax in serialization.
* When the full Base.projector is needed for rendering, use `to_projector`. */
Expand Down
19 changes: 14 additions & 5 deletions src/util/Id.re
Original file line number Diff line number Diff line change
Expand Up @@ -109,11 +109,20 @@ module Map = {
|> List.to_seq
|> of_seq;

let pp = (pp_v, fmt, map) =>
bindings(map)
|> List.iter(((k, v)) =>
Format.fprintf(fmt, "%a -> %a\n", pp, k, pp_v, v)
);
/* Outputs valid OCaml code for empty maps only.
* Non-empty maps will fail - this is intentional. Currently only empty maps
* are serialized via show (see Refractors.for_serialization which resets
* autos to empty before serialization). If you need to persist non-empty
* Id.Map values, implement proper nested Id.Map.add output here. */
let pp = (_pp_v, fmt, map) =>
if (is_empty(map)) {
Format.fprintf(fmt, "Haz3lcore.Id.Map.empty");
} else {
failwith(
"Id.Map.pp: non-empty map serialization not implemented. "
++ "See Refractors.for_serialization if you're seeing this during exercise export.",
);
};
};
let invalid: t =
"00000000-0000-0000-0000-000000000000" |> Uuidm.of_string |> Option.get;
Expand Down
4 changes: 3 additions & 1 deletion src/web/exercises/Exercise.re
Original file line number Diff line number Diff line change
Expand Up @@ -837,8 +837,10 @@ let pos_of_key = (key: string): pos =>

let editor_pp = (fmt, editor: Editor.t) => {
let zipper = editor.state.zipper;
/* Reset non-persistable refractor state before serialization.
* See Refractors.for_serialization - keeps manuals, resets autos/sample_cursor. */
let zipper = Zipper.update_refractors(zipper, Refractors.for_serialization);
let serialization = Zipper.show(zipper);
// let string_literal = "\"" ++ String.escaped(serialization) ++ "\"";
Format.pp_print_string(fmt, serialization);
};

Expand Down