src/Pure/Isar/outer_syntax.ML

--- a/src/Pure/Isar/outer_syntax.ML	Wed Feb 03 16:50:31 1999 +0100
+++ b/src/Pure/Isar/outer_syntax.ML	Wed Feb 03 17:20:09 1999 +0100
@@ -10,7 +10,6 @@
   val main: unit -> unit
   val loop: unit -> unit
   val help: unit -> unit
-  val load: string -> unit
 end;
 
 signature OUTER_SYNTAX =
@@ -24,17 +23,14 @@
   val commands: unit -> string list
   val add_keywords: string list -> unit
   val add_parsers: parser list -> unit
-  val get_header: Position.T -> (string, 'a) Source.source -> (bstring * bstring list) option
-  val read_text: Position.T -> (string, 'a) Source.source -> Toplevel.transition list
-  val read_file: string -> Toplevel.transition list
+  val deps_thy: string -> bool -> Path.T -> string list * Path.T list
+  val load_thy: string -> bool -> bool -> Path.T -> unit
   val isar: Toplevel.isar
 end;
 
 structure OuterSyntax: OUTER_SYNTAX =
 struct
 
-open OuterParse;
-
 
 (** outer syntax **)
 
@@ -51,6 +47,8 @@
 
 (* parse command *)
 
+local open OuterParse in
+
 fun command_name cmd =
   group "command"
     (position (Scan.one (OuterLex.keyword_pred (is_some o cmd)) >> OuterLex.val_of));
@@ -65,6 +63,8 @@
     Some (Toplevel.empty |> Toplevel.name name |> Toplevel.position pos |>
       Toplevel.interactive int_only |> f));
 
+end;
+
 
 
 (** global syntax state **)
@@ -128,37 +128,101 @@
 
 fun source do_recover cmd src =
   src
-  |> Source.source OuterLex.stopper (Scan.bulk (fn xs => !!! (command (cmd ())) xs))
+  |> Source.source OuterLex.stopper (Scan.bulk (fn xs => OuterParse.!!! (command (cmd ())) xs))
     (if do_recover then Some (fn xs => recover (cmd ()) xs) else None)
   |> Source.mapfilter I;
 
 
 (* detect header *)
 
-val head_lexicon =
-  Scan.make_lexicon (map Symbol.explode ["+", ":", "=", "theory"]);
-
-val head_parser =
-  $$$ "theory" |-- !!! (name -- ($$$ "=" |-- enum "+" name --| (Scan.ahead eof || $$$ ":")));
-
-fun get_header pos src =
+fun scan_header get_lexicon scan (src, pos) =
   src
   |> Symbol.source false
-  |> OuterLex.source false (K head_lexicon) pos
-  |> Source.source OuterLex.stopper (Scan.single (Scan.option head_parser)) None
+  |> OuterLex.source false get_lexicon pos
+  |> Source.source OuterLex.stopper (Scan.single scan) None
   |> (fst o the o Source.get_single);
 
+val check_header_lexicon = Scan.make_lexicon [Symbol.explode "theory"];
 
-(* read text (including header) *)
+fun is_old_theory src =
+  is_none (scan_header (K check_header_lexicon) (Scan.option (OuterParse.$$$ "theory")) src);
+
+fun warn_theory_style path is_old =
+  let
+    val style = if is_old then "old" else "new";
+    val _ = warning ("Assuming " ^ style ^ "-style theory format for " ^ quote (Path.pack path));
+  in is_old end;
+
+
+(* deps_thy --- inspect theory header *)
+
+val new_header_lexicon =
+  Scan.make_lexicon (map Symbol.explode ["+", ":", "=", "files", "theory"]);
+
+local open OuterParse in
+
+val new_header =
+  $$$ "theory" |-- !!! (name -- ($$$ "=" |-- enum1 "+" name) --
+    Scan.optional ($$$ "files" |-- !!! (Scan.repeat1 name)) [] --| (Scan.ahead eof || $$$ ":"));
+
+val old_header =
+  name -- ($$$ "=" |-- name -- Scan.repeat ($$$ "+" |-- name))
+  >> (fn (A, (B, Bs)) => ((A, B :: Bs), []));
+
+end;
 
-fun read_text pos src =
+fun deps_thy name ml path =
+  let
+    val src = Source.of_file path;
+    val is_old = warn_theory_style path (is_old_theory src);
+    val ((name', parents), files) =
+      (*Note: old style headers dynamically depend on the current lexicon :-( *)
+      if is_old then scan_header ThySyn.get_lexicon (Scan.error old_header) src
+      else scan_header (K new_header_lexicon) (Scan.error new_header) src;
+
+    val ml_path = ThyLoad.ml_path name;
+    val ml_file = if not ml orelse is_none (ThyLoad.check_file ml_path) then [] else [ml_path];
+  in
+    if name <> name' then
+      error ("Filename " ^ quote (Path.pack path) ^ " does not match theory name " ^ quote name)
+    else (parents, map Path.unpack files @ ml_file)
+  end;
+
+
+(* load_thy --- read text (including header) *)
+
+fun try_ml_file name ml =
+  let
+    val path = ThyLoad.ml_path name;
+    val tr = Toplevel.imperative (fn () => ThyInfo.load_file path);
+  in
+    if not ml orelse is_none (ThyLoad.check_file path) then ()
+    else Toplevel.excursion [Toplevel.empty |> Toplevel.name "use" |> tr]
+  end;
+
+fun parse_thy (src, pos) =
   src
   |> Symbol.source false
   |> OuterLex.source false (K (get_lexicon ())) pos
   |> source false (K (get_parser ()))
   |> Source.exhaust;
 
-fun read_file name = read_text (Position.line_name 1 (quote name)) (Source.of_file name);
+fun read_thy name ml path =
+  let
+    val (src, pos) = Source.of_file path;
+    val _ =
+      if is_old_theory (src, pos) then ThySyn.load_thy name (Source.exhaust src)
+      else (Toplevel.excursion (parse_thy (src, pos))
+        handle exn => error (Toplevel.exn_message exn));
+    val theory = ThyInfo.get_theory name;
+  in Context.setmp theory try_ml_file name ml end;
+
+fun load_thy name ml time path =
+  if not time then read_thy name ml path
+  else timeit (fn () =>
+   (writeln ("\n**** Starting Theory " ^ quote name ^ " ****");
+    setmp Goals.proof_timing true (read_thy name ml) path;
+    writeln ("**** Finished Theory " ^ quote name ^ " ****\n")));
 
 
 (* interactive source of state transformers *)
@@ -180,16 +244,10 @@
 fun main () =
  (Toplevel.set_state Toplevel.toplevel;
   ml_prompts "ML> " "ML# ";
-  writeln (Context.welcome ());
+  writeln (Session.welcome ());
   loop ());
 
 
-(* load *)
-
-fun load name = Toplevel.excursion (read_file (name ^ ".thy"))
-  handle exn => error (Toplevel.exn_message exn);
-
-
 (* help *)
 
 fun help () =
@@ -199,5 +257,10 @@
 
 end;
 
+(*setup theory syntax dependent operations*)
+ThyLoad.deps_thy_fn := OuterSyntax.deps_thy;
+ThyLoad.load_thy_fn := OuterSyntax.load_thy;
+structure ThyLoad: THY_LOAD = ThyLoad;
+
 structure BasicOuterSyntax: BASIC_OUTER_SYNTAX = OuterSyntax;
 open BasicOuterSyntax;