src/Pure/Isar/spec_parse.ML
changeset 30726 67388cc4ccb4
parent 30720 6d8dcfb264dc
child 33287 0f99569d23e1
equal deleted inserted replaced
30725:c23a5b3cd1b9 30726:67388cc4ccb4
    20   val name_facts: (Attrib.binding * (Facts.ref * Attrib.src list) list) list parser
    20   val name_facts: (Attrib.binding * (Facts.ref * Attrib.src list) list) list parser
    21   val locale_mixfix: mixfix parser
    21   val locale_mixfix: mixfix parser
    22   val locale_fixes: (binding * string option * mixfix) list parser
    22   val locale_fixes: (binding * string option * mixfix) list parser
    23   val locale_insts: (string option list * (Attrib.binding * string) list) parser
    23   val locale_insts: (string option list * (Attrib.binding * string) list) parser
    24   val class_expr: string list parser
    24   val class_expr: string list parser
    25   val locale_expression: Expression.expression parser
    25   val locale_expression: bool -> Expression.expression parser
    26   val locale_keyword: string parser
    26   val locale_keyword: string parser
    27   val context_element: Element.context parser
    27   val context_element: Element.context parser
    28   val statement: (Attrib.binding * (string * string list) list) list parser
    28   val statement: (Attrib.binding * (string * string list) list) list parser
    29   val general_statement: (Element.context list * Element.statement) parser
    29   val general_statement: (Element.context list * Element.statement) parser
    30   val statement_keyword: string parser
    30   val statement_keyword: string parser
    75     >> (single o P.triple1) ||
    75     >> (single o P.triple1) ||
    76   P.params >> map Syntax.no_syn) >> flat;
    76   P.params >> map Syntax.no_syn) >> flat;
    77 
    77 
    78 val locale_insts =
    78 val locale_insts =
    79   Scan.optional (P.$$$ "[" |-- P.!!! (Scan.repeat1 (P.maybe P.term) --| P.$$$ "]")) []
    79   Scan.optional (P.$$$ "[" |-- P.!!! (Scan.repeat1 (P.maybe P.term) --| P.$$$ "]")) []
    80   -- Scan.optional (P.$$$ "where" |-- P.and_list1 (opt_thm_name ":" -- P.prop)) [];
    80   -- Scan.optional (P.where_ |-- P.and_list1 (opt_thm_name ":" -- P.prop)) [];
    81 
    81 
    82 local
    82 local
    83 
    83 
    84 val loc_element =
    84 val loc_element =
    85   P.$$$ "fixes" |-- P.!!! locale_fixes >> Element.Fixes ||
    85   P.$$$ "fixes" |-- P.!!! locale_fixes >> Element.Fixes ||
    93     >> (curry Element.Notes "");
    93     >> (curry Element.Notes "");
    94 
    94 
    95 fun plus1_unless test scan =
    95 fun plus1_unless test scan =
    96   scan ::: Scan.repeat (P.$$$ "+" |-- Scan.unless test (P.!!! scan));
    96   scan ::: Scan.repeat (P.$$$ "+" |-- Scan.unless test (P.!!! scan));
    97 
    97 
    98 val rename = P.name -- Scan.option P.mixfix;
    98 fun prefix mandatory =
       
    99   P.name -- (P.$$$ "!" >> K true || P.$$$ "?" >> K false || Scan.succeed mandatory) --| P.$$$ ":";
    99 
   100 
   100 val prefix = P.name -- Scan.optional (P.$$$ "!" >> K true) false --| P.$$$ ":";
   101 val instance = P.where_ |--
   101 val named = P.name -- (P.$$$ "=" |-- P.term);
   102   P.and_list1 (P.name -- (P.$$$ "=" |-- P.term)) >> Expression.Named ||
   102 val position = P.maybe P.term;
   103   Scan.repeat1 (P.maybe P.term) >> Expression.Positional;
   103 val instance = P.$$$ "where" |-- P.and_list1 named >> Expression.Named ||
       
   104   Scan.repeat1 position >> Expression.Positional;
       
   105 
   104 
   106 in
   105 in
   107 
   106 
   108 val locale_keyword = P.$$$ "fixes" || P.$$$ "constrains" || P.$$$ "assumes" ||
   107 val locale_keyword = P.$$$ "fixes" || P.$$$ "constrains" || P.$$$ "assumes" ||
   109    P.$$$ "defines" || P.$$$ "notes";
   108    P.$$$ "defines" || P.$$$ "notes";
   110 
   109 
   111 val class_expr = plus1_unless locale_keyword P.xname;
   110 val class_expr = plus1_unless locale_keyword P.xname;
   112 
   111 
   113 val locale_expression =
   112 fun locale_expression mandatory =
   114   let
   113   let
   115     val expr2 = P.xname;
   114     val expr2 = P.xname;
   116     val expr1 = Scan.optional prefix ("", false) -- expr2 --
   115     val expr1 = Scan.optional (prefix mandatory) ("", false) -- expr2 --
   117       Scan.optional instance (Expression.Named []) >> (fn ((p, l), i) => (l, (p, i)));
   116       Scan.optional instance (Expression.Named []) >> (fn ((p, l), i) => (l, (p, i)));
   118     val expr0 = plus1_unless locale_keyword expr1;
   117     val expr0 = plus1_unless locale_keyword expr1;
   119   in expr0 -- Scan.optional (P.$$$ "for" |-- P.!!! locale_fixes) [] end;
   118   in expr0 -- Scan.optional (P.$$$ "for" |-- P.!!! locale_fixes) [] end;
   120 
   119 
   121 val context_element = P.group "context element" loc_element;
   120 val context_element = P.group "context element" loc_element;
   126 (* statements *)
   125 (* statements *)
   127 
   126 
   128 val statement = P.and_list1 (opt_thm_name ":" -- Scan.repeat1 P.propp);
   127 val statement = P.and_list1 (opt_thm_name ":" -- Scan.repeat1 P.propp);
   129 
   128 
   130 val obtain_case =
   129 val obtain_case =
   131   P.parbinding -- (Scan.optional (P.simple_fixes --| P.$$$ "where") [] --
   130   P.parbinding -- (Scan.optional (P.simple_fixes --| P.where_) [] --
   132     (P.and_list1 (Scan.repeat1 P.prop) >> flat));
   131     (P.and_list1 (Scan.repeat1 P.prop) >> flat));
   133 
   132 
   134 val general_statement =
   133 val general_statement =
   135   statement >> (fn x => ([], Element.Shows x)) ||
   134   statement >> (fn x => ([], Element.Shows x)) ||
   136   Scan.repeat context_element --
   135   Scan.repeat context_element --