new theory header syntax.
authornipkow
Mon Aug 16 17:06:47 2004 +0200 (2004-08-16)
changeset 15132df2b7976d1e7
parent 15131 c69542757a4d
child 15133 87c074aad007
new theory header syntax.
src/Pure/Isar/isar_syn.ML
src/Pure/Isar/thy_header.ML
     1.1 --- a/src/Pure/Isar/isar_syn.ML	Mon Aug 16 14:22:27 2004 +0200
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Mon Aug 16 17:06:47 2004 +0200
     1.3 @@ -754,8 +754,8 @@
     1.4  
     1.5  val keywords =
     1.6   ["!", "!!", "%", "%%", "(", ")", "+", ",", "--", ":", "::", ";", "<",
     1.7 -  "<=", "=", "==", "=>", "?", "[", "]", "advanced", "and", "assumes",
     1.8 -  "binder", "concl", "defines", "files", "fixes", "in", "includes",
     1.9 +  "<=", "=", "==", "=>", "?", "[", "]", "advanced", "and", "assumes", "begin",
    1.10 +  "binder", "concl", "defines", "files", "fixes", "import", "in", "includes",
    1.11    "infix", "infixl", "infixr", "is", "notes", "open", "output",
    1.12    "overloaded", "shows", "structure", "where", "|", "\\<equiv>",
    1.13    "\\<leftharpoondown>", "\\<rightharpoonup>",
     2.1 --- a/src/Pure/Isar/thy_header.ML	Mon Aug 16 14:22:27 2004 +0200
     2.2 +++ b/src/Pure/Isar/thy_header.ML	Mon Aug 16 17:06:47 2004 +0200
     2.3 @@ -56,16 +56,17 @@
     2.4  
     2.5  (* scan old/new headers *)
     2.6  
     2.7 -val header_lexicon =
     2.8 -  T.make_lexicon ["(", ")", "+", ":", ";", "=", "files", headerN, theoryN];
     2.9 +val header_lexicon = T.make_lexicon
    2.10 +  ["(", ")", "+", ":", ";", "=", "begin", "files", headerN, "import", theoryN];
    2.11  
    2.12  val file_name =
    2.13    (P.$$$ "(" |-- P.!!! (P.name --| P.$$$ ")")) >> rpair false || P.name >> rpair true;
    2.14  
    2.15 -
    2.16  val args =
    2.17 -  (P.name -- (P.$$$ "=" |-- P.enum1 "+" P.name) --
    2.18 -    Scan.optional (P.$$$ "files" |-- P.!!! (Scan.repeat1 file_name)) [] --|  P.$$$ ":")
    2.19 +  (P.name -- (P.$$$ "=" |-- P.enum1 "+" P.name ||
    2.20 +              P.$$$ "import" |-- Scan.repeat1 P.name) --
    2.21 +    Scan.optional (P.$$$ "files" |-- P.!!! (Scan.repeat1 file_name)) [] --|
    2.22 +  (P.$$$ ":" || P.$$$ "begin"))
    2.23    >> (fn ((A, Bs), files) => (A, Bs, files));
    2.24  
    2.25