# HG changeset patch
# User wenzelm
# Date 939151134 -7200
# Node ID b52c1a632e6a185a6c3b9466bd58ec323e79c258
# Parent  131005d3a62ddf9d1df7bd1fac23c4e334f2c939
simplified;
header command;

diff -r 131005d3a62d -r b52c1a632e6a src/Pure/Isar/outer_syntax.ML
--- a/src/Pure/Isar/outer_syntax.ML	Tue Oct 05 21:18:13 1999 +0200
+++ b/src/Pure/Isar/outer_syntax.ML	Tue Oct 05 21:18:54 1999 +0200
@@ -206,10 +206,14 @@
 
 (** read theory **)
 
-(* theory keyword *)
+(* special keywords *)
 
+val headerN = "header";
 val theoryN = "theory";
+
 val theory_keyword = OuterParse.$$$ theoryN;
+val header_keyword = OuterParse.$$$ headerN;
+val semicolon = P.$$$ ";";
 
 
 (* sources *)
@@ -217,7 +221,7 @@
 local
 
 val no_terminator =
-  Scan.unless (P.$$$ ";") (Scan.one (OuterLex.not_sync andf OuterLex.not_eof));
+  Scan.unless semicolon (Scan.one (OuterLex.not_sync andf OuterLex.not_eof));
 
 val recover = Scan.prompt "recover# " (Scan.repeat no_terminator);
 
@@ -242,7 +246,7 @@
   |> Source.filter OuterLex.is_proper;
 
 
-(* detect header *)
+(* scan header *)
 
 fun scan_header get_lex scan (src, pos) =
   src
@@ -252,46 +256,54 @@
   |> Source.source OuterLex.stopper (Scan.single scan) None
   |> (fst o the o Source.get_single);
 
-val check_header_lexicon = Scan.make_lexicon [Symbol.explode theoryN];
+
+(* detect new/old header *)
+
+local
 
-fun is_old_theory src =
-  is_none (scan_header (K check_header_lexicon) (Scan.option theory_keyword) src);
+val check_header_lexicon = Scan.make_lexicon [Symbol.explode headerN, Symbol.explode theoryN];
+val check_header = Scan.option (header_keyword || theory_keyword);
+
+in
+
+fun is_old_theory src = is_none (scan_header (K check_header_lexicon) check_header src);
+
+end;
 
 
 (* deps_thy --- inspect theory header *)
 
+local
+
 val header_lexicon =
-  Scan.make_lexicon (map Symbol.explode ["(", ")", "+", ":", "=", "files", theoryN]);
-
-local
+  Scan.make_lexicon (map Symbol.explode ["(", ")", "+", ":", ";", "=", "files", headerN, theoryN]);
 
 val file_name =
   (P.$$$ "(" |-- P.!!! (P.name --| P.$$$ ")")) >> rpair false || P.name >> rpair true;
 
-val theory_head =
+in
+
+val theory_header =
   (P.name -- (P.$$$ "=" |-- P.enum1 "+" P.name) --
-    Scan.optional (P.$$$ "files" |-- P.!!! (Scan.repeat1 file_name)) [])
+    Scan.optional (P.$$$ "files" |-- P.!!! (Scan.repeat1 file_name)) [] --|  P.$$$ ":")
   >> (fn ((A, Bs), files) => (A, Bs, files));
 
-in
-
-val theory_header = theory_head --| (Scan.ahead P.eof || P.$$$ ":");
-val only_header = theory_keyword |-- theory_head --| Scan.ahead P.eof;
-val new_header = theory_keyword |-- P.!!! theory_header;
+val new_header =
+  header_keyword |-- (P.!!! (P.text -- Scan.option semicolon -- theory_keyword |-- theory_header))
+    || theory_keyword |-- P.!!! theory_header;
 
 val old_header =
   P.name -- (P.$$$ "=" |-- P.name -- Scan.repeat (P.$$$ "+" |-- P.name))
   >> (fn (A, (B, Bs)) => (A, B :: Bs, []: (string * bool) list));
 
-end;
-
 fun deps_thy name path =
   let
     val src = Source.of_string (File.read path);
     val pos = Path.position path;
     val (name', parents, files) =
       (*Note: old style headers dynamically depend on the current lexicon :-( *)
-      if is_old_theory (src, pos) then scan_header ThySyn.get_lexicon (Scan.error old_header) (src, pos)
+      if is_old_theory (src, pos) then
+        scan_header ThySyn.get_lexicon (Scan.error old_header) (src, pos)
       else scan_header (K header_lexicon) (Scan.error new_header) (src, pos);
 
     val ml_path = ThyLoad.ml_path name;
@@ -302,9 +314,13 @@
     else (parents, map (Path.unpack o #1) files @ ml_file)
   end;
 
+end;
+
 
 (* load_thy --- read text (including header) *)
 
+local
+
 fun try_ml_file name ml time =
   let
     val path = ThyLoad.ml_path name;
@@ -316,22 +332,11 @@
   end;
 
 fun parse_thy src_pos =
-  let
-    val lex_src = filter_proper (token_source src_pos);
-    val only_head =
-      lex_src
-      |> Source.source OuterLex.stopper (Scan.single (Scan.option only_header)) None
-      |> (fst o the o Source.get_single);
-  in
-    (case only_head of
-      None =>
-        lex_src
-        |> source false false (K (get_parser ()))
-        |> Source.exhaust
-    | Some spec =>
-        [Toplevel.empty |> Toplevel.name theoryN |> IsarThy.theory spec,
-          Toplevel.empty |> Toplevel.name "end" |> Toplevel.exit])
-  end;
+  src_pos
+  |> token_source
+  |> filter_proper
+  |> source false false (K (get_parser ()))
+  |> Source.exhaust;
 
 fun run_thy name path =
   let
@@ -350,6 +355,8 @@
     Present.verbatim_source name present_text
   end;
 
+in
+
 fun load_thy name ml time path =
  (if time then
     timeit (fn () =>
@@ -360,6 +367,8 @@
   Context.context (ThyInfo.get_theory name);
   try_ml_file name ml time);
 
+end;
+
 
 (* interactive source of state transformers *)