# HG changeset patch
# User wenzelm
# Date 1672327049 -3600
# Node ID 0eb3ea050fa9906fbe8f1fbc2cfab8e96594d68e
# Parent  294004c907c751fd6b179bac179ddc47f448e02f
support asynchronous presentation commands, but not for "no_update" / "Keep", which is usually forked via "Toplevel.diag";

diff -r 294004c907c7 -r 0eb3ea050fa9 src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Thu Dec 29 15:54:49 2022 +0100
+++ b/src/Pure/Isar/toplevel.ML	Thu Dec 29 16:17:29 2022 +0100
@@ -139,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))
@@ -270,11 +270,15 @@
 
 local
 
-fun present_state g node_pr prev_thy =
+fun present_state fork g node_pr prev_thy =
   let
     val state = State (node_pr, (prev_thy, NONE));
-    val state' = State (node_pr, (prev_thy, Option.map (fn pr => pr state) g));
-  in state' end;
+    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;
 
 fun no_update f g state =
   Runtime.controlled_execution (try generic_theory_of state)
@@ -283,7 +287,7 @@
         val prev_thy = previous_theory_of state;
         val () = f state;
         val node_pr = node_presentation (node_of state);
-      in present_state g node_pr prev_thy end) ()
+      in present_state false g node_pr prev_thy end) ()
 
 fun update f g state =
   Runtime.controlled_execution (try generic_theory_of state)
@@ -291,7 +295,7 @@
       let
         val prev_thy = previous_theory_of state;
         val node_pr' = f (node_of state);
-      in present_state g node_pr' prev_thy end) ();
+      in present_state true g node_pr' prev_thy end) ();
 
 fun apply_tr int trans state =
   (case (trans, node_of state) of