# HG changeset patch # User wenzelm # Date 1552172227 -3600 # Node ID 0cb8753bdb50a7c957786a5977e5b044df906be5 # Parent 6dc5506ad44971ab6046b4a179d1d7f47bffa605 clarified signature; diff -r 6dc5506ad449 -r 0cb8753bdb50 src/Pure/Isar/isar_cmd.ML --- 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; diff -r 6dc5506ad449 -r 0cb8753bdb50 src/Pure/Isar/toplevel.ML --- 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)); diff -r 6dc5506ad449 -r 0cb8753bdb50 src/Pure/PIDE/command.ML --- 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 = diff -r 6dc5506ad449 -r 0cb8753bdb50 src/Pure/PIDE/document.ML --- 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)))); diff -r 6dc5506ad449 -r 0cb8753bdb50 src/Pure/Thy/thy_info.ML --- 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; diff -r 6dc5506ad449 -r 0cb8753bdb50 src/Pure/Thy/thy_output.ML --- 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" diff -r 6dc5506ad449 -r 0cb8753bdb50 src/Pure/theory.ML --- 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 **)