merged

--- a/src/Pure/Isar/outer_syntax.ML	Thu Dec 29 22:14:12 2022 +0000
+++ b/src/Pure/Isar/outer_syntax.ML	Thu Dec 29 22:14:25 2022 +0000
@@ -163,8 +163,7 @@
       Parse.opt_target -- parse >> (fn (target, f) => trans restricted target f)));
 
 val local_theory' =
-  local_theory_command
-    (fn a => fn b => fn c => Toplevel.local_theory' a b c Toplevel.no_presentation);
+  local_theory_command (fn a => fn b => fn c => Toplevel.local_theory' a b c NONE);
 val local_theory = local_theory_command Toplevel.local_theory;
 val local_theory_to_proof' = local_theory_command Toplevel.local_theory_to_proof';
 val local_theory_to_proof = local_theory_command Toplevel.local_theory_to_proof;

--- a/src/Pure/Isar/toplevel.ML	Thu Dec 29 22:14:12 2022 +0000
+++ b/src/Pure/Isar/toplevel.ML	Thu Dec 29 22:14:25 2022 +0000
@@ -29,9 +29,7 @@
   val pretty_state: state -> Pretty.T list
   val string_of_state: state -> string
   val pretty_abstract: state -> Pretty.T
-  type presentation = state -> Latex.text option
-  val presentation: (state -> Latex.text) -> presentation
-  val no_presentation: presentation
+  type presentation = state -> Latex.text
   type transition
   val empty: transition
   val name_of: transition -> string
@@ -46,7 +44,7 @@
   val is_init: transition -> bool
   val modify_init: (unit -> theory) -> transition -> transition
   val exit: transition -> transition
-  val present: (state -> Latex.text) -> transition -> transition
+  val present: presentation -> transition -> transition
   val keep: (state -> unit) -> transition -> transition
   val keep': (bool -> state -> unit) -> transition -> transition
   val keep_proof: (state -> unit) -> transition -> transition
@@ -55,17 +53,17 @@
   val ignored: Position.T -> transition
   val malformed: Position.T -> string -> transition
   val generic_theory: (generic_theory -> generic_theory) -> transition -> transition
-  val theory': (bool -> theory -> theory) -> presentation -> transition -> transition
+  val theory': (bool -> theory -> theory) -> presentation option -> transition -> transition
   val theory: (theory -> theory) -> transition -> transition
   val begin_main_target: bool -> (theory -> local_theory) -> transition -> transition
   val end_main_target: transition -> transition
   val begin_nested_target: (Context.generic -> local_theory) -> transition -> transition
   val end_nested_target: transition -> transition
   val local_theory': (bool * Position.T) option -> (xstring * Position.T) option ->
-    (bool -> local_theory -> local_theory) -> presentation -> transition -> transition
+    (bool -> local_theory -> local_theory) -> presentation option -> transition -> transition
   val local_theory: (bool * Position.T) option -> (xstring * Position.T) option ->
     (local_theory -> local_theory) -> transition -> transition
-  val present_local_theory: (xstring * Position.T) option -> (state -> Latex.text) ->
+  val present_local_theory: (xstring * Position.T) option -> presentation ->
     transition -> transition
   val local_theory_to_proof': (bool * Position.T) option -> (xstring * Position.T) option ->
     (bool -> local_theory -> Proof.state) -> transition -> transition
@@ -141,12 +139,12 @@
   (node, cases_node init_presentation Context.proof_of Proof.context_of node);
 
 datatype state =
-  State of node_presentation * (theory option * Latex.text option);
+  State of node_presentation * (theory option * Latex.text future option);
     (*current node with presentation context, previous theory, document output*)
 
 fun node_of (State ((node, _), _)) = node;
 fun previous_theory_of (State (_, (prev_thy, _))) = prev_thy;
-fun output_of (State (_, (_, output))) = output;
+fun output_of (State (_, (_, output))) = Option.map Future.join output;
 
 fun make_state opt_thy =
   let val node = (case opt_thy of NONE => Toplevel | SOME thy => Theory (Context.Theory thy))
@@ -256,14 +254,9 @@
 
 (** toplevel transitions **)
 
-(* presentation *)
+(* primitive transitions *)
 
-type presentation = state -> Latex.text option;
-fun presentation g : presentation = SOME o g;
-val no_presentation: presentation = K NONE;
-
-
-(* primitive transitions *)
+type presentation = state -> Latex.text;
 
 datatype trans =
   (*init theory*)
@@ -271,78 +264,76 @@
   (*formal exit of theory*)
   Exit |
   (*keep state unchanged*)
-  Keep of bool -> presentation |
+  Keep of (bool -> state -> unit) * presentation option |
   (*node transaction and presentation*)
-  Transaction of (bool -> node -> node_presentation) * presentation;
+  Transaction of (bool -> node -> node_presentation) * presentation option;
 
 local
 
-exception FAILURE of state * exn;
-
-fun apply_presentation g (st as State (node, (prev_thy, _))) =
-  State (node, (prev_thy, g st));
-
-fun apply f g node =
+fun present_state fork g node_pr prev_thy =
   let
-    val node_pr = node_presentation node;
-    val context = cases_proper_node I (Context.Proof o Proof.context_of) node;
-    fun make_state node_pr' = State (node_pr', (get_theory node, NONE));
+    val state = State (node_pr, (prev_thy, NONE));
+    fun present pr =
+      if fork andalso Future.proofs_enabled 1 then
+        Execution.fork {name = "Toplevel.present_state", pos = Position.thread_data (), pri = ~1}
+          (fn () => pr state)
+      else Future.value (pr state);
+  in State (node_pr, (prev_thy, Option.map present g)) end;
 
-    val (st', err) =
-      (Runtime.controlled_execution (SOME context) (f #> make_state #> apply_presentation g) node,
-        NONE) handle exn => (make_state node_pr, SOME exn);
-  in
-    (case err of
-      NONE => st'
-    | SOME exn => raise FAILURE (st', exn))
-  end;
+fun no_update f g state =
+  Runtime.controlled_execution (try generic_theory_of state)
+    (fn () =>
+      let
+        val prev_thy = previous_theory_of state;
+        val () = f state;
+        val node_pr = node_presentation (node_of state);
+      in present_state false g node_pr prev_thy end) ()
+
+fun update f g state =
+  Runtime.controlled_execution (try generic_theory_of state)
+    (fn () =>
+      let
+        val prev_thy = previous_theory_of state;
+        val node_pr' = f (node_of state);
+      in present_state true g node_pr' prev_thy end) ();
 
 fun apply_tr int trans state =
   (case (trans, node_of state) of
     (Init f, Toplevel) =>
       Runtime.controlled_execution NONE (fn () =>
         State (node_presentation (Theory (Context.Theory (f ()))), (NONE, NONE))) ()
-  | (Exit, node as Theory (Context.Theory thy)) =>
+  | (Exit, Theory (Context.Theory thy)) =>
       let
         val State ((node', pr_ctxt), _) =
-          node |> apply
+          state |> update
             (fn _ =>
               node_presentation
                 (Theory (Context.Theory (tap Thm.expose_theory (Theory.end_theory thy)))))
-            no_presentation;
+            NONE;
       in State ((Toplevel, pr_ctxt), (get_theory node', NONE)) end
-  | (Keep f, node) =>
-      Runtime.controlled_execution (try generic_theory_of state)
-        (fn () =>
-          let
-            val prev_thy = previous_theory_of state;
-            val state' = State (node_presentation node, (prev_thy, NONE));
-          in apply_presentation (fn st => f int st) state' end) ()
+  | (Keep (f, g), _) => no_update (fn x => f int x) g state
   | (Transaction _, Toplevel) => raise UNDEF
-  | (Transaction (f, g), node) => apply (fn x => f int x) g node
+  | (Transaction (f, g), _) => update (fn x => f int x) g state
   | _ => raise UNDEF);
 
-fun apply_union _ [] state = raise FAILURE (state, UNDEF)
-  | apply_union int (tr :: trs) state =
-      apply_union int trs state
-        handle Runtime.UNDEF => apply_tr int tr state
-          | FAILURE (alt_state, UNDEF) => apply_tr int tr alt_state
-          | exn as FAILURE _ => raise exn
-          | exn => raise FAILURE (state, exn);
+fun apply_body _ [] _ = raise UNDEF
+  | apply_body int [tr] state = apply_tr int tr state
+  | apply_body int (tr :: trs) state =
+      apply_body int trs state
+        handle Runtime.UNDEF => apply_tr int tr state;
 
 fun apply_markers name markers (state as State ((node, pr_ctxt), prev_thy)) =
   let
     val state' =
       Runtime.controlled_execution (try generic_theory_of state)
         (fn () => State ((node, fold (Document_Marker.evaluate name) markers pr_ctxt), prev_thy)) ();
-  in (state', NONE) end
-  handle exn => (state, SOME exn);
+  in (state', NONE) end;
 
 in
 
-fun apply_trans int name markers trans state =
-  (apply_union int trans state |> apply_markers name markers)
-  handle FAILURE (alt_state, exn) => (alt_state, SOME exn) | exn => (state, SOME exn);
+fun apply_capture int name markers trans state =
+  (apply_body int trans state |> apply_markers name markers)
+    handle exn => (state, SOME exn);
 
 end;
 
@@ -412,12 +403,12 @@
 val exit = add_trans Exit;
 
 fun present_transaction f g = add_trans (Transaction (f, g));
-fun transaction f = present_transaction f no_presentation;
-fun transaction0 f = present_transaction (node_presentation oo f) no_presentation;
+fun transaction f = present_transaction f NONE;
+fun transaction0 f = present_transaction (node_presentation oo f) NONE;
 
-fun present f = add_trans (Keep (K (presentation f)));
-fun keep f = add_trans (Keep (fn _ => fn st => let val () = f st in NONE end));
-fun keep' f = add_trans (Keep (fn int => fn st => let val () = f int st in NONE end));
+fun present g = add_trans (Keep (fn _ => fn _ => (), SOME g));
+fun keep f = add_trans (Keep (K f, NONE));
+fun keep' f = add_trans (Keep (f, NONE));
 
 fun keep_proof f =
   keep (fn st =>
@@ -453,7 +444,7 @@
       in node_presentation (Theory (Context.Theory thy')) end
     | _ => raise UNDEF));
 
-fun theory f = theory' (K f) no_presentation;
+fun theory f = theory' (K f) NONE;
 
 fun begin_main_target begin f = transaction (fn _ =>
   (fn Theory (Context.Theory thy) =>
@@ -505,14 +496,14 @@
     | _ => raise UNDEF));
 
 fun local_theory restricted target f =
-  local_theory' restricted target (K f) no_presentation;
+  local_theory' restricted target (K f) NONE;
 
 fun present_local_theory target g = present_transaction (fn _ =>
   (fn Theory gthy =>
         let val (finish, lthy) = Target_Context.switch_named_cmd target gthy;
         in (Theory (finish lthy), lthy) end
     | _ => raise UNDEF))
-  (presentation g);
+  (SOME g);
 
 
 (* proof transitions *)
@@ -641,8 +632,8 @@
 
 fun app int (tr as Transition {name, markers, trans, ...}) =
   setmp_thread_position tr
-    (Timing.protocol (name_of tr) (pos_of tr) (apply_trans int name markers trans)
-      ##> Option.map (fn UNDEF => ERROR (type_error tr) | exn => exn)
+    (Timing.protocol (name_of tr) (pos_of tr) (apply_capture int name markers trans)
+      ##> Option.map (fn Runtime.UNDEF => ERROR (type_error tr) | exn => exn)
       #> show_state);
 
 in
@@ -790,8 +781,7 @@
 
             val future_proof =
               Proof.future_proof (fn state =>
-                Execution.fork
-                  {name = "Toplevel.future_proof", pos = pos_of head_tr, pri = ~1}
+                Execution.fork {name = "Toplevel.future_proof", pos = pos_of head_tr, pri = ~1}
                   (fn () =>
                     let
                       val State ((Proof (prf, (_, orig_gthy)), _), prev_thy) = st';

--- a/src/Pure/PIDE/resources.ML	Thu Dec 29 22:14:12 2022 +0000
+++ b/src/Pure/PIDE/resources.ML	Thu Dec 29 22:14:25 2022 +0000
@@ -38,6 +38,7 @@
    {master: Path.T * SHA1.digest, text: string, theory_pos: Position.T,
     imports: (string * Position.T) list, keywords: Thy_Header.keywords}
   val read_file_node: string -> Path.T -> Path.T * Position.T -> Token.file
+  val read_file: Path.T -> Path.T * Position.T -> Token.file
   val parsed_files: (Path.T -> Path.T list) ->
     Token.file Exn.result list * Input.source -> theory -> Token.file list
   val parse_files: (Path.T -> Path.T list) -> (theory -> Token.file list) parser
@@ -330,7 +331,7 @@
   end;
 
 
-(* read_file_node *)
+(* read_file *)
 
 fun read_file_node file_node master_dir (src_path, pos) =
   let
@@ -358,6 +359,8 @@
   in {src_path = src_path, lines = lines, digest = digest, pos = Position.copy_id pos file_pos} end
   handle ERROR msg => error (msg ^ Position.here pos);
 
+val read_file = read_file_node "";
+
 
 (* load files *)
 
@@ -374,7 +377,7 @@
           [(pos, Markup.path (Path.implode_symbolic (master_dir + src_path))),
            (pos, Markup.language_path delimited)]);
       val _ = Position.reports reports;
-    in map (read_file_node "" master_dir o rpair pos) src_paths end
+    in map (read_file master_dir o rpair pos) src_paths end
   else map Exn.release files;
 
 fun parse_files make_paths =