more standard bootstrapping of Pure.thy;
authorwenzelm
Wed Aug 01 19:53:20 2012 +0200 (2012-08-01)
changeset 4863822d65e375c01
parent 48637 547b075669ae
child 48639 675988e64bf9
more standard bootstrapping of Pure.thy;
src/Pure/Isar/outer_syntax.ML
src/Pure/Pure.thy
src/Pure/Thy/thy_header.ML
src/Pure/Thy/thy_header.scala
src/Pure/Thy/thy_info.ML
src/Pure/context.ML
src/Pure/pure_setup.ML
src/Pure/theory.ML
     1.1 --- a/src/Pure/Isar/outer_syntax.ML	Wed Aug 01 18:57:17 2012 +0200
     1.2 +++ b/src/Pure/Isar/outer_syntax.ML	Wed Aug 01 19:53:20 2012 +0200
     1.3 @@ -31,7 +31,6 @@
     1.4    val print_outer_syntax: unit -> unit
     1.5    val scan: Position.T -> string -> Token.T list
     1.6    val parse: Position.T -> string -> Toplevel.transition list
     1.7 -  val process_file: Path.T -> theory -> theory
     1.8    type isar
     1.9    val isar: TextIO.instream -> bool -> isar
    1.10    val read_span: outer_syntax -> Token.T list -> Toplevel.transition * bool
    1.11 @@ -242,20 +241,6 @@
    1.12    |> Source.exhaust;
    1.13  
    1.14  
    1.15 -(* process file *)
    1.16 -
    1.17 -fun process_file path thy =
    1.18 -  let
    1.19 -    val trs = parse (Path.position path) (File.read path);
    1.20 -    val init = Toplevel.init_theory (K thy) Toplevel.empty;
    1.21 -    val result = fold Toplevel.command (init :: trs) Toplevel.toplevel;
    1.22 -  in
    1.23 -    (case (Toplevel.is_theory result, Toplevel.generic_theory_of result) of
    1.24 -      (true, Context.Theory thy') => thy'
    1.25 -    | _ => error "Bad result state: global theory expected")
    1.26 -  end;
    1.27 -
    1.28 -
    1.29  (* interactive source of toplevel transformers *)
    1.30  
    1.31  type isar =
     2.1 --- a/src/Pure/Pure.thy	Wed Aug 01 18:57:17 2012 +0200
     2.2 +++ b/src/Pure/Pure.thy	Wed Aug 01 19:53:20 2012 +0200
     2.3 @@ -1,3 +1,5 @@
     2.4 +theory Pure
     2.5 +begin
     2.6  
     2.7  section {* Further content for the Pure theory *}
     2.8  
     2.9 @@ -82,3 +84,5 @@
    2.10    qed
    2.11  qed
    2.12  
    2.13 +end
    2.14 +
     3.1 --- a/src/Pure/Thy/thy_header.ML	Wed Aug 01 18:57:17 2012 +0200
     3.2 +++ b/src/Pure/Thy/thy_header.ML	Wed Aug 01 19:53:20 2012 +0200
     3.3 @@ -97,7 +97,7 @@
     3.4  
     3.5  val args =
     3.6    theory_name --
     3.7 -  (Parse.$$$ importsN |-- Parse.!!! (Scan.repeat1 theory_name)) --
     3.8 +  Scan.optional (Parse.$$$ importsN |-- Parse.!!! (Scan.repeat1 theory_name)) [] --
     3.9    Scan.optional (Parse.$$$ keywordsN |-- Parse.!!! keyword_decls) [] --
    3.10    Scan.optional (Parse.$$$ usesN |-- Parse.!!! (Scan.repeat1 file)) [] --|
    3.11    Parse.$$$ beginN >>
     4.1 --- a/src/Pure/Thy/thy_header.scala	Wed Aug 01 18:57:17 2012 +0200
     4.2 +++ b/src/Pure/Thy/thy_header.scala	Wed Aug 01 19:53:20 2012 +0200
     4.3 @@ -62,7 +62,7 @@
     4.4  
     4.5      val args =
     4.6        theory_name ~
     4.7 -      (keyword(IMPORTS) ~! (rep1(theory_name)) ^^ { case _ ~ xs => xs }) ~
     4.8 +      (opt(keyword(IMPORTS) ~! (rep1(theory_name))) ^^ { case None => Nil case Some(_ ~ xs) => xs }) ~
     4.9        (opt(keyword(KEYWORDS) ~! keyword_decls) ^^ { case None => Nil case Some(_ ~ xs) => xs }) ~
    4.10        (opt(keyword(USES) ~! (rep1(file))) ^^ { case None => Nil case Some(_ ~ xs) => xs }) ~
    4.11        keyword(BEGIN) ^^
     5.1 --- a/src/Pure/Thy/thy_info.ML	Wed Aug 01 18:57:17 2012 +0200
     5.2 +++ b/src/Pure/Thy/thy_info.ML	Wed Aug 01 19:53:20 2012 +0200
     5.3 @@ -236,7 +236,9 @@
     5.4      val {uses, keywords, ...} = Thy_Header.read pos text;
     5.5      val header = Thy_Header.make name imports keywords uses;
     5.6  
     5.7 -    val (theory, present) = Thy_Load.load_thy update_time dir header pos text parents;
     5.8 +    val (theory, present) =
     5.9 +      Thy_Load.load_thy update_time dir header pos text
    5.10 +        (if name = Context.PureN then [ML_Context.the_global_context ()] else parents);
    5.11      fun commit () = update_thy deps theory;
    5.12    in (theory, present, commit) end;
    5.13  
     6.1 --- a/src/Pure/context.ML	Wed Aug 01 18:57:17 2012 +0200
     6.2 +++ b/src/Pure/context.ML	Wed Aug 01 19:53:20 2012 +0200
     6.3 @@ -410,7 +410,7 @@
     6.4  
     6.5        val Theory ({ids, ...}, data, _, _) =
     6.6          (case parents of
     6.7 -          [] => error "No parent theories"
     6.8 +          [] => error "Missing theory imports"
     6.9          | [thy] => extend_thy thy
    6.10          | thy :: thys => Library.foldl (merge_thys pp) (thy, thys));
    6.11  
     7.1 --- a/src/Pure/pure_setup.ML	Wed Aug 01 18:57:17 2012 +0200
     7.2 +++ b/src/Pure/pure_setup.ML	Wed Aug 01 19:53:20 2012 +0200
     7.3 @@ -4,16 +4,21 @@
     7.4  Pure theory and ML toplevel setup.
     7.5  *)
     7.6  
     7.7 +(* ML toplevel use commands *)
     7.8 +
     7.9 +fun use name = Toplevel.program (fn () => Thy_Load.use_ml (Path.explode name));
    7.10 +
    7.11 +fun use_thys name = Toplevel.program (fn () => Thy_Info.use_thys name);
    7.12 +fun use_thy name = Toplevel.program (fn () => Thy_Info.use_thy name);
    7.13 +
    7.14 +
    7.15  (* the Pure theory *)
    7.16  
    7.17 -Context.>> (Context.map_theory
    7.18 - (Outer_Syntax.process_file (Path.explode "Pure.thy") #>
    7.19 -  Theory.end_theory));
    7.20 +Unsynchronized.setmp Multithreading.max_threads 1
    7.21 +  use_thy "Pure";
    7.22 +Context.set_thread_data NONE;
    7.23  
    7.24 -structure Pure = struct val thy = ML_Context.the_global_context () end;
    7.25 -
    7.26 -Context.set_thread_data NONE;
    7.27 -Thy_Info.register_thy Pure.thy;
    7.28 +structure Pure = struct val thy = Thy_Info.get_theory "Pure" end;
    7.29  
    7.30  
    7.31  (* ML toplevel pretty printing *)
    7.32 @@ -39,14 +44,6 @@
    7.33  if ML_System.is_polyml then use "ML/install_pp_polyml.ML" else ();
    7.34  
    7.35  
    7.36 -(* ML toplevel use commands *)
    7.37 -
    7.38 -fun use name = Toplevel.program (fn () => Thy_Load.use_ml (Path.explode name));
    7.39 -
    7.40 -fun use_thys name = Toplevel.program (fn () => Thy_Info.use_thys name);
    7.41 -fun use_thy name = Toplevel.program (fn () => Thy_Info.use_thy name);
    7.42 -
    7.43 -
    7.44  (* misc *)
    7.45  
    7.46  val cd = File.cd o Path.explode;
     8.1 --- a/src/Pure/theory.ML	Wed Aug 01 18:57:17 2012 +0200
     8.2 +++ b/src/Pure/theory.ML	Wed Aug 01 19:53:20 2012 +0200
     8.3 @@ -138,16 +138,19 @@
     8.4  fun at_end f = map_wrappers (apsnd (cons (f, stamp ())));
     8.5  
     8.6  fun begin_theory name imports =
     8.7 -  let
     8.8 -    val thy = Context.begin_thy Context.pretty_global name imports;
     8.9 -    val wrappers = begin_wrappers thy;
    8.10 -  in
    8.11 -    thy
    8.12 -    |> Sign.local_path
    8.13 -    |> Sign.map_naming (Name_Space.set_theory_name name)
    8.14 -    |> apply_wrappers wrappers
    8.15 -    |> tap (Syntax.force_syntax o Sign.syn_of)
    8.16 -  end;
    8.17 +  if name = Context.PureN then
    8.18 +    (case imports of [thy] => thy | _ => error "Bad bootstrapping of theory Pure")
    8.19 +  else
    8.20 +    let
    8.21 +      val thy = Context.begin_thy Context.pretty_global name imports;
    8.22 +      val wrappers = begin_wrappers thy;
    8.23 +    in
    8.24 +      thy
    8.25 +      |> Sign.local_path
    8.26 +      |> Sign.map_naming (Name_Space.set_theory_name name)
    8.27 +      |> apply_wrappers wrappers
    8.28 +      |> tap (Syntax.force_syntax o Sign.syn_of)
    8.29 +    end;
    8.30  
    8.31  fun end_theory thy =
    8.32    thy |> apply_wrappers (end_wrappers thy) |> Context.finish_thy;