# HG changeset patch
# User wenzelm
# Date 1026837595 -7200
# Node ID 33b7736d8cc0462f6629949d93949d18b4049f80
# Parent  18790d503fe06e5c3a2d34737f54bcef3c6a4a2a
locale: optional predicate name, or "open";

diff -r 18790d503fe0 -r 33b7736d8cc0 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Tue Jul 16 18:39:27 2002 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Tue Jul 16 18:39:55 2002 +0200
@@ -284,10 +284,14 @@
     Scan.optional (P.$$$ "+" |-- P.!!! (Scan.repeat1 P.locale_element)) [] ||
   Scan.repeat1 P.locale_element >> pair Locale.empty);
 
+val locale_pred =
+  P.$$$ "(" |-- P.!!! ((P.$$$ "open" >> K None || P.name >> Some) --| P.$$$ ")");
+
 val localeP =
   OuterSyntax.command "locale" "define named proof context" K.thy_decl
-    (P.name -- (P.$$$ "=" |-- P.!!! locale_val || Scan.succeed (Locale.empty, []))
-      >> (Toplevel.theory o IsarThy.add_locale o P.triple2));
+    (Scan.option locale_pred -- P.name --
+      (P.$$$ "=" |-- P.!!! locale_val || Scan.succeed (Locale.empty, []))
+      >> (Toplevel.theory o IsarThy.add_locale o (fn ((x, y), (z, w)) => (x, y, z, w))));
 
 
 
@@ -720,9 +724,10 @@
  ["!", "!!", "%", "%%", "(", ")", "+", ",", "--", ":", "::", ";", "<",
   "<=", "=", "==", "=>", "?", "[", "]", "and", "assumes", "binder",
   "concl", "defines", "files", "fixes", "in", "includes", "infix",
-  "infixl", "infixr", "is", "notes", "output", "overloaded", "shows",
-  "structure", "where", "|", "\\<equiv>", "\\<leftharpoondown>",
-  "\\<rightharpoonup>", "\\<rightleftharpoons>", "\\<subseteq>"];
+  "infixl", "infixr", "is", "notes", "open", "output", "overloaded",
+  "shows", "structure", "where", "|", "\\<equiv>",
+  "\\<leftharpoondown>", "\\<rightharpoonup>",
+  "\\<rightleftharpoons>", "\\<subseteq>"];
 
 val parsers = [
   (*theory structure*)