more tight presentation context: avoid storing full Toplevel.state;
authorwenzelm
Sat Feb 17 16:36:40 2018 +0100 (16 months ago ago)
changeset 6764210ff1f077119
parent 67641 3eb12473a8bd
child 67643 b846f7a11fda
more tight presentation context: avoid storing full Toplevel.state;
src/Pure/Isar/toplevel.ML
     1.1 --- a/src/Pure/Isar/toplevel.ML	Sat Feb 17 15:17:17 2018 +0100
     1.2 +++ b/src/Pure/Isar/toplevel.ML	Sat Feb 17 16:36:40 2018 +0100
     1.3 @@ -178,15 +178,18 @@
     1.4    fun init _ = NONE;
     1.5  );
     1.6  
     1.7 -fun presentation_context state =
     1.8 +fun presentation_context0 state =
     1.9    (case try node_of state of
    1.10      SOME (Theory (_, SOME ctxt)) => ctxt
    1.11    | SOME node => cases_node Context.proof_of Proof.context_of node
    1.12    | NONE =>
    1.13        (case try Theory.get_pure () of
    1.14          SOME thy => Proof_Context.init_global thy
    1.15 -      | NONE => raise UNDEF))
    1.16 -  |> Presentation_State.put (SOME state);
    1.17 +      | NONE => raise UNDEF));
    1.18 +
    1.19 +fun presentation_context (state as State (current, _)) =
    1.20 +  presentation_context0 state
    1.21 +  |> Presentation_State.put (SOME (State (current, NONE)));
    1.22  
    1.23  fun presentation_state ctxt =
    1.24    (case Presentation_State.get ctxt of
    1.25 @@ -596,7 +599,7 @@
    1.26  fun transition int tr st =
    1.27    let
    1.28      val (st', opt_err) =
    1.29 -      Context.setmp_generic_context (try (Context.Proof o presentation_context) st)
    1.30 +      Context.setmp_generic_context (try (Context.Proof o presentation_context0) st)
    1.31          (fn () => app int tr st) ();
    1.32      val opt_err' = opt_err |> Option.map
    1.33        (fn Runtime.EXCURSION_FAIL exn_info => exn_info
    1.34 @@ -720,7 +723,7 @@
    1.35                        val (result, result_state) =
    1.36                          State (SOME (Proof (prf', (finish, orig_gthy))), prev)
    1.37                          |> fold_map (element_result keywords) body_elems ||> command end_tr;
    1.38 -                    in (Result_List result, presentation_context result_state) end))
    1.39 +                    in (Result_List result, presentation_context0 result_state) end))
    1.40                #> (fn (res, state') => state' |> put_result (Result_Future res));
    1.41  
    1.42              val forked_proof =
    1.43 @@ -733,7 +736,7 @@
    1.44                |> command (head_tr |> reset_trans |> forked_proof);
    1.45              val end_result = Result (end_tr, st'');
    1.46              val result =
    1.47 -              Result_List [head_result, Result.get (presentation_context st''), end_result];
    1.48 +              Result_List [head_result, Result.get (presentation_context0 st''), end_result];
    1.49            in (result, st'') end
    1.50        end;
    1.51