# HG changeset patch
# User wenzelm
# Date 1518881800 -3600
# Node ID 10ff1f077119edb50fd6d4afd6bb089d7e293290
# Parent  3eb12473a8bd0a97656ce3adac73d7bed7b2671e
more tight presentation context: avoid storing full Toplevel.state;

diff -r 3eb12473a8bd -r 10ff1f077119 src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Sat Feb 17 15:17:17 2018 +0100
+++ b/src/Pure/Isar/toplevel.ML	Sat Feb 17 16:36:40 2018 +0100
@@ -178,15 +178,18 @@
   fun init _ = NONE;
 );
 
-fun presentation_context state =
+fun presentation_context0 state =
   (case try node_of state of
     SOME (Theory (_, SOME ctxt)) => ctxt
   | SOME node => cases_node Context.proof_of Proof.context_of node
   | NONE =>
       (case try Theory.get_pure () of
         SOME thy => Proof_Context.init_global thy
-      | NONE => raise UNDEF))
-  |> Presentation_State.put (SOME state);
+      | NONE => raise UNDEF));
+
+fun presentation_context (state as State (current, _)) =
+  presentation_context0 state
+  |> Presentation_State.put (SOME (State (current, NONE)));
 
 fun presentation_state ctxt =
   (case Presentation_State.get ctxt of
@@ -596,7 +599,7 @@
 fun transition int tr st =
   let
     val (st', opt_err) =
-      Context.setmp_generic_context (try (Context.Proof o presentation_context) st)
+      Context.setmp_generic_context (try (Context.Proof o presentation_context0) st)
         (fn () => app int tr st) ();
     val opt_err' = opt_err |> Option.map
       (fn Runtime.EXCURSION_FAIL exn_info => exn_info
@@ -720,7 +723,7 @@
                       val (result, result_state) =
                         State (SOME (Proof (prf', (finish, orig_gthy))), prev)
                         |> fold_map (element_result keywords) body_elems ||> command end_tr;
-                    in (Result_List result, presentation_context result_state) end))
+                    in (Result_List result, presentation_context0 result_state) end))
               #> (fn (res, state') => state' |> put_result (Result_Future res));
 
             val forked_proof =
@@ -733,7 +736,7 @@
               |> command (head_tr |> reset_trans |> forked_proof);
             val end_result = Result (end_tr, st'');
             val result =
-              Result_List [head_result, Result.get (presentation_context st''), end_result];
+              Result_List [head_result, Result.get (presentation_context0 st''), end_result];
           in (result, st'') end
       end;