locale_expression: mandatory as parameter;
misc tuning and simplifications of parsers;
--- 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 =