src/Pure/Isar/spec_parse.ML
author wenzelm
Wed, 19 Mar 2008 22:27:57 +0100
changeset 26336 a0e2b706ce73
parent 25999 f8bcd311d501
child 26361 7946f459c6c8
permissions -rw-r--r--
renamed datatype thmref to Facts.ref, tuned interfaces;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
22104
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/Isar/spec_parse.ML
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
     3
    Author:     Makarius
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
     4
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
     5
Parsers for complex specifications.
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
     6
*)
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
     7
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
     8
signature SPEC_PARSE =
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
     9
sig
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
    10
  type token
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
    11
  val attrib: OuterLex.token list -> Attrib.src * token list
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
    12
  val attribs: token list -> Attrib.src list * token list
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
    13
  val opt_attribs: token list -> Attrib.src list * token list
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
    14
  val thm_name: string -> token list -> (bstring * Attrib.src list) * token list
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
    15
  val opt_thm_name: string -> token list -> (bstring * Attrib.src list) * token list
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
    16
  val spec: token list -> ((bstring * Attrib.src list) * string list) * token list
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
    17
  val named_spec: token list -> ((bstring * Attrib.src list) * string list) * token list
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
    18
  val spec_name: token list -> ((bstring * string) * Attrib.src list) * token list
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
    19
  val spec_opt_name: token list -> ((bstring * string) * Attrib.src list) * token list
26336
a0e2b706ce73 renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents: 25999
diff changeset
    20
  val xthm: token list -> (Facts.ref * Attrib.src list) * token list
a0e2b706ce73 renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents: 25999
diff changeset
    21
  val xthms1: token list -> (Facts.ref * Attrib.src list) list * token list
22104
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
    22
  val name_facts: token list ->
26336
a0e2b706ce73 renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents: 25999
diff changeset
    23
    ((bstring * Attrib.src list) * (Facts.ref * Attrib.src list) list) list * token list
22104
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
    24
  val locale_mixfix: token list -> mixfix * token list
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
    25
  val locale_fixes: token list -> (string * string option * mixfix) list * token list
25094
ba43514068fd Interpretation equations may have name and/or attribute.
ballarin
parents: 24869
diff changeset
    26
  val locale_insts: token list ->
ba43514068fd Interpretation equations may have name and/or attribute.
ballarin
parents: 24869
diff changeset
    27
    (string option list * ((bstring * Attrib.src list) * string) list) * token list
24869
bad2b2be1f24 added class_expr;
wenzelm
parents: 24014
diff changeset
    28
  val class_expr: token list -> string list * token list
22104
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
    29
  val locale_expr: token list -> Locale.expr * token list
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
    30
  val locale_keyword: token list -> string * token list
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
    31
  val locale_element: token list -> Element.context Locale.element * token list
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
    32
  val context_element: token list -> Element.context * token list
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
    33
  val statement: token list ->
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
    34
    ((bstring * Attrib.src list) * (string * string list) list) list * token list
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
    35
  val general_statement: token list ->
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
    36
    (Element.context Locale.element list * Element.statement) * OuterLex.token list
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
    37
  val statement_keyword: token list -> string * token list
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
    38
  val specification: token list ->
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
    39
    (string *
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
    40
      (((bstring * Attrib.src list) * string list) list * (string * string option) list)) list *
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
    41
    token list
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
    42
end;
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
    43
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
    44
structure SpecParse: SPEC_PARSE =
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
    45
struct
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
    46
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
    47
structure P = OuterParse;
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
    48
type token = P.token;
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
    49
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
    50
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
    51
(* theorem specifications *)
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
    52
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
    53
val attrib = P.position ((P.keyword_sid || P.xname) -- P.!!! P.arguments) >> Args.src;
24014
d3873741678d attribs: not cut (!!!);
wenzelm
parents: 24013
diff changeset
    54
val attribs = P.$$$ "[" |-- P.list attrib --| P.$$$ "]";
22104
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
    55
val opt_attribs = Scan.optional attribs [];
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
    56
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
    57
fun thm_name s = P.name -- opt_attribs --| P.$$$ s;
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
    58
fun opt_thm_name s =
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
    59
  Scan.optional ((P.name -- opt_attribs || (attribs >> pair "")) --| P.$$$ s) ("", []);
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
    60
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
    61
val spec = opt_thm_name ":" -- Scan.repeat1 P.prop;
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
    62
val named_spec = thm_name ":" -- Scan.repeat1 P.prop;
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
    63
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
    64
val spec_name = thm_name ":" -- P.prop >> (fn ((x, y), z) => ((x, z), y));
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
    65
val spec_opt_name = opt_thm_name ":" -- P.prop >> (fn ((x, y), z) => ((x, z), y));
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
    66
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
    67
val thm_sel = P.$$$ "(" |-- P.list1
26336
a0e2b706ce73 renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents: 25999
diff changeset
    68
 (P.nat --| P.minus -- P.nat >> Facts.FromTo ||
a0e2b706ce73 renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents: 25999
diff changeset
    69
  P.nat --| P.minus >> Facts.From ||
a0e2b706ce73 renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents: 25999
diff changeset
    70
  P.nat >> Facts.Single) --| P.$$$ ")";
22104
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
    71
24013
3063a756611d xthm: added [[declaration]] syntax (abbreviates dummy_thm [att]);
wenzelm
parents: 23919
diff changeset
    72
val xthm =
26336
a0e2b706ce73 renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents: 25999
diff changeset
    73
  P.$$$ "[" |-- attribs --| P.$$$ "]" >> pair (Facts.Named ("", NONE)) ||
a0e2b706ce73 renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents: 25999
diff changeset
    74
  (P.alt_string >> Facts.Fact || P.xname -- Scan.option thm_sel >> Facts.Named) -- opt_attribs;
24013
3063a756611d xthm: added [[declaration]] syntax (abbreviates dummy_thm [att]);
wenzelm
parents: 23919
diff changeset
    75
22104
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
    76
val xthms1 = Scan.repeat1 xthm;
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
    77
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
    78
val name_facts = P.and_list1 (opt_thm_name "=" -- xthms1);
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
    79
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
    80
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
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
    83
val locale_mixfix = P.$$$ "(" -- P.$$$ "structure" -- P.!!! (P.$$$ ")") >> K Structure || P.mixfix;
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
    84
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
    85
val locale_fixes =
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
    86
  P.and_list1 (P.name -- Scan.option (P.$$$ "::" |-- P.typ) -- locale_mixfix
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
    87
    >> (single o P.triple1) ||
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
    88
  P.params >> map Syntax.no_syn) >> flat;
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 =
22658
263d42253f53 Experimental interpretation code for definitions.
ballarin
parents: 22104
diff changeset
    91
  Scan.optional (P.$$$ "[" |-- P.!!! (Scan.repeat1 (P.maybe P.term) --| P.$$$ "]")) []
25094
ba43514068fd Interpretation equations may have name and/or attribute.
ballarin
parents: 24869
diff changeset
    92
  -- Scan.optional (P.$$$ "where" |-- P.and_list1 (opt_thm_name ":" -- P.prop)) [];
22104
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
    93
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
    94
local
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
    95
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
    96
val loc_keyword = P.$$$ "fixes" || P.$$$ "constrains" || P.$$$ "assumes" ||
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
    97
   P.$$$ "defines" || P.$$$ "notes" || P.$$$ "includes";
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
    98
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
    99
val loc_element =
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
   100
  P.$$$ "fixes" |-- P.!!! locale_fixes >> Element.Fixes ||
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
   101
  P.$$$ "constrains" |-- P.!!! (P.and_list1 (P.name -- (P.$$$ "::" |-- P.typ)))
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
   102
    >> Element.Constrains ||
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
   103
  P.$$$ "assumes" |-- P.!!! (P.and_list1 (opt_thm_name ":" -- Scan.repeat1 P.propp))
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
   104
    >> Element.Assumes ||
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
   105
  P.$$$ "defines" |-- P.!!! (P.and_list1 (opt_thm_name ":" -- P.propp))
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
   106
    >> Element.Defines ||
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
   107
  P.$$$ "notes" |-- P.!!! (P.and_list1 (opt_thm_name "=" -- xthms1))
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
   108
    >> (curry Element.Notes "");
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
   109
24869
bad2b2be1f24 added class_expr;
wenzelm
parents: 24014
diff changeset
   110
fun plus1_unless test scan =
25999
f8bcd311d501 added ::: / @@@ scanner combinators;
wenzelm
parents: 25094
diff changeset
   111
  scan ::: Scan.repeat (P.$$$ "+" |-- Scan.unless test (P.!!! scan));
22104
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
   112
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
   113
val rename = P.name -- Scan.option P.mixfix;
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
   114
24869
bad2b2be1f24 added class_expr;
wenzelm
parents: 24014
diff changeset
   115
in
bad2b2be1f24 added class_expr;
wenzelm
parents: 24014
diff changeset
   116
bad2b2be1f24 added class_expr;
wenzelm
parents: 24014
diff changeset
   117
val class_expr = plus1_unless loc_keyword P.xname;
bad2b2be1f24 added class_expr;
wenzelm
parents: 24014
diff changeset
   118
bad2b2be1f24 added class_expr;
wenzelm
parents: 24014
diff changeset
   119
val locale_expr =
22104
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
   120
  let
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
   121
    fun expr2 x = (P.xname >> Locale.Locale || P.$$$ "(" |-- P.!!! (expr0 --| P.$$$ ")")) x
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
   122
    and expr1 x = (expr2 -- Scan.repeat1 (P.maybe rename) >> Locale.Rename || expr2) x
24869
bad2b2be1f24 added class_expr;
wenzelm
parents: 24014
diff changeset
   123
    and expr0 x = (plus1_unless loc_keyword expr1 >> (fn [e] => e | es => Locale.Merge es)) x;
22104
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
   124
  in expr0 end;
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
   125
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
   126
val locale_keyword = loc_keyword;
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
   127
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
   128
val locale_element = P.group "locale element"
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
   129
  (loc_element >> Locale.Elem || P.$$$ "includes" |-- P.!!! locale_expr >> Locale.Expr);
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
   130
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
   131
val context_element = P.group "context element" loc_element;
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
   132
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
   133
end;
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
   134
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
   135
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
   136
(* statements *)
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
   137
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
   138
val statement = P.and_list1 (opt_thm_name ":" -- Scan.repeat1 P.propp);
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
   139
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
   140
val obtain_case =
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
   141
  P.parname -- (Scan.optional (P.simple_fixes --| P.$$$ "where") [] --
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
   142
    (P.and_list1 (Scan.repeat1 P.prop) >> flat));
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
val general_statement =
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
   145
  statement >> (fn x => ([], Element.Shows x)) ||
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
   146
  Scan.repeat locale_element --
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
   147
   (P.$$$ "obtains" |-- P.!!! (P.enum1 "|" obtain_case) >> Element.Obtains ||
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
   148
    P.$$$ "shows" |-- P.!!! statement >> Element.Shows);
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
   149
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
   150
val statement_keyword = P.$$$ "obtains" || P.$$$ "shows";
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
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
   153
(* specifications *)
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
   154
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
   155
val specification = P.enum1 "|" (P.parname -- (P.and_list1 spec -- P.for_simple_fixes));
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
   156
e8a1c88be824 Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff changeset
   157
end;