src/Pure/Isar/spec_parse.ML
changeset 30726 67388cc4ccb4
parent 30720 6d8dcfb264dc
child 33287 0f99569d23e1
     1.1 --- a/src/Pure/Isar/spec_parse.ML	Thu Mar 26 17:00:59 2009 +0100
     1.2 +++ b/src/Pure/Isar/spec_parse.ML	Thu Mar 26 18:59:25 2009 +0100
     1.3 @@ -22,7 +22,7 @@
     1.4    val locale_fixes: (binding * string option * mixfix) list parser
     1.5    val locale_insts: (string option list * (Attrib.binding * string) list) parser
     1.6    val class_expr: string list parser
     1.7 -  val locale_expression: Expression.expression parser
     1.8 +  val locale_expression: bool -> Expression.expression parser
     1.9    val locale_keyword: string parser
    1.10    val context_element: Element.context parser
    1.11    val statement: (Attrib.binding * (string * string list) list) list parser
    1.12 @@ -77,7 +77,7 @@
    1.13  
    1.14  val locale_insts =
    1.15    Scan.optional (P.$$$ "[" |-- P.!!! (Scan.repeat1 (P.maybe P.term) --| P.$$$ "]")) []
    1.16 -  -- Scan.optional (P.$$$ "where" |-- P.and_list1 (opt_thm_name ":" -- P.prop)) [];
    1.17 +  -- Scan.optional (P.where_ |-- P.and_list1 (opt_thm_name ":" -- P.prop)) [];
    1.18  
    1.19  local
    1.20  
    1.21 @@ -95,13 +95,12 @@
    1.22  fun plus1_unless test scan =
    1.23    scan ::: Scan.repeat (P.$$$ "+" |-- Scan.unless test (P.!!! scan));
    1.24  
    1.25 -val rename = P.name -- Scan.option P.mixfix;
    1.26 +fun prefix mandatory =
    1.27 +  P.name -- (P.$$$ "!" >> K true || P.$$$ "?" >> K false || Scan.succeed mandatory) --| P.$$$ ":";
    1.28  
    1.29 -val prefix = P.name -- Scan.optional (P.$$$ "!" >> K true) false --| P.$$$ ":";
    1.30 -val named = P.name -- (P.$$$ "=" |-- P.term);
    1.31 -val position = P.maybe P.term;
    1.32 -val instance = P.$$$ "where" |-- P.and_list1 named >> Expression.Named ||
    1.33 -  Scan.repeat1 position >> Expression.Positional;
    1.34 +val instance = P.where_ |--
    1.35 +  P.and_list1 (P.name -- (P.$$$ "=" |-- P.term)) >> Expression.Named ||
    1.36 +  Scan.repeat1 (P.maybe P.term) >> Expression.Positional;
    1.37  
    1.38  in
    1.39  
    1.40 @@ -110,10 +109,10 @@
    1.41  
    1.42  val class_expr = plus1_unless locale_keyword P.xname;
    1.43  
    1.44 -val locale_expression =
    1.45 +fun locale_expression mandatory =
    1.46    let
    1.47      val expr2 = P.xname;
    1.48 -    val expr1 = Scan.optional prefix ("", false) -- expr2 --
    1.49 +    val expr1 = Scan.optional (prefix mandatory) ("", false) -- expr2 --
    1.50        Scan.optional instance (Expression.Named []) >> (fn ((p, l), i) => (l, (p, i)));
    1.51      val expr0 = plus1_unless locale_keyword expr1;
    1.52    in expr0 -- Scan.optional (P.$$$ "for" |-- P.!!! locale_fixes) [] end;
    1.53 @@ -128,7 +127,7 @@
    1.54  val statement = P.and_list1 (opt_thm_name ":" -- Scan.repeat1 P.propp);
    1.55  
    1.56  val obtain_case =
    1.57 -  P.parbinding -- (Scan.optional (P.simple_fixes --| P.$$$ "where") [] --
    1.58 +  P.parbinding -- (Scan.optional (P.simple_fixes --| P.where_) [] --
    1.59      (P.and_list1 (Scan.repeat1 P.prop) >> flat));
    1.60  
    1.61  val general_statement =