clarified signature;
authorwenzelm
Sat Mar 09 23:57:07 2019 +0100 (5 weeks ago ago)
changeset 700670cb8753bdb50
parent 70066 6dc5506ad449
child 70068 b9985133805d
clarified signature;
src/Pure/Isar/isar_cmd.ML
src/Pure/Isar/toplevel.ML
src/Pure/PIDE/command.ML
src/Pure/PIDE/document.ML
src/Pure/Thy/thy_info.ML
src/Pure/Thy/thy_output.ML
src/Pure/theory.ML
     1.1 --- a/src/Pure/Isar/isar_cmd.ML	Sat Mar 09 13:35:49 2019 +0100
     1.2 +++ b/src/Pure/Isar/isar_cmd.ML	Sat Mar 09 23:57:07 2019 +0100
     1.3 @@ -195,7 +195,7 @@
     1.4  fun diag_state ctxt =
     1.5    (case Diag_State.get ctxt of
     1.6      SOME st => st
     1.7 -  | NONE => Toplevel.init ());
     1.8 +  | NONE => Toplevel.init_toplevel ());
     1.9  
    1.10  val diag_goal = Proof.goal o Toplevel.proof_of o diag_state;
    1.11  
     2.1 --- a/src/Pure/Isar/toplevel.ML	Sat Mar 09 13:35:49 2019 +0100
     2.2 +++ b/src/Pure/Isar/toplevel.ML	Sat Mar 09 23:57:07 2019 +0100
     2.3 @@ -8,8 +8,8 @@
     2.4  sig
     2.5    exception UNDEF
     2.6    type state
     2.7 +  val init_toplevel: unit -> state
     2.8    val theory_toplevel: theory -> state
     2.9 -  val init: unit -> state
    2.10    val is_toplevel: state -> bool
    2.11    val is_theory: state -> bool
    2.12    val is_proof: state -> bool
    2.13 @@ -128,8 +128,12 @@
    2.14  
    2.15  type node_presentation = node * Proof.context;
    2.16  
    2.17 -fun node_presentation0 node =
    2.18 -  (node, cases_proper_node Context.proof_of Proof.context_of node);
    2.19 +fun init_presentation () =
    2.20 +  Proof_Context.init_global (Theory.get_pure_bootstrap ());
    2.21 +
    2.22 +fun node_presentation node =
    2.23 +  (node, cases_node init_presentation Context.proof_of Proof.context_of node);
    2.24 +
    2.25  
    2.26  datatype state =
    2.27    State of node_presentation * theory option;
    2.28 @@ -138,13 +142,13 @@
    2.29  fun node_of (State ((node, _), _)) = node;
    2.30  fun previous_theory_of (State (_, prev_thy)) = prev_thy;
    2.31  
    2.32 -fun theory_toplevel thy =
    2.33 -  State (node_presentation0 (Theory (Context.Theory thy)), NONE);
    2.34 -
    2.35 -fun init () =
    2.36 +fun init_toplevel () =
    2.37    let val thy0 = Theory.get_pure () handle Fail _ => Context.the_global_context ();
    2.38    in State ((Toplevel, Proof_Context.init_global thy0), NONE) end;
    2.39  
    2.40 +fun theory_toplevel thy =
    2.41 +  State (node_presentation (Theory (Context.Theory thy)), NONE);
    2.42 +
    2.43  fun level state =
    2.44    (case node_of state of
    2.45      Toplevel => 0
    2.46 @@ -213,7 +217,7 @@
    2.47  
    2.48  fun presentation_state ctxt =
    2.49    (case Presentation_State.get ctxt of
    2.50 -    NONE => State (node_presentation0 (Theory (Context.Proof ctxt)), NONE)
    2.51 +    NONE => State (node_presentation (Theory (Context.Proof ctxt)), NONE)
    2.52    | SOME state => state);
    2.53  
    2.54  
    2.55 @@ -255,7 +259,7 @@
    2.56  
    2.57  fun apply_transaction f g node =
    2.58    let
    2.59 -    val node_pr = node_presentation0 node;
    2.60 +    val node_pr = node_presentation node;
    2.61      val context = cases_proper_node I (Context.Proof o Proof.context_of) node;
    2.62      fun state_error e node_pr' = (State (node_pr', get_theory node), e);
    2.63  
    2.64 @@ -287,12 +291,12 @@
    2.65  
    2.66  fun apply_tr _ (Init f) (State ((Toplevel, _), _)) =
    2.67        let val node = Theory (Context.Theory (Runtime.controlled_execution NONE f ()))
    2.68 -      in State (node_presentation0 node, NONE) end
    2.69 +      in State (node_presentation node, NONE) end
    2.70    | apply_tr _ Exit (State ((node as Theory (Context.Theory thy), _), _)) =
    2.71        let
    2.72          val State ((node', pr_ctxt), _) =
    2.73            node |> apply_transaction
    2.74 -            (fn _ => node_presentation0 (Theory (Context.Theory (Theory.end_theory thy))))
    2.75 +            (fn _ => node_presentation (Theory (Context.Theory (Theory.end_theory thy))))
    2.76              (K ());
    2.77        in State ((Toplevel, pr_ctxt), get_theory node') end
    2.78    | apply_tr int (Keep f) state =
    2.79 @@ -381,7 +385,7 @@
    2.80  
    2.81  fun present_transaction f g = add_trans (Transaction (f, g));
    2.82  fun transaction f = present_transaction f (K ());
    2.83 -fun transaction0 f = present_transaction (node_presentation0 oo f) (K ());
    2.84 +fun transaction0 f = present_transaction (node_presentation oo f) (K ());
    2.85  
    2.86  fun keep f = add_trans (Keep (fn _ => f));
    2.87  
    2.88 @@ -401,7 +405,7 @@
    2.89  (* theory transitions *)
    2.90  
    2.91  fun generic_theory f = transaction (fn _ =>
    2.92 -  (fn Theory gthy => node_presentation0 (Theory (f gthy))
    2.93 +  (fn Theory gthy => node_presentation (Theory (f gthy))
    2.94      | _ => raise UNDEF));
    2.95  
    2.96  fun theory' f = transaction (fn int =>
    2.97 @@ -410,7 +414,7 @@
    2.98          |> Sign.new_group
    2.99          |> f int
   2.100          |> Sign.reset_group;
   2.101 -      in node_presentation0 (Theory (Context.Theory thy')) end
   2.102 +      in node_presentation (Theory (Context.Theory thy')) end
   2.103      | _ => raise UNDEF));
   2.104  
   2.105  fun theory f = theory' (K f);
   2.106 @@ -488,7 +492,7 @@
   2.107              in (Theory gthy', ctxt') end
   2.108            else raise UNDEF
   2.109          end
   2.110 -    | Skipped_Proof (0, (gthy, _)) => node_presentation0 (Theory gthy)
   2.111 +    | Skipped_Proof (0, (gthy, _)) => node_presentation (Theory gthy)
   2.112      | _ => raise UNDEF));
   2.113  
   2.114  local
   2.115 @@ -741,7 +745,7 @@
   2.116                        val State ((Proof (prf, (_, orig_gthy)), _), prev_thy) = st';
   2.117                        val node' = Proof (Proof_Node.apply (K state) prf, (finish, orig_gthy));
   2.118                        val (result, result_state) =
   2.119 -                        State (node_presentation0 node', prev_thy)
   2.120 +                        State (node_presentation node', prev_thy)
   2.121                          |> fold_map (element_result keywords) body_elems ||> command end_tr;
   2.122                      in (Result_List result, presentation_context0 result_state) end))
   2.123                #> (fn (res, state') => state' |> put_result (Result_Future res));
     3.1 --- a/src/Pure/PIDE/command.ML	Sat Mar 09 13:35:49 2019 +0100
     3.2 +++ b/src/Pure/PIDE/command.ML	Sat Mar 09 23:57:07 2019 +0100
     3.3 @@ -175,7 +175,7 @@
     3.4    command = Toplevel.empty,
     3.5    state =
     3.6      (case opt_thy of
     3.7 -      NONE => Toplevel.init ()
     3.8 +      NONE => Toplevel.init_toplevel ()
     3.9      | SOME thy => Toplevel.theory_toplevel thy)};
    3.10  
    3.11  datatype eval =
     4.1 --- a/src/Pure/PIDE/document.ML	Sat Mar 09 13:35:49 2019 +0100
     4.2 +++ b/src/Pure/PIDE/document.ML	Sat Mar 09 23:57:07 2019 +0100
     4.3 @@ -575,7 +575,7 @@
     4.4      val imports = #imports header;
     4.5  
     4.6      fun maybe_eval_result eval = Command.eval_result_state eval
     4.7 -      handle Fail _ => Toplevel.init ();
     4.8 +      handle Fail _ => Toplevel.init_toplevel ();
     4.9  
    4.10      fun maybe_end_theory pos st = SOME (Toplevel.end_theory pos st)
    4.11        handle ERROR msg => (Output.error_message msg; NONE);
    4.12 @@ -586,7 +586,7 @@
    4.13            NONE =>
    4.14              maybe_end_theory pos
    4.15                (case get_result (snd (the (AList.lookup (op =) deps import))) of
    4.16 -                NONE => Toplevel.init ()
    4.17 +                NONE => Toplevel.init_toplevel ()
    4.18                | SOME (_, eval) => maybe_eval_result eval)
    4.19          | some => some)
    4.20          |> Option.map (fn thy => (thy, (pos, Theory.get_markup thy))));
     5.1 --- a/src/Pure/Thy/thy_info.ML	Sat Mar 09 13:35:49 2019 +0100
     5.2 +++ b/src/Pure/Thy/thy_info.ML	Sat Mar 09 23:57:07 2019 +0100
     5.3 @@ -295,7 +295,7 @@
     5.4        in (results, (st', pos')) end;
     5.5  
     5.6      val (results, (end_state, end_pos)) =
     5.7 -      fold_map element_result elements (Toplevel.init (), Position.none);
     5.8 +      fold_map element_result elements (Toplevel.init_toplevel (), Position.none);
     5.9  
    5.10      val thy = Toplevel.end_theory end_pos end_state;
    5.11    in (results, thy) end;
    5.12 @@ -455,7 +455,7 @@
    5.13        Outer_Syntax.parse thy pos txt
    5.14        |> map (Toplevel.modify_init (K thy));
    5.15      val end_pos = if null trs then pos else Toplevel.pos_of (List.last trs);
    5.16 -    val end_state = fold (Toplevel.command_exception true) trs (Toplevel.init ());
    5.17 +    val end_state = fold (Toplevel.command_exception true) trs (Toplevel.init_toplevel ());
    5.18    in Toplevel.end_theory end_pos end_state end;
    5.19  
    5.20  
     6.1 --- a/src/Pure/Thy/thy_output.ML	Sat Mar 09 13:35:49 2019 +0100
     6.2 +++ b/src/Pure/Thy/thy_output.ML	Sat Mar 09 23:57:07 2019 +0100
     6.3 @@ -449,7 +449,7 @@
     6.4    in
     6.5      if length command_results = length spans then
     6.6        ((NONE, []), NONE, true, [], (I, I))
     6.7 -      |> present (Toplevel.init ()) (spans ~~ command_results)
     6.8 +      |> present (Toplevel.init_toplevel ()) (spans ~~ command_results)
     6.9        |> present_trailer
    6.10        |> rev
    6.11      else error "Messed-up outer syntax for presentation"
     7.1 --- a/src/Pure/theory.ML	Sat Mar 09 13:35:49 2019 +0100
     7.2 +++ b/src/Pure/theory.ML	Sat Mar 09 23:57:07 2019 +0100
     7.3 @@ -13,6 +13,7 @@
     7.4    val local_setup: (Proof.context -> Proof.context) -> unit
     7.5    val install_pure: theory -> unit
     7.6    val get_pure: unit -> theory
     7.7 +  val get_pure_bootstrap: unit -> theory
     7.8    val get_markup: theory -> Markup.T
     7.9    val check: {long: bool} -> Proof.context -> string * Position.T -> theory
    7.10    val axiom_table: theory -> term Name_Space.table
    7.11 @@ -59,6 +60,11 @@
    7.12      SOME thy => thy
    7.13    | NONE => raise Fail "Theory Pure not present");
    7.14  
    7.15 +fun get_pure_bootstrap () =
    7.16 +  (case Single_Assignment.peek pure of
    7.17 +    SOME thy => thy
    7.18 +  | NONE => Context.the_global_context ());
    7.19 +
    7.20  
    7.21  
    7.22  (** datatype thy **)