# HG changeset patch
# User wenzelm
# Date 1169240894 -3600
# Node ID 0886ec05f951858fb29f73e2929da386a756881b
# Parent  ecdbab20c92c5aadd391746bf3dfd33c6e4a6eb2
renamed Isar/thy_header.ML to Thy/thy_header.ML;

diff -r ecdbab20c92c -r 0886ec05f951 src/Pure/Isar/thy_header.ML
--- a/src/Pure/Isar/thy_header.ML	Fri Jan 19 22:08:13 2007 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,65 +0,0 @@
-(*  Title:      Pure/Isar/thy_header.ML
-    ID:         $Id$
-    Author:     Markus Wenzel, TU Muenchen
-
-Theory headers -- processed separately with minimal outer syntax.
-*)
-
-signature THY_HEADER =
-sig
-  val args: OuterLex.token list ->
-    (string * string list * (string * bool) list) * OuterLex.token list
-  val read: (string, 'a) Source.source * Position.T ->
-    string * string list * (string * bool) list
-end;
-
-structure ThyHeader: THY_HEADER =
-struct
-
-structure T = OuterLex;
-structure P = OuterParse;
-
-
-(* 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 *)
-
-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 () => (header_lexicon, Scan.empty_lexicon)) pos
-    |> T.source_proper
-    |> 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;
-
-end;
diff -r ecdbab20c92c -r 0886ec05f951 src/Pure/Thy/thy_header.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Thy/thy_header.ML	Fri Jan 19 22:08:14 2007 +0100
@@ -0,0 +1,65 @@
+(*  Title:      Pure/Thy/thy_header.ML
+    ID:         $Id$
+    Author:     Markus Wenzel, TU Muenchen
+
+Theory headers -- independent of outer syntax.
+*)
+
+signature THY_HEADER =
+sig
+  val args: OuterLex.token list ->
+    (string * string list * (string * bool) list) * OuterLex.token list
+  val read: (string, 'a) Source.source * Position.T ->
+    string * string list * (string * bool) list
+end;
+
+structure ThyHeader: THY_HEADER =
+struct
+
+structure T = OuterLex;
+structure P = OuterParse;
+
+
+(* 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 *)
+
+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 () => (header_lexicon, Scan.empty_lexicon)) pos
+    |> T.source_proper
+    |> 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;
+
+end;