changeset 76415 | f362975e8ba1 |
parent 76410 | 687fb18e805c |
child 76432 | d0079b509d99 |
--- a/src/Pure/Thy/document_output.ML Thu Nov 03 16:08:28 2022 +0100 +++ b/src/Pure/Thy/document_output.ML Thu Nov 03 20:10:35 2022 +0100 @@ -476,7 +476,7 @@ in if length command_results = length spans then (([], []), NONE, true, [], (I, I)) - |> present (Toplevel.init_toplevel ()) (spans ~~ command_results) + |> present (Toplevel.make_state NONE) (spans ~~ command_results) |> present_trailer |> rev else error "Messed-up outer syntax for presentation"