clarified implicit Pure.thy;
authorwenzelm
Mon Jan 08 22:36:02 2018 +0100 (16 months ago)
changeset 673808bef51521f21
parent 67379 c2dfc510a38c
child 67381 146757999c8d
clarified implicit Pure.thy;
src/Pure/ML/ml_pp.ML
src/Pure/PIDE/document.ML
src/Pure/Thy/thy_info.ML
src/Pure/Tools/build.scala
src/Pure/theory.ML
     1.1 --- a/src/Pure/ML/ml_pp.ML	Mon Jan 08 16:45:30 2018 +0100
     1.2 +++ b/src/Pure/ML/ml_pp.ML	Mon Jan 08 22:36:02 2018 +0100
     1.3 @@ -12,19 +12,19 @@
     1.4  
     1.5  val _ =
     1.6    ML_system_pp (fn depth => fn _ =>
     1.7 -    ML_Pretty.to_polyml o Pretty.to_ML depth o Proof_Display.pp_thm Thy_Info.pure_theory);
     1.8 +    ML_Pretty.to_polyml o Pretty.to_ML depth o Proof_Display.pp_thm Theory.get_pure);
     1.9  
    1.10  val _ =
    1.11    ML_system_pp (fn depth => fn _ =>
    1.12 -    ML_Pretty.to_polyml o Pretty.to_ML depth o Proof_Display.pp_cterm Thy_Info.pure_theory);
    1.13 +    ML_Pretty.to_polyml o Pretty.to_ML depth o Proof_Display.pp_cterm Theory.get_pure);
    1.14  
    1.15  val _ =
    1.16    ML_system_pp (fn depth => fn _ =>
    1.17 -    ML_Pretty.to_polyml o Pretty.to_ML depth o Proof_Display.pp_ctyp Thy_Info.pure_theory);
    1.18 +    ML_Pretty.to_polyml o Pretty.to_ML depth o Proof_Display.pp_ctyp Theory.get_pure);
    1.19  
    1.20  val _ =
    1.21    ML_system_pp (fn depth => fn _ =>
    1.22 -    ML_Pretty.to_polyml o Pretty.to_ML depth o Proof_Display.pp_typ Thy_Info.pure_theory);
    1.23 +    ML_Pretty.to_polyml o Pretty.to_ML depth o Proof_Display.pp_typ Theory.get_pure);
    1.24  
    1.25  
    1.26  local
     2.1 --- a/src/Pure/PIDE/document.ML	Mon Jan 08 16:45:30 2018 +0100
     2.2 +++ b/src/Pure/PIDE/document.ML	Mon Jan 08 22:36:02 2018 +0100
     2.3 @@ -574,7 +574,7 @@
     2.4          |> Option.map (fn thy => (thy, (pos, Theory.get_markup thy))));
     2.5  
     2.6      val parents =
     2.7 -      if null parents_reports then [Thy_Info.pure_theory ()] else map #1 parents_reports;
     2.8 +      if null parents_reports then [Theory.get_pure ()] else map #1 parents_reports;
     2.9      val _ = Position.reports (map #2 parents_reports);
    2.10    in Resources.begin_theory master_dir header parents end;
    2.11  
     3.1 --- a/src/Pure/Thy/thy_info.ML	Mon Jan 08 16:45:30 2018 +0100
     3.2 +++ b/src/Pure/Thy/thy_info.ML	Mon Jan 08 22:36:02 2018 +0100
     3.3 @@ -10,7 +10,6 @@
     3.4    val get_names: unit -> string list
     3.5    val lookup_theory: string -> theory option
     3.6    val get_theory: string -> theory
     3.7 -  val pure_theory: unit -> theory
     3.8    val master_directory: string -> Path.T
     3.9    val remove_thy: string -> unit
    3.10    val use_theories:
    3.11 @@ -102,8 +101,6 @@
    3.12      SOME theory => theory
    3.13    | _ => error ("Theory loader: undefined entry for theory " ^ quote name));
    3.14  
    3.15 -fun pure_theory () = get_theory Context.PureN;
    3.16 -
    3.17  val get_imports = Resources.imports_of o get_theory;
    3.18  
    3.19  
     4.1 --- a/src/Pure/Tools/build.scala	Mon Jan 08 16:45:30 2018 +0100
     4.2 +++ b/src/Pure/Tools/build.scala	Mon Jan 08 22:36:02 2018 +0100
     4.3 @@ -265,7 +265,8 @@
     4.4            val eval =
     4.5              "Command_Line.tool0 (fn () => (" +
     4.6              "Build.build " + ML_Syntax.print_string_bytes(File.standard_path(args_file)) +
     4.7 -            (if (do_output) "; " + save_heap else "") + "));"
     4.8 +            (if (Sessions.is_pure(name)) "; Theory.install_pure (Thy_Info.get_theory Context.PureN)"
     4.9 +             else "") + (if (do_output) "; " + save_heap else "") + "));"
    4.10  
    4.11            val process =
    4.12              if (Sessions.is_pure(name)) {
     5.1 --- a/src/Pure/theory.ML	Mon Jan 08 16:45:30 2018 +0100
     5.2 +++ b/src/Pure/theory.ML	Mon Jan 08 22:36:02 2018 +0100
     5.3 @@ -11,6 +11,8 @@
     5.4    val nodes_of: theory -> theory list
     5.5    val setup: (theory -> theory) -> unit
     5.6    val local_setup: (Proof.context -> Proof.context) -> unit
     5.7 +  val get_pure: unit -> theory
     5.8 +  val install_pure: theory -> unit
     5.9    val get_markup: theory -> Markup.T
    5.10    val check: Proof.context -> string * Position.T -> theory
    5.11    val axiom_table: theory -> term Name_Space.table
    5.12 @@ -45,6 +47,10 @@
    5.13  fun setup f = Context.>> (Context.map_theory f);
    5.14  fun local_setup f = Context.>> (Context.map_proof f);
    5.15  
    5.16 +val pure: theory Single_Assignment.var = Single_Assignment.var "pure";
    5.17 +fun get_pure () = the (Single_Assignment.peek pure);
    5.18 +fun install_pure thy = Single_Assignment.assign pure thy;
    5.19 +
    5.20  
    5.21  
    5.22  (** datatype thy **)