# HG changeset patch
# User wenzelm
# Date 1667502635 -3600
# Node ID f362975e8ba11c5be07a3f3fc606a009a7feb40b
# Parent  cda63f26d0cb77ce8da3b2c82f95dd3e69543611
clarified signature;

diff -r cda63f26d0cb -r f362975e8ba1 src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Thu Nov 03 16:08:28 2022 +0100
+++ b/src/Pure/Isar/isar_cmd.ML	Thu Nov 03 20:10:35 2022 +0100
@@ -195,7 +195,7 @@
 fun diag_state ctxt =
   (case Diag_State.get ctxt of
     SOME st => st
-  | NONE => Toplevel.init_toplevel ());
+  | NONE => Toplevel.make_state NONE);
 
 val diag_goal = Proof.goal o Toplevel.proof_of o diag_state;
 
diff -r cda63f26d0cb -r f362975e8ba1 src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Thu Nov 03 16:08:28 2022 +0100
+++ b/src/Pure/Isar/toplevel.ML	Thu Nov 03 20:10:35 2022 +0100
@@ -8,8 +8,7 @@
 sig
   exception UNDEF
   type state
-  val init_toplevel: unit -> state
-  val theory_toplevel: theory -> state
+  val make_state: theory option -> state
   val is_toplevel: state -> bool
   val is_theory: state -> bool
   val is_proof: state -> bool
@@ -149,8 +148,9 @@
 fun previous_theory_of (State (_, (prev_thy, _))) = prev_thy;
 fun output_of (State (_, (_, output))) = output;
 
-fun init_toplevel () = State (node_presentation Toplevel, (NONE, NONE));
-fun theory_toplevel thy = State (node_presentation (Theory (Context.Theory thy)), (NONE, NONE));
+fun make_state opt_thy =
+  let val node = (case opt_thy of NONE => Toplevel | SOME thy => Theory (Context.Theory thy))
+  in State (node_presentation node, (NONE, NONE)) end;
 
 fun level state =
   (case node_of state of
@@ -717,7 +717,7 @@
   let
     fun add (tr, st') res =
       (case res of
-        [] => [(init_toplevel (), tr, st')]
+        [] => [(make_state NONE, tr, st')]
       | (_, _, st) :: _ => (st, tr, st') :: res);
     fun acc (Result r) = add r
       | acc (Result_List rs) = fold acc rs
diff -r cda63f26d0cb -r f362975e8ba1 src/Pure/PIDE/command.ML
--- a/src/Pure/PIDE/command.ML	Thu Nov 03 16:08:28 2022 +0100
+++ b/src/Pure/PIDE/command.ML	Thu Nov 03 20:10:35 2022 +0100
@@ -170,10 +170,7 @@
 fun init_eval_state opt_thy =
  {failed = false,
   command = Toplevel.empty,
-  state =
-    (case opt_thy of
-      NONE => Toplevel.init_toplevel ()
-    | SOME thy => Toplevel.theory_toplevel thy)};
+  state = Toplevel.make_state opt_thy};
 
 datatype eval =
   Eval of
diff -r cda63f26d0cb -r f362975e8ba1 src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Thu Nov 03 16:08:28 2022 +0100
+++ b/src/Pure/PIDE/document.ML	Thu Nov 03 20:10:35 2022 +0100
@@ -614,7 +614,7 @@
     val imports = #imports header;
 
     fun maybe_eval_result eval = Command.eval_result_state eval
-      handle Fail _ => Toplevel.init_toplevel ();
+      handle Fail _ => Toplevel.make_state NONE;
 
     fun maybe_end_theory pos st = SOME (Toplevel.end_theory pos st)
       handle ERROR msg => (Output.error_message msg; NONE);
@@ -625,7 +625,7 @@
           NONE =>
             maybe_end_theory pos
               (case get_result (snd (the (AList.lookup (op =) deps import))) of
-                NONE => Toplevel.init_toplevel ()
+                NONE => Toplevel.make_state NONE
               | SOME (_, eval) => maybe_eval_result eval)
             |> Option.map (fn thy => (thy, (pos, Theory.get_markup thy)))
         | SOME thy => SOME (thy, (Position.none, Markup.empty))));
@@ -760,7 +760,7 @@
 
                               val st =
                                 (case try (#1 o the o the_entry node o the) prev of
-                                  NONE => Toplevel.init_toplevel ()
+                                  NONE => Toplevel.make_state NONE
                                 | SOME prev_eval => Command.eval_result_state prev_eval);
 
                               val exec_id = Command.eval_exec_id eval;
diff -r cda63f26d0cb -r f362975e8ba1 src/Pure/Thy/document_output.ML
--- 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"
diff -r cda63f26d0cb -r f362975e8ba1 src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Thu Nov 03 16:08:28 2022 +0100
+++ b/src/Pure/Thy/thy_info.ML	Thu Nov 03 20:10:35 2022 +0100
@@ -292,7 +292,7 @@
           in (results, (st', pos')) end;
 
         val (results, (end_state, end_pos)) =
-          fold_map element_result elements (Toplevel.init_toplevel (), Position.none);
+          fold_map element_result elements (Toplevel.make_state NONE, Position.none);
 
         val thy = Toplevel.end_theory end_pos end_state;
       in (results, thy) end;
@@ -434,7 +434,7 @@
   let
     val trs = Outer_Syntax.parse_text thy (K thy) pos txt;
     val end_pos = if null trs then pos else Toplevel.pos_of (List.last trs);
-    val end_state = fold (Toplevel.command_exception true) trs (Toplevel.init_toplevel ());
+    val end_state = fold (Toplevel.command_exception true) trs (Toplevel.make_state NONE);
   in Toplevel.end_theory end_pos end_state end;