src/Pure/Isar/parse_spec.ML
author blanchet
Tue, 13 May 2014 11:10:22 +0200
changeset 56945 3d1ead21a055
parent 56201 dd2df97b379b
child 58011 bc6bced136e5
permissions -rw-r--r--
tuning
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
36952
338c3f8229e4 renamed structure SpecParse to Parse_Spec, keeping the old name as alias for some time;
wenzelm
parents: 36950
diff changeset
     1
(*  Title:      Pure/Isar/parse_spec.ML
22104
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
     3
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
     4
Parsers for complex specifications.
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
     5
*)
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
     6
36952
338c3f8229e4 renamed structure SpecParse to Parse_Spec, keeping the old name as alias for some time;
wenzelm
parents: 36950
diff changeset
     7
signature PARSE_SPEC =
22104
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
     8
sig
29312
f369fb19146e added type 'a parser, simplified signature;
wenzelm
parents: 29214
diff changeset
     9
  val attribs: Attrib.src list parser
f369fb19146e added type 'a parser, simplified signature;
wenzelm
parents: 29214
diff changeset
    10
  val opt_attribs: Attrib.src list parser
f369fb19146e added type 'a parser, simplified signature;
wenzelm
parents: 29214
diff changeset
    11
  val thm_name: string -> Attrib.binding parser
f369fb19146e added type 'a parser, simplified signature;
wenzelm
parents: 29214
diff changeset
    12
  val opt_thm_name: string -> Attrib.binding parser
30481
de003023c302 removed old named_spec, spec_name, spec_opt_name;
wenzelm
parents: 29601
diff changeset
    13
  val spec: (Attrib.binding * string) parser
de003023c302 removed old named_spec, spec_name, spec_opt_name;
wenzelm
parents: 29601
diff changeset
    14
  val specs: (Attrib.binding * string list) parser
de003023c302 removed old named_spec, spec_name, spec_opt_name;
wenzelm
parents: 29601
diff changeset
    15
  val alt_specs: (Attrib.binding * string) list parser
de003023c302 removed old named_spec, spec_name, spec_opt_name;
wenzelm
parents: 29601
diff changeset
    16
  val where_alt_specs: (Attrib.binding * string) list parser
29312
f369fb19146e added type 'a parser, simplified signature;
wenzelm
parents: 29214
diff changeset
    17
  val xthm: (Facts.ref * Attrib.src list) parser
f369fb19146e added type 'a parser, simplified signature;
wenzelm
parents: 29214
diff changeset
    18
  val xthms1: (Facts.ref * Attrib.src list) list parser
f369fb19146e added type 'a parser, simplified signature;
wenzelm
parents: 29214
diff changeset
    19
  val name_facts: (Attrib.binding * (Facts.ref * Attrib.src list) list) list parser
33287
0f99569d23e1 provide SpecParse.constdecl/constdef, e.g. for quotient_definition;
wenzelm
parents: 30726
diff changeset
    20
  val constdecl: (binding * string option * mixfix) parser
0f99569d23e1 provide SpecParse.constdecl/constdef, e.g. for quotient_definition;
wenzelm
parents: 30726
diff changeset
    21
  val constdef: ((binding * string option * mixfix) option * (Attrib.binding * string)) parser
47067
4ef29b0c568f optional 'includes' element for long theorem statements;
wenzelm
parents: 46922
diff changeset
    22
  val includes: (xstring * Position.T) list parser
29581
b3b33e0298eb binding is alias for Binding.T
haftmann
parents: 29360
diff changeset
    23
  val locale_fixes: (binding * string option * mixfix) list parser
29312
f369fb19146e added type 'a parser, simplified signature;
wenzelm
parents: 29214
diff changeset
    24
  val locale_insts: (string option list * (Attrib.binding * string) list) parser
46922
3717f3878714 source positions for locale and class expressions;
wenzelm
parents: 45592
diff changeset
    25
  val class_expression: string list parser
49754
acafcac41690 more explicit namespace prefix for 'statespace' -- duplicate facts;
wenzelm
parents: 47067
diff changeset
    26
  val locale_prefix: bool -> (string * bool) parser
acafcac41690 more explicit namespace prefix for 'statespace' -- duplicate facts;
wenzelm
parents: 47067
diff changeset
    27
  val locale_keyword: string parser
30726
67388cc4ccb4 locale_expression: mandatory as parameter;
wenzelm
parents: 30720
diff changeset
    28
  val locale_expression: bool -> Expression.expression parser
29312
f369fb19146e added type 'a parser, simplified signature;
wenzelm
parents: 29214
diff changeset
    29
  val context_element: Element.context parser
f369fb19146e added type 'a parser, simplified signature;
wenzelm
parents: 29214
diff changeset
    30
  val statement: (Attrib.binding * (string * string list) list) list parser
f369fb19146e added type 'a parser, simplified signature;
wenzelm
parents: 29214
diff changeset
    31
  val general_statement: (Element.context list * Element.statement) parser
f369fb19146e added type 'a parser, simplified signature;
wenzelm
parents: 29214
diff changeset
    32
  val statement_keyword: string parser
22104
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
    33
end;
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
    34
36952
338c3f8229e4 renamed structure SpecParse to Parse_Spec, keeping the old name as alias for some time;
wenzelm
parents: 36950
diff changeset
    35
structure Parse_Spec: PARSE_SPEC =
22104
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
    36
struct
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
    37
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
    38
(* theorem specifications *)
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
    39
56201
dd2df97b379b tuned signature;
wenzelm
parents: 56029
diff changeset
    40
val attrib = Parse.position Parse.liberal_name -- Parse.!!! Parse.args >> uncurry Args.src;
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 33287
diff changeset
    41
val attribs = Parse.$$$ "[" |-- Parse.list attrib --| Parse.$$$ "]";
22104
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
    42
val opt_attribs = Scan.optional attribs [];
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
    43
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 33287
diff changeset
    44
fun thm_name s = Parse.binding -- opt_attribs --| Parse.$$$ s;
28083
103d9282a946 explicit type Name.binding for higher-specification elements;
wenzelm
parents: 27816
diff changeset
    45
22104
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
    46
fun opt_thm_name s =
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 33287
diff changeset
    47
  Scan.optional ((Parse.binding -- opt_attribs || attribs >> pair Binding.empty) --| Parse.$$$ s)
28965
1de908189869 cleaned up binding module and related code
haftmann
parents: 28722
diff changeset
    48
    Attrib.empty_binding;
22104
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
    49
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 33287
diff changeset
    50
val spec = opt_thm_name ":" -- Parse.prop;
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 33287
diff changeset
    51
val specs = opt_thm_name ":" -- Scan.repeat1 Parse.prop;
22104
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
    52
30481
de003023c302 removed old named_spec, spec_name, spec_opt_name;
wenzelm
parents: 29601
diff changeset
    53
val alt_specs =
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 33287
diff changeset
    54
  Parse.enum1 "|"
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 33287
diff changeset
    55
    (spec --| Scan.option (Scan.ahead (Parse.name || Parse.$$$ "[") -- Parse.!!! (Parse.$$$ "|")));
30481
de003023c302 removed old named_spec, spec_name, spec_opt_name;
wenzelm
parents: 29601
diff changeset
    56
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 33287
diff changeset
    57
val where_alt_specs = Parse.where_ |-- Parse.!!! alt_specs;
22104
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
    58
24013
3063a756611d xthm: added [[declaration]] syntax (abbreviates dummy_thm [att]);
wenzelm
parents: 23919
diff changeset
    59
val xthm =
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 33287
diff changeset
    60
  Parse.$$$ "[" |-- attribs --| Parse.$$$ "]" >> pair (Facts.named "") ||
40793
d21aedaa91e7 added Parse.literal_fact with proper inner_syntax markup (source position);
wenzelm
parents: 36955
diff changeset
    61
  (Parse.literal_fact >> Facts.Fact ||
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 33287
diff changeset
    62
    Parse.position Parse.xname -- Scan.option Attrib.thm_sel >> Facts.Named) -- opt_attribs;
24013
3063a756611d xthm: added [[declaration]] syntax (abbreviates dummy_thm [att]);
wenzelm
parents: 23919
diff changeset
    63
22104
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
    64
val xthms1 = Scan.repeat1 xthm;
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
    65
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 33287
diff changeset
    66
val name_facts = Parse.and_list1 (opt_thm_name "=" -- xthms1);
22104
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
    67
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
    68
33287
0f99569d23e1 provide SpecParse.constdecl/constdef, e.g. for quotient_definition;
wenzelm
parents: 30726
diff changeset
    69
(* basic constant specifications *)
0f99569d23e1 provide SpecParse.constdecl/constdef, e.g. for quotient_definition;
wenzelm
parents: 30726
diff changeset
    70
0f99569d23e1 provide SpecParse.constdecl/constdef, e.g. for quotient_definition;
wenzelm
parents: 30726
diff changeset
    71
val constdecl =
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 33287
diff changeset
    72
  Parse.binding --
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 33287
diff changeset
    73
    (Parse.where_ >> K (NONE, NoSyn) ||
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 33287
diff changeset
    74
      Parse.$$$ "::" |-- Parse.!!! ((Parse.typ >> SOME) -- Parse.opt_mixfix' --| Parse.where_) ||
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 33287
diff changeset
    75
      Scan.ahead (Parse.$$$ "(") |-- Parse.!!! (Parse.mixfix' --| Parse.where_ >> pair NONE))
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 33287
diff changeset
    76
  >> Parse.triple2;
33287
0f99569d23e1 provide SpecParse.constdecl/constdef, e.g. for quotient_definition;
wenzelm
parents: 30726
diff changeset
    77
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 33287
diff changeset
    78
val constdef = Scan.option constdecl -- (opt_thm_name ":" -- Parse.prop);
33287
0f99569d23e1 provide SpecParse.constdecl/constdef, e.g. for quotient_definition;
wenzelm
parents: 30726
diff changeset
    79
0f99569d23e1 provide SpecParse.constdecl/constdef, e.g. for quotient_definition;
wenzelm
parents: 30726
diff changeset
    80
22104
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
    81
(* locale and context elements *)
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
    82
47067
4ef29b0c568f optional 'includes' element for long theorem statements;
wenzelm
parents: 46922
diff changeset
    83
val includes = Parse.$$$ "includes" |-- Parse.!!! (Scan.repeat1 (Parse.position Parse.xname));
4ef29b0c568f optional 'includes' element for long theorem statements;
wenzelm
parents: 46922
diff changeset
    84
22104
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
    85
val locale_fixes =
51654
8450b944e58a just one syntax category "mixfix" -- check structure annotation semantically;
wenzelm
parents: 49754
diff changeset
    86
  Parse.and_list1 (Parse.binding -- Scan.option (Parse.$$$ "::" |-- Parse.typ) -- Parse.mixfix
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 33287
diff changeset
    87
    >> (single o Parse.triple1) ||
42287
d98eb048a2e4 discontinued special treatment of structure Mixfix;
wenzelm
parents: 40800
diff changeset
    88
  Parse.params >> map (fn (x, y) => (x, y, NoSyn))) >> flat;
22104
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
    89
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
    90
val locale_insts =
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 33287
diff changeset
    91
  Scan.optional
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 33287
diff changeset
    92
    (Parse.$$$ "[" |-- Parse.!!! (Scan.repeat1 (Parse.maybe Parse.term) --| Parse.$$$ "]")) [] --
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 33287
diff changeset
    93
  Scan.optional (Parse.where_ |-- Parse.and_list1 (opt_thm_name ":" -- Parse.prop)) [];
22104
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
    94
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
    95
local
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
    96
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
    97
val loc_element =
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 33287
diff changeset
    98
  Parse.$$$ "fixes" |-- Parse.!!! locale_fixes >> Element.Fixes ||
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 33287
diff changeset
    99
  Parse.$$$ "constrains" |--
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 33287
diff changeset
   100
    Parse.!!! (Parse.and_list1 (Parse.name -- (Parse.$$$ "::" |-- Parse.typ)))
22104
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
   101
    >> Element.Constrains ||
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 33287
diff changeset
   102
  Parse.$$$ "assumes" |-- Parse.!!! (Parse.and_list1 (opt_thm_name ":" -- Scan.repeat1 Parse.propp))
22104
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
   103
    >> Element.Assumes ||
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 33287
diff changeset
   104
  Parse.$$$ "defines" |-- Parse.!!! (Parse.and_list1 (opt_thm_name ":" -- Parse.propp))
22104
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
   105
    >> Element.Defines ||
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 33287
diff changeset
   106
  Parse.$$$ "notes" |-- Parse.!!! (Parse.and_list1 (opt_thm_name "=" -- xthms1))
22104
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
   107
    >> (curry Element.Notes "");
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
   108
24869
bad2b2be1f24 added class_expr;
wenzelm
parents: 24014
diff changeset
   109
fun plus1_unless test scan =
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 33287
diff changeset
   110
  scan ::: Scan.repeat (Parse.$$$ "+" |-- Scan.unless test (Parse.!!! scan));
22104
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
   111
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 33287
diff changeset
   112
val instance = Parse.where_ |--
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 33287
diff changeset
   113
  Parse.and_list1 (Parse.name -- (Parse.$$$ "=" |-- Parse.term)) >> Expression.Named ||
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 33287
diff changeset
   114
  Scan.repeat1 (Parse.maybe Parse.term) >> Expression.Positional;
29033
721529248e31 Enable keyword 'structure' in for clause of locale expression.
ballarin
parents: 28965
diff changeset
   115
24869
bad2b2be1f24 added class_expr;
wenzelm
parents: 24014
diff changeset
   116
in
bad2b2be1f24 added class_expr;
wenzelm
parents: 24014
diff changeset
   117
49754
acafcac41690 more explicit namespace prefix for 'statespace' -- duplicate facts;
wenzelm
parents: 47067
diff changeset
   118
fun locale_prefix mandatory =
acafcac41690 more explicit namespace prefix for 'statespace' -- duplicate facts;
wenzelm
parents: 47067
diff changeset
   119
  Scan.optional
acafcac41690 more explicit namespace prefix for 'statespace' -- duplicate facts;
wenzelm
parents: 47067
diff changeset
   120
    (Parse.name --
acafcac41690 more explicit namespace prefix for 'statespace' -- duplicate facts;
wenzelm
parents: 47067
diff changeset
   121
      (Parse.$$$ "!" >> K true || Parse.$$$ "?" >> K false || Scan.succeed mandatory) --|
acafcac41690 more explicit namespace prefix for 'statespace' -- duplicate facts;
wenzelm
parents: 47067
diff changeset
   122
      Parse.$$$ ":")
acafcac41690 more explicit namespace prefix for 'statespace' -- duplicate facts;
wenzelm
parents: 47067
diff changeset
   123
    ("", false);
acafcac41690 more explicit namespace prefix for 'statespace' -- duplicate facts;
wenzelm
parents: 47067
diff changeset
   124
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 33287
diff changeset
   125
val locale_keyword =
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 33287
diff changeset
   126
  Parse.$$$ "fixes" || Parse.$$$ "constrains" || Parse.$$$ "assumes" ||
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 33287
diff changeset
   127
  Parse.$$$ "defines" || Parse.$$$ "notes";
28722
bdb694e18bf8 Minor cleanup.
ballarin
parents: 28710
diff changeset
   128
46922
3717f3878714 source positions for locale and class expressions;
wenzelm
parents: 45592
diff changeset
   129
val class_expression = plus1_unless locale_keyword Parse.class;
24869
bad2b2be1f24 added class_expr;
wenzelm
parents: 24014
diff changeset
   130
30726
67388cc4ccb4 locale_expression: mandatory as parameter;
wenzelm
parents: 30720
diff changeset
   131
fun locale_expression mandatory =
29033
721529248e31 Enable keyword 'structure' in for clause of locale expression.
ballarin
parents: 28965
diff changeset
   132
  let
46922
3717f3878714 source positions for locale and class expressions;
wenzelm
parents: 45592
diff changeset
   133
    val expr2 = Parse.position Parse.xname;
49754
acafcac41690 more explicit namespace prefix for 'statespace' -- duplicate facts;
wenzelm
parents: 47067
diff changeset
   134
    val expr1 = locale_prefix mandatory -- expr2 --
30720
wenzelm
parents: 30513
diff changeset
   135
      Scan.optional instance (Expression.Named []) >> (fn ((p, l), i) => (l, (p, i)));
wenzelm
parents: 30513
diff changeset
   136
    val expr0 = plus1_unless locale_keyword expr1;
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 33287
diff changeset
   137
  in expr0 -- Scan.optional (Parse.$$$ "for" |-- Parse.!!! locale_fixes) [] end;
29033
721529248e31 Enable keyword 'structure' in for clause of locale expression.
ballarin
parents: 28965
diff changeset
   138
44357
5f5649ac8235 tuned Parse.group: delayed failure message;
wenzelm
parents: 42287
diff changeset
   139
val context_element = Parse.group (fn () => "context element") loc_element;
22104
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
   140
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
   141
end;
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
   142
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
   143
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
   144
(* statements *)
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
   145
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 33287
diff changeset
   146
val statement = Parse.and_list1 (opt_thm_name ":" -- Scan.repeat1 Parse.propp);
22104
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
   147
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
   148
val obtain_case =
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 33287
diff changeset
   149
  Parse.parbinding -- (Scan.optional (Parse.simple_fixes --| Parse.where_) [] --
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 33287
diff changeset
   150
    (Parse.and_list1 (Scan.repeat1 Parse.prop) >> flat));
22104
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
   151
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
   152
val general_statement =
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
   153
  statement >> (fn x => ([], Element.Shows x)) ||
28722
bdb694e18bf8 Minor cleanup.
ballarin
parents: 28710
diff changeset
   154
  Scan.repeat context_element --
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 33287
diff changeset
   155
   (Parse.$$$ "obtains" |-- Parse.!!! (Parse.enum1 "|" obtain_case) >> Element.Obtains ||
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 33287
diff changeset
   156
    Parse.$$$ "shows" |-- Parse.!!! statement >> Element.Shows);
22104
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
   157
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 33287
diff changeset
   158
val statement_keyword = Parse.$$$ "obtains" || Parse.$$$ "shows";
22104
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
   159
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
   160
end;