src/Pure/Isar/toplevel.ML
changeset 70067 0cb8753bdb50
parent 70064 f8293bf510a0
child 70068 b9985133805d
     1.1 --- a/src/Pure/Isar/toplevel.ML	Sat Mar 09 13:35:49 2019 +0100
     1.2 +++ b/src/Pure/Isar/toplevel.ML	Sat Mar 09 23:57:07 2019 +0100
     1.3 @@ -8,8 +8,8 @@
     1.4  sig
     1.5    exception UNDEF
     1.6    type state
     1.7 +  val init_toplevel: unit -> state
     1.8    val theory_toplevel: theory -> state
     1.9 -  val init: unit -> state
    1.10    val is_toplevel: state -> bool
    1.11    val is_theory: state -> bool
    1.12    val is_proof: state -> bool
    1.13 @@ -128,8 +128,12 @@
    1.14  
    1.15  type node_presentation = node * Proof.context;
    1.16  
    1.17 -fun node_presentation0 node =
    1.18 -  (node, cases_proper_node Context.proof_of Proof.context_of node);
    1.19 +fun init_presentation () =
    1.20 +  Proof_Context.init_global (Theory.get_pure_bootstrap ());
    1.21 +
    1.22 +fun node_presentation node =
    1.23 +  (node, cases_node init_presentation Context.proof_of Proof.context_of node);
    1.24 +
    1.25  
    1.26  datatype state =
    1.27    State of node_presentation * theory option;
    1.28 @@ -138,13 +142,13 @@
    1.29  fun node_of (State ((node, _), _)) = node;
    1.30  fun previous_theory_of (State (_, prev_thy)) = prev_thy;
    1.31  
    1.32 -fun theory_toplevel thy =
    1.33 -  State (node_presentation0 (Theory (Context.Theory thy)), NONE);
    1.34 -
    1.35 -fun init () =
    1.36 +fun init_toplevel () =
    1.37    let val thy0 = Theory.get_pure () handle Fail _ => Context.the_global_context ();
    1.38    in State ((Toplevel, Proof_Context.init_global thy0), NONE) end;
    1.39  
    1.40 +fun theory_toplevel thy =
    1.41 +  State (node_presentation (Theory (Context.Theory thy)), NONE);
    1.42 +
    1.43  fun level state =
    1.44    (case node_of state of
    1.45      Toplevel => 0
    1.46 @@ -213,7 +217,7 @@
    1.47  
    1.48  fun presentation_state ctxt =
    1.49    (case Presentation_State.get ctxt of
    1.50 -    NONE => State (node_presentation0 (Theory (Context.Proof ctxt)), NONE)
    1.51 +    NONE => State (node_presentation (Theory (Context.Proof ctxt)), NONE)
    1.52    | SOME state => state);
    1.53  
    1.54  
    1.55 @@ -255,7 +259,7 @@
    1.56  
    1.57  fun apply_transaction f g node =
    1.58    let
    1.59 -    val node_pr = node_presentation0 node;
    1.60 +    val node_pr = node_presentation node;
    1.61      val context = cases_proper_node I (Context.Proof o Proof.context_of) node;
    1.62      fun state_error e node_pr' = (State (node_pr', get_theory node), e);
    1.63  
    1.64 @@ -287,12 +291,12 @@
    1.65  
    1.66  fun apply_tr _ (Init f) (State ((Toplevel, _), _)) =
    1.67        let val node = Theory (Context.Theory (Runtime.controlled_execution NONE f ()))
    1.68 -      in State (node_presentation0 node, NONE) end
    1.69 +      in State (node_presentation node, NONE) end
    1.70    | apply_tr _ Exit (State ((node as Theory (Context.Theory thy), _), _)) =
    1.71        let
    1.72          val State ((node', pr_ctxt), _) =
    1.73            node |> apply_transaction
    1.74 -            (fn _ => node_presentation0 (Theory (Context.Theory (Theory.end_theory thy))))
    1.75 +            (fn _ => node_presentation (Theory (Context.Theory (Theory.end_theory thy))))
    1.76              (K ());
    1.77        in State ((Toplevel, pr_ctxt), get_theory node') end
    1.78    | apply_tr int (Keep f) state =
    1.79 @@ -381,7 +385,7 @@
    1.80  
    1.81  fun present_transaction f g = add_trans (Transaction (f, g));
    1.82  fun transaction f = present_transaction f (K ());
    1.83 -fun transaction0 f = present_transaction (node_presentation0 oo f) (K ());
    1.84 +fun transaction0 f = present_transaction (node_presentation oo f) (K ());
    1.85  
    1.86  fun keep f = add_trans (Keep (fn _ => f));
    1.87  
    1.88 @@ -401,7 +405,7 @@
    1.89  (* theory transitions *)
    1.90  
    1.91  fun generic_theory f = transaction (fn _ =>
    1.92 -  (fn Theory gthy => node_presentation0 (Theory (f gthy))
    1.93 +  (fn Theory gthy => node_presentation (Theory (f gthy))
    1.94      | _ => raise UNDEF));
    1.95  
    1.96  fun theory' f = transaction (fn int =>
    1.97 @@ -410,7 +414,7 @@
    1.98          |> Sign.new_group
    1.99          |> f int
   1.100          |> Sign.reset_group;
   1.101 -      in node_presentation0 (Theory (Context.Theory thy')) end
   1.102 +      in node_presentation (Theory (Context.Theory thy')) end
   1.103      | _ => raise UNDEF));
   1.104  
   1.105  fun theory f = theory' (K f);
   1.106 @@ -488,7 +492,7 @@
   1.107              in (Theory gthy', ctxt') end
   1.108            else raise UNDEF
   1.109          end
   1.110 -    | Skipped_Proof (0, (gthy, _)) => node_presentation0 (Theory gthy)
   1.111 +    | Skipped_Proof (0, (gthy, _)) => node_presentation (Theory gthy)
   1.112      | _ => raise UNDEF));
   1.113  
   1.114  local
   1.115 @@ -741,7 +745,7 @@
   1.116                        val State ((Proof (prf, (_, orig_gthy)), _), prev_thy) = st';
   1.117                        val node' = Proof (Proof_Node.apply (K state) prf, (finish, orig_gthy));
   1.118                        val (result, result_state) =
   1.119 -                        State (node_presentation0 node', prev_thy)
   1.120 +                        State (node_presentation node', prev_thy)
   1.121                          |> fold_map (element_result keywords) body_elems ||> command end_tr;
   1.122                      in (Result_List result, presentation_context0 result_state) end))
   1.123                #> (fn (res, state') => state' |> put_result (Result_Future res));