late setup of Pure and CPure;
authorwenzelm
Wed Jul 29 15:38:08 1998 +0200 (1998-07-29)
changeset 5211c02b0c727780
parent 5210 54aaa779b6b4
child 5212 2bc5b5cf0516
late setup of Pure and CPure;
src/Pure/ROOT.ML
src/Pure/Thy/thy_info.ML
src/Pure/pure.ML
     1.1 --- a/src/Pure/ROOT.ML	Tue Jul 28 17:05:34 1998 +0200
     1.2 +++ b/src/Pure/ROOT.ML	Wed Jul 29 15:38:08 1998 +0200
     1.3 @@ -46,13 +46,14 @@
     1.4  use "tactic.ML";
     1.5  use "goals.ML";
     1.6  use "axclass.ML";
     1.7 -use "pure.ML";
     1.8  
     1.9  (*theory parser and loader*)
    1.10  cd "Thy";
    1.11  use "ROOT.ML";
    1.12  cd "..";
    1.13  
    1.14 +use "pure.ML";
    1.15 +
    1.16  use "install_pp.ML";
    1.17  
    1.18  (*if true then some packages won't be too serious about actually proving things*)
     2.1 --- a/src/Pure/Thy/thy_info.ML	Tue Jul 28 17:05:34 1998 +0200
     2.2 +++ b/src/Pure/Thy/thy_info.ML	Wed Jul 29 15:38:08 1998 +0200
     2.3 @@ -36,6 +36,7 @@
     2.4  signature THY_INFO =
     2.5  sig
     2.6    include BASIC_THY_INFO
     2.7 +  val mk_info: string * string list * string list * theory -> string * thy_info
     2.8    val loaded_thys: thy_info Symtab.table ref
     2.9    val get_thyinfo: string -> thy_info option
    2.10    val store_theory: theory -> unit
    2.11 @@ -58,11 +59,7 @@
    2.12      thy_time = Some "", ml_time = Some "", theory = Some theory}: thy_info);
    2.13  
    2.14  (*preloaded theories*)
    2.15 -val loaded_thys =
    2.16 -  ref (Symtab.make (map mk_info
    2.17 -    [("ProtoPure", ["Pure", "CPure"], [], ProtoPure.thy),
    2.18 -     ("Pure", [], ["ProtoPure"], Pure.thy),
    2.19 -     ("CPure", [], ["ProtoPure"], CPure.thy)]));
    2.20 +val loaded_thys = ref (Symtab.empty: thy_info Symtab.table);
    2.21  
    2.22  
    2.23  (* retrieve info *)
     3.1 --- a/src/Pure/pure.ML	Tue Jul 28 17:05:34 1998 +0200
     3.2 +++ b/src/Pure/pure.ML	Wed Jul 29 15:38:08 1998 +0200
     3.3 @@ -2,26 +2,27 @@
     3.4      ID:         $Id$
     3.5      Author:     Markus Wenzel, TU Muenchen
     3.6  
     3.7 -The actual Pure and CPure theories.
     3.8 +Setup the actual Pure and CPure theories.
     3.9  *)
    3.10  
    3.11  structure Pure =
    3.12  struct
    3.13 -
    3.14 -val thy =
    3.15 -  PureThy.begin_theory "Pure" [ProtoPure.thy]
    3.16 -  |> Theory.add_syntax Syntax.pure_appl_syntax
    3.17 -  |> PureThy.end_theory;
    3.18 -
    3.19 +  val thy =
    3.20 +    PureThy.begin_theory "Pure" [ProtoPure.thy]
    3.21 +    |> Theory.add_syntax Syntax.pure_appl_syntax
    3.22 +    |> PureThy.end_theory;
    3.23  end;
    3.24  
    3.25 -
    3.26  structure CPure =
    3.27  struct
    3.28 +  val thy =
    3.29 +    PureThy.begin_theory "CPure" [ProtoPure.thy]
    3.30 +    |> Theory.add_syntax Syntax.pure_applC_syntax
    3.31 +    |> PureThy.end_theory;
    3.32 +end;
    3.33  
    3.34 -val thy =
    3.35 -  PureThy.begin_theory "CPure" [ProtoPure.thy]
    3.36 -  |> Theory.add_syntax Syntax.pure_applC_syntax
    3.37 -  |> PureThy.end_theory;
    3.38 -
    3.39 -end;
    3.40 +ThyInfo.loaded_thys :=
    3.41 +  (Symtab.make (map ThyInfo.mk_info
    3.42 +    [("ProtoPure", ["Pure", "CPure"], [], ProtoPure.thy),
    3.43 +     ("Pure", [], ["ProtoPure"], Pure.thy),
    3.44 +     ("CPure", [], ["ProtoPure"], CPure.thy)]));