# HG changeset patch # User wenzelm # Date 1238090365 -3600 # Node ID 67388cc4ccb4526aa9bdee27fb10b14e1647f2e6 # Parent c23a5b3cd1b9ab043457f66a1ccfc00d9e7825fd locale_expression: mandatory as parameter; misc tuning and simplifications of parsers; diff -r c23a5b3cd1b9 -r 67388cc4ccb4 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 =