locale syntax;
authorwenzelm
Sun, 04 Nov 2001 20:57:29 +0100
changeset 12044 d6294ebfff24
parent 12043 8c86683597a8
child 12045 bfaa23b19f47
locale syntax;
src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Sun Nov 04 20:56:59 2001 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Sun Nov 04 20:57:29 2001 +0100
@@ -284,7 +284,10 @@
 
 (* statements *)
 
-val locale = Scan.option (P.$$$ "(" |-- P.!!! (P.$$$ "in" |-- P.xname --| P.$$$ ")"));
+val locale = Scan.optional (P.$$$ "(" |-- P.!!!
+    ((P.$$$ "in" |-- P.xname >> Some) -- Scan.repeat P.locale_element ||
+      Scan.repeat1 P.locale_element >> pair None) --| P.$$$ ")") (None, []);
+
 val statement = P.opt_thm_name ":" -- P.propp -- P.marg_comment;
 
 val theoremP =
@@ -700,10 +703,11 @@
 
 val keywords =
  ["!", "!!", "%", "%%", "(", ")", "+", ",", "--", ":", "::", ";", "<",
-  "<=", "=", "==", "=>", "?", "[", "]", "and", "binder", "concl",
-  "files", "in", "infix", "infixl", "infixr", "is", "output", "overloaded",
-  "where", "|", "\\<equiv>", "\\<rightharpoonup>", "\\<leftharpoondown>",
-  "\\<rightleftharpoons>", "\\<subseteq>"];
+  "<=", "=", "==", "=>", "?", "[", "]", "and", "assumes", "binder",
+  "concl", "defines", "files", "fixes", "in", "infix", "infixl",
+  "infixr", "is", "notes", "output", "overloaded", "structure",
+  "uses", "where", "|", "\\<equiv>", "\\<leftharpoondown>",
+  "\\<rightharpoonup>", "\\<rightleftharpoons>", "\\<subseteq>"];
 
 val parsers = [
   (*theory structure*)