# HG changeset patch
# User nipkow
# Date 1092668807 -7200
# Node ID df2b7976d1e79626677b0109dc488c7bd484634c
# Parent  c69542757a4d57d9ea06e9fd5260ce5d2f28c998
new theory header syntax.

diff -r c69542757a4d -r df2b7976d1e7 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Mon Aug 16 14:22:27 2004 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Mon Aug 16 17:06:47 2004 +0200
@@ -754,8 +754,8 @@
 
 val keywords =
  ["!", "!!", "%", "%%", "(", ")", "+", ",", "--", ":", "::", ";", "<",
-  "<=", "=", "==", "=>", "?", "[", "]", "advanced", "and", "assumes",
-  "binder", "concl", "defines", "files", "fixes", "in", "includes",
+  "<=", "=", "==", "=>", "?", "[", "]", "advanced", "and", "assumes", "begin",
+  "binder", "concl", "defines", "files", "fixes", "import", "in", "includes",
   "infix", "infixl", "infixr", "is", "notes", "open", "output",
   "overloaded", "shows", "structure", "where", "|", "\\<equiv>",
   "\\<leftharpoondown>", "\\<rightharpoonup>",
diff -r c69542757a4d -r df2b7976d1e7 src/Pure/Isar/thy_header.ML
--- a/src/Pure/Isar/thy_header.ML	Mon Aug 16 14:22:27 2004 +0200
+++ b/src/Pure/Isar/thy_header.ML	Mon Aug 16 17:06:47 2004 +0200
@@ -56,16 +56,17 @@
 
 (* scan old/new headers *)
 
-val header_lexicon =
-  T.make_lexicon ["(", ")", "+", ":", ";", "=", "files", headerN, theoryN];
+val header_lexicon = T.make_lexicon
+  ["(", ")", "+", ":", ";", "=", "begin", "files", headerN, "import", theoryN];
 
 val file_name =
   (P.$$$ "(" |-- P.!!! (P.name --| P.$$$ ")")) >> rpair false || P.name >> rpair true;
 
-
 val args =
-  (P.name -- (P.$$$ "=" |-- P.enum1 "+" P.name) --
-    Scan.optional (P.$$$ "files" |-- P.!!! (Scan.repeat1 file_name)) [] --|  P.$$$ ":")
+  (P.name -- (P.$$$ "=" |-- P.enum1 "+" P.name ||
+              P.$$$ "import" |-- Scan.repeat1 P.name) --
+    Scan.optional (P.$$$ "files" |-- P.!!! (Scan.repeat1 file_name)) [] --|
+  (P.$$$ ":" || P.$$$ "begin"))
   >> (fn ((A, Bs), files) => (A, Bs, files));