src/Pure/Isar/toplevel.ML
changeset 67381 146757999c8d
parent 67376 d5007d93bcc6
child 67390 a256051dd3d6
     1.1 --- a/src/Pure/Isar/toplevel.ML	Mon Jan 08 22:36:02 2018 +0100
     1.2 +++ b/src/Pure/Isar/toplevel.ML	Mon Jan 08 23:45:43 2018 +0100
     1.3 @@ -16,7 +16,6 @@
     1.4    val is_proof: state -> bool
     1.5    val is_skipped_proof: state -> bool
     1.6    val level: state -> int
     1.7 -  val presentation_context_of: state -> Proof.context
     1.8    val previous_context_of: state -> Proof.context option
     1.9    val context_of: state -> Proof.context
    1.10    val generic_theory_of: state -> generic_theory
    1.11 @@ -24,6 +23,8 @@
    1.12    val proof_of: state -> Proof.state
    1.13    val proof_position_of: state -> int
    1.14    val end_theory: Position.T -> state -> theory
    1.15 +  val presentation_context: state -> Proof.context
    1.16 +  val presentation_state: Proof.context -> state
    1.17    val pretty_context: state -> Pretty.T list
    1.18    val pretty_state: state -> Pretty.T list
    1.19    val string_of_state: state -> string
    1.20 @@ -154,12 +155,6 @@
    1.21  
    1.22  fun node_case f g state = cases_node f g (node_of state);
    1.23  
    1.24 -fun presentation_context_of state =
    1.25 -  (case try node_of state of
    1.26 -    SOME (Theory (_, SOME ctxt)) => ctxt
    1.27 -  | SOME node => context_node node
    1.28 -  | NONE => raise UNDEF);
    1.29 -
    1.30  fun previous_context_of (State (_, NONE)) = NONE
    1.31    | previous_context_of (State (_, SOME prev)) = SOME (context_node prev);
    1.32  
    1.33 @@ -178,6 +173,30 @@
    1.34    | end_theory pos (State (SOME _, _)) = error ("Unfinished theory" ^ Position.here pos);
    1.35  
    1.36  
    1.37 +(* presentation context *)
    1.38 +
    1.39 +structure Presentation_State = Proof_Data
    1.40 +(
    1.41 +  type T = state option;
    1.42 +  fun init _ = NONE;
    1.43 +);
    1.44 +
    1.45 +fun presentation_context state =
    1.46 +  (case try node_of state of
    1.47 +    SOME (Theory (_, SOME ctxt)) => ctxt
    1.48 +  | SOME node => context_node node
    1.49 +  | NONE =>
    1.50 +      (case try Theory.get_pure () of
    1.51 +        SOME thy => Proof_Context.init_global thy
    1.52 +      | NONE => raise UNDEF))
    1.53 +  |> Presentation_State.put (SOME state);
    1.54 +
    1.55 +fun presentation_state ctxt =
    1.56 +  (case Presentation_State.get ctxt of
    1.57 +    NONE => generic_theory_toplevel (Context.Proof ctxt)
    1.58 +  | SOME state => state);
    1.59 +
    1.60 +
    1.61  (* print state *)
    1.62  
    1.63  fun pretty_context state =
    1.64 @@ -580,7 +599,7 @@
    1.65  fun transition int tr st =
    1.66    let
    1.67      val (st', opt_err) =
    1.68 -      Context.setmp_generic_context (try (Context.Proof o presentation_context_of) st)
    1.69 +      Context.setmp_generic_context (try (Context.Proof o presentation_context) st)
    1.70          (fn () => app int tr st) ();
    1.71      val opt_err' = opt_err |> Option.map
    1.72        (fn Runtime.EXCURSION_FAIL exn_info => exn_info
    1.73 @@ -704,7 +723,7 @@
    1.74                        val (result, result_state) =
    1.75                          State (SOME (Proof (prf', (finish, orig_gthy))), prev)
    1.76                          |> fold_map (element_result keywords) body_elems ||> command end_tr;
    1.77 -                    in (Result_List result, presentation_context_of result_state) end))
    1.78 +                    in (Result_List result, presentation_context result_state) end))
    1.79                #> (fn (res, state') => state' |> put_result (Result_Future res));
    1.80  
    1.81              val forked_proof =
    1.82 @@ -717,7 +736,7 @@
    1.83                |> command (head_tr |> reset_trans |> forked_proof);
    1.84              val end_result = Result (end_tr, st'');
    1.85              val result =
    1.86 -              Result_List [head_result, Result.get (presentation_context_of st''), end_result];
    1.87 +              Result_List [head_result, Result.get (presentation_context st''), end_result];
    1.88            in (result, st'') end
    1.89        end;
    1.90