Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
import locale expression;
authorwenzelm
Thu, 22 Nov 2001 23:44:30 +0100
changeset 12270 71534648d5d4
parent 12269 fda9192d0344
child 12271 37b9c807b461
import locale expression;
src/Pure/Isar/isar_syn.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/Isar/isar_syn.ML	Thu Nov 22 23:15:12 2001 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Thu Nov 22 23:44:30 2001 +0100
@@ -283,8 +283,9 @@
 
 val locale_decl =
   (P.name --| P.$$$ "=") --
-    (Scan.repeat1 (P.xname --| P.$$$ "+") -- Scan.repeat (P.locale_element -- P.marg_comment) ||
-      Scan.repeat1 (P.locale_element -- P.marg_comment) >> pair []) >> P.triple2;
+    (P.locale_expr -- Scan.optional
+      (P.$$$ "+" |-- P.!!! (Scan.repeat1 (P.locale_element -- P.marg_comment))) [] ||
+    Scan.repeat1 (P.locale_element -- P.marg_comment) >> pair Locale.empty) >> P.triple2;
 
 val localeP =
   OuterSyntax.command "locale" "define named proof context" K.thy_decl
isabelle