--- a/src/Pure/Isar/isar_cmd.ML Sat Mar 09 13:35:49 2019 +0100
+++ b/src/Pure/Isar/isar_cmd.ML Sat Mar 09 23:57:07 2019 +0100
@@ -195,7 +195,7 @@
fun diag_state ctxt =
(case Diag_State.get ctxt of
SOME st => st
- | NONE => Toplevel.init ());
+ | NONE => Toplevel.init_toplevel ());
val diag_goal = Proof.goal o Toplevel.proof_of o diag_state;
--- a/src/Pure/Isar/toplevel.ML Sat Mar 09 13:35:49 2019 +0100
+++ b/src/Pure/Isar/toplevel.ML Sat Mar 09 23:57:07 2019 +0100
@@ -8,8 +8,8 @@
sig
exception UNDEF
type state
+ val init_toplevel: unit -> state
val theory_toplevel: theory -> state
- val init: unit -> state
val is_toplevel: state -> bool
val is_theory: state -> bool
val is_proof: state -> bool
@@ -128,8 +128,12 @@
type node_presentation = node * Proof.context;
-fun node_presentation0 node =
- (node, cases_proper_node Context.proof_of Proof.context_of node);
+fun init_presentation () =
+ Proof_Context.init_global (Theory.get_pure_bootstrap ());
+
+fun node_presentation node =
+ (node, cases_node init_presentation Context.proof_of Proof.context_of node);
+
datatype state =
State of node_presentation * theory option;
@@ -138,13 +142,13 @@
fun node_of (State ((node, _), _)) = node;
fun previous_theory_of (State (_, prev_thy)) = prev_thy;
-fun theory_toplevel thy =
- State (node_presentation0 (Theory (Context.Theory thy)), NONE);
-
-fun init () =
+fun init_toplevel () =
let val thy0 = Theory.get_pure () handle Fail _ => Context.the_global_context ();
in State ((Toplevel, Proof_Context.init_global thy0), NONE) end;
+fun theory_toplevel thy =
+ State (node_presentation (Theory (Context.Theory thy)), NONE);
+
fun level state =
(case node_of state of
Toplevel => 0
@@ -213,7 +217,7 @@
fun presentation_state ctxt =
(case Presentation_State.get ctxt of
- NONE => State (node_presentation0 (Theory (Context.Proof ctxt)), NONE)
+ NONE => State (node_presentation (Theory (Context.Proof ctxt)), NONE)
| SOME state => state);
@@ -255,7 +259,7 @@
fun apply_transaction f g node =
let
- val node_pr = node_presentation0 node;
+ val node_pr = node_presentation node;
val context = cases_proper_node I (Context.Proof o Proof.context_of) node;
fun state_error e node_pr' = (State (node_pr', get_theory node), e);
@@ -287,12 +291,12 @@
fun apply_tr _ (Init f) (State ((Toplevel, _), _)) =
let val node = Theory (Context.Theory (Runtime.controlled_execution NONE f ()))
- in State (node_presentation0 node, NONE) end
+ in State (node_presentation node, NONE) end
| apply_tr _ Exit (State ((node as Theory (Context.Theory thy), _), _)) =
let
val State ((node', pr_ctxt), _) =
node |> apply_transaction
- (fn _ => node_presentation0 (Theory (Context.Theory (Theory.end_theory thy))))
+ (fn _ => node_presentation (Theory (Context.Theory (Theory.end_theory thy))))
(K ());
in State ((Toplevel, pr_ctxt), get_theory node') end
| apply_tr int (Keep f) state =
@@ -381,7 +385,7 @@
fun present_transaction f g = add_trans (Transaction (f, g));
fun transaction f = present_transaction f (K ());
-fun transaction0 f = present_transaction (node_presentation0 oo f) (K ());
+fun transaction0 f = present_transaction (node_presentation oo f) (K ());
fun keep f = add_trans (Keep (fn _ => f));
@@ -401,7 +405,7 @@
(* theory transitions *)
fun generic_theory f = transaction (fn _ =>
- (fn Theory gthy => node_presentation0 (Theory (f gthy))
+ (fn Theory gthy => node_presentation (Theory (f gthy))
| _ => raise UNDEF));
fun theory' f = transaction (fn int =>
@@ -410,7 +414,7 @@
|> Sign.new_group
|> f int
|> Sign.reset_group;
- in node_presentation0 (Theory (Context.Theory thy')) end
+ in node_presentation (Theory (Context.Theory thy')) end
| _ => raise UNDEF));
fun theory f = theory' (K f);
@@ -488,7 +492,7 @@
in (Theory gthy', ctxt') end
else raise UNDEF
end
- | Skipped_Proof (0, (gthy, _)) => node_presentation0 (Theory gthy)
+ | Skipped_Proof (0, (gthy, _)) => node_presentation (Theory gthy)
| _ => raise UNDEF));
local
@@ -741,7 +745,7 @@
val State ((Proof (prf, (_, orig_gthy)), _), prev_thy) = st';
val node' = Proof (Proof_Node.apply (K state) prf, (finish, orig_gthy));
val (result, result_state) =
- State (node_presentation0 node', prev_thy)
+ State (node_presentation node', prev_thy)
|> fold_map (element_result keywords) body_elems ||> command end_tr;
in (Result_List result, presentation_context0 result_state) end))
#> (fn (res, state') => state' |> put_result (Result_Future res));
--- a/src/Pure/PIDE/command.ML Sat Mar 09 13:35:49 2019 +0100
+++ b/src/Pure/PIDE/command.ML Sat Mar 09 23:57:07 2019 +0100
@@ -175,7 +175,7 @@
command = Toplevel.empty,
state =
(case opt_thy of
- NONE => Toplevel.init ()
+ NONE => Toplevel.init_toplevel ()
| SOME thy => Toplevel.theory_toplevel thy)};
datatype eval =
--- a/src/Pure/PIDE/document.ML Sat Mar 09 13:35:49 2019 +0100
+++ b/src/Pure/PIDE/document.ML Sat Mar 09 23:57:07 2019 +0100
@@ -575,7 +575,7 @@
val imports = #imports header;
fun maybe_eval_result eval = Command.eval_result_state eval
- handle Fail _ => Toplevel.init ();
+ handle Fail _ => Toplevel.init_toplevel ();
fun maybe_end_theory pos st = SOME (Toplevel.end_theory pos st)
handle ERROR msg => (Output.error_message msg; NONE);
@@ -586,7 +586,7 @@
NONE =>
maybe_end_theory pos
(case get_result (snd (the (AList.lookup (op =) deps import))) of
- NONE => Toplevel.init ()
+ NONE => Toplevel.init_toplevel ()
| SOME (_, eval) => maybe_eval_result eval)
| some => some)
|> Option.map (fn thy => (thy, (pos, Theory.get_markup thy))));
--- a/src/Pure/Thy/thy_info.ML Sat Mar 09 13:35:49 2019 +0100
+++ b/src/Pure/Thy/thy_info.ML Sat Mar 09 23:57:07 2019 +0100
@@ -295,7 +295,7 @@
in (results, (st', pos')) end;
val (results, (end_state, end_pos)) =
- fold_map element_result elements (Toplevel.init (), Position.none);
+ fold_map element_result elements (Toplevel.init_toplevel (), Position.none);
val thy = Toplevel.end_theory end_pos end_state;
in (results, thy) end;
@@ -455,7 +455,7 @@
Outer_Syntax.parse thy pos txt
|> map (Toplevel.modify_init (K thy));
val end_pos = if null trs then pos else Toplevel.pos_of (List.last trs);
- val end_state = fold (Toplevel.command_exception true) trs (Toplevel.init ());
+ val end_state = fold (Toplevel.command_exception true) trs (Toplevel.init_toplevel ());
in Toplevel.end_theory end_pos end_state end;
--- a/src/Pure/Thy/thy_output.ML Sat Mar 09 13:35:49 2019 +0100
+++ b/src/Pure/Thy/thy_output.ML Sat Mar 09 23:57:07 2019 +0100
@@ -449,7 +449,7 @@
in
if length command_results = length spans then
((NONE, []), NONE, true, [], (I, I))
- |> present (Toplevel.init ()) (spans ~~ command_results)
+ |> present (Toplevel.init_toplevel ()) (spans ~~ command_results)
|> present_trailer
|> rev
else error "Messed-up outer syntax for presentation"
--- a/src/Pure/theory.ML Sat Mar 09 13:35:49 2019 +0100
+++ b/src/Pure/theory.ML Sat Mar 09 23:57:07 2019 +0100
@@ -13,6 +13,7 @@
val local_setup: (Proof.context -> Proof.context) -> unit
val install_pure: theory -> unit
val get_pure: unit -> theory
+ val get_pure_bootstrap: unit -> theory
val get_markup: theory -> Markup.T
val check: {long: bool} -> Proof.context -> string * Position.T -> theory
val axiom_table: theory -> term Name_Space.table
@@ -59,6 +60,11 @@
SOME thy => thy
| NONE => raise Fail "Theory Pure not present");
+fun get_pure_bootstrap () =
+ (case Single_Assignment.peek pure of
+ SOME thy => thy
+ | NONE => Context.the_global_context ());
+
(** datatype thy **)