src/Pure/Isar/spec_parse.ML

--- a/src/Pure/Isar/spec_parse.ML	Thu Mar 26 17:00:59 2009 +0100
+++ b/src/Pure/Isar/spec_parse.ML	Thu Mar 26 18:59:25 2009 +0100
@@ -22,7 +22,7 @@
   val locale_fixes: (binding * string option * mixfix) list parser
   val locale_insts: (string option list * (Attrib.binding * string) list) parser
   val class_expr: string list parser
-  val locale_expression: Expression.expression parser
+  val locale_expression: bool -> Expression.expression parser
   val locale_keyword: string parser
   val context_element: Element.context parser
   val statement: (Attrib.binding * (string * string list) list) list parser
@@ -77,7 +77,7 @@
 
 val locale_insts =
   Scan.optional (P.$$$ "[" |-- P.!!! (Scan.repeat1 (P.maybe P.term) --| P.$$$ "]")) []
-  -- Scan.optional (P.$$$ "where" |-- P.and_list1 (opt_thm_name ":" -- P.prop)) [];
+  -- Scan.optional (P.where_ |-- P.and_list1 (opt_thm_name ":" -- P.prop)) [];
 
 local
 
@@ -95,13 +95,12 @@
 fun plus1_unless test scan =
   scan ::: Scan.repeat (P.$$$ "+" |-- Scan.unless test (P.!!! scan));
 
-val rename = P.name -- Scan.option P.mixfix;
+fun prefix mandatory =
+  P.name -- (P.$$$ "!" >> K true || P.$$$ "?" >> K false || Scan.succeed mandatory) --| P.$$$ ":";
 
-val prefix = P.name -- Scan.optional (P.$$$ "!" >> K true) false --| P.$$$ ":";
-val named = P.name -- (P.$$$ "=" |-- P.term);
-val position = P.maybe P.term;
-val instance = P.$$$ "where" |-- P.and_list1 named >> Expression.Named ||
-  Scan.repeat1 position >> Expression.Positional;
+val instance = P.where_ |--
+  P.and_list1 (P.name -- (P.$$$ "=" |-- P.term)) >> Expression.Named ||
+  Scan.repeat1 (P.maybe P.term) >> Expression.Positional;
 
 in
 
@@ -110,10 +109,10 @@
 
 val class_expr = plus1_unless locale_keyword P.xname;
 
-val locale_expression =
+fun locale_expression mandatory =
   let
     val expr2 = P.xname;
-    val expr1 = Scan.optional prefix ("", false) -- expr2 --
+    val expr1 = Scan.optional (prefix mandatory) ("", false) -- expr2 --
       Scan.optional instance (Expression.Named []) >> (fn ((p, l), i) => (l, (p, i)));
     val expr0 = plus1_unless locale_keyword expr1;
   in expr0 -- Scan.optional (P.$$$ "for" |-- P.!!! locale_fixes) [] end;
@@ -128,7 +127,7 @@
 val statement = P.and_list1 (opt_thm_name ":" -- Scan.repeat1 P.propp);
 
 val obtain_case =
-  P.parbinding -- (Scan.optional (P.simple_fixes --| P.$$$ "where") [] --
+  P.parbinding -- (Scan.optional (P.simple_fixes --| P.where_) [] --
     (P.and_list1 (Scan.repeat1 P.prop) >> flat));
 
 val general_statement =