# HG changeset patch
# User wenzelm
# Date 1129751566 -7200
# Node ID b8f2dd8858f64ada6d51bd67873cc6ff1365d90d
# Parent  677f7bec354e010e76b05d97ec3bcd7e3e05ea59
removed obsolete non-Isar theory format and old Isar theory headers;

diff -r 677f7bec354e -r b8f2dd8858f6 src/Pure/Isar/thy_header.ML
--- a/src/Pure/Isar/thy_header.ML	Wed Oct 19 21:52:45 2005 +0200
+++ b/src/Pure/Isar/thy_header.ML	Wed Oct 19 21:52:46 2005 +0200
@@ -2,15 +2,14 @@
     ID:         $Id$
     Author:     Markus Wenzel, TU Muenchen
 
-Theory headers (old and new-style).
+Theory headers.
 *)
 
 signature THY_HEADER =
 sig
-  val is_old: (string, 'a) Source.source * Position.T -> bool
   val args: OuterLex.token list ->
     (string * string list * (string * bool) list) * OuterLex.token list
-  val scan: (string, 'a) Source.source * Position.T ->
+  val read: (string, 'a) Source.source * Position.T ->
     string * string list * (string * bool) list
 end;
 
@@ -21,72 +20,46 @@
 structure P = OuterParse;
 
 
-(* scan header *)
+(* keywords *)
+
+val headerN = "header";
+val theoryN = "theory";
+val importsN = "imports";
+val usesN = "uses";
+val beginN = "begin";
+
+val header_lexicon = T.make_lexicon
+  ["%", "(", ")", ";", beginN, headerN, importsN, theoryN, usesN];
+
+
+(* header args *)
 
-fun scan_header get_lex scan (src, pos) =
+val file = (P.$$$ "(" |-- P.!!! (P.name --| P.$$$ ")")) >> rpair false || P.name >> rpair true;
+val uses = Scan.optional (P.$$$ usesN |-- P.!!! (Scan.repeat1 file)) [];
+
+val args =
+  P.name -- (P.$$$ importsN |-- P.!!! (Scan.repeat1 P.name -- uses --| P.$$$ beginN))
+  >> P.triple2;
+
+
+(* read header *)
+
+val header =
+  (P.$$$ headerN -- P.tags) |-- (P.!!! (P.text -- Scan.repeat P.semicolon --
+    (P.$$$ theoryN -- P.tags) |-- args)) ||
+  (P.$$$ theoryN -- P.tags) |-- P.!!! args;
+
+fun read (src, pos) =
   let val res =
     src
     |> Symbol.source false
-    |> T.source false (fn () => (get_lex (), Scan.empty_lexicon)) pos
+    |> T.source false (fn () => (header_lexicon, Scan.empty_lexicon)) pos
     |> T.source_proper
-    |> Source.source T.stopper (Scan.single scan) NONE
+    |> Source.source T.stopper (Scan.single (Scan.error header)) NONE
     |> Source.get_single;
   in
     (case res of SOME (x, _) => x
     | NONE => error ("Unexpected end of input" ^ Position.str_of pos))
   end;
 
-
-(* keywords *)
-
-val headerN = "header";
-val theoryN = "theory";
-val importsN = "imports";
-val filesN = "files";
-val usesN = "uses";
-val beginN = "begin";
-
-
-(* detect new/old headers *)
-
-val check_header_lexicon = T.make_lexicon [headerN, theoryN];
-val check_header = Scan.option (P.$$$ headerN || P.$$$ theoryN);
-
-fun is_old src_pos =
-  is_none (scan_header (K check_header_lexicon) check_header src_pos);
-
-
-(* scan old/new headers *)
-
-val header_lexicon = T.make_lexicon
-  ["%", "(", ")", "+", ":", ";", "=", beginN, filesN, headerN, importsN, theoryN, usesN];
-
-val file =
-  (P.$$$ "(" |-- P.!!! (P.name --| P.$$$ ")")) >> rpair false || P.name >> rpair true;
-fun files keyword = Scan.optional (keyword |-- P.!!! (Scan.repeat1 file)) [];
-
-val args =
-  P.name --
-   (P.$$$ "=" |-- P.!!! (P.enum1 "+" P.name -- files (P.$$$ filesN) --| P.$$$ ":") ||
-    P.$$$ importsN |-- P.!!! (Scan.repeat1 P.name -- files (P.$$$ usesN) --| P.$$$ beginN))
-  >> P.triple2;
-
-
-val new_header =
-  (P.$$$ headerN -- P.tags) |-- (P.!!! (P.text -- Scan.repeat P.semicolon --
-    (P.$$$ theoryN -- P.tags) |-- args)) ||
-  (P.$$$ theoryN -- P.tags) |-- P.!!! args;
-
-val old_header =
-  P.!!! (P.group "theory header"
-    (P.name -- (P.$$$ "=" |-- P.name -- Scan.repeat (P.$$$ "+" |-- P.name))))
-  >> (fn (A, (B, Bs)) => (A, B :: Bs, []: (string * bool) list));
-
-fun scan src_pos =
-  (*sadly, old-style headers depend on the current (dynamic!) lexicon*)
-  if is_old 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;
-
-
 end;