src/Pure/Isar/parse.ML
author wenzelm
Sun, 01 May 2011 18:05:09 +0200
changeset 42519 8ac7e96f913b
parent 42326 e2d22eb4aeb9
child 42657 6b404fe40877
permissions -rw-r--r--
tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
36949
080e85d46108 renamed structure OuterKeyword to Keyword and OuterParse to Parse, keeping the old names as legacy aliases for some time;
wenzelm
parents: 35838
diff changeset
     1
(*  Title:      Pure/Isar/parse.ML
5826
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
     2
    Author:     Markus Wenzel, TU Muenchen
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
     3
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
     4
Generic parsers for Isabelle/Isar outer syntax.
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
     5
*)
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
     6
36949
080e85d46108 renamed structure OuterKeyword to Keyword and OuterParse to Parse, keeping the old names as legacy aliases for some time;
wenzelm
parents: 35838
diff changeset
     7
signature PARSE =
5826
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
     8
sig
36959
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 36955
diff changeset
     9
  type 'a parser = Token.T list -> 'a * Token.T list
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 36955
diff changeset
    10
  type 'a context_parser = Context.generic * Token.T list -> 'a * (Context.generic * Token.T list)
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 36955
diff changeset
    11
  val group: string -> (Token.T list -> 'a) -> Token.T list -> 'a
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 36955
diff changeset
    12
  val !!! : (Token.T list -> 'a) -> Token.T list -> 'a
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 36955
diff changeset
    13
  val !!!! : (Token.T list -> 'a) -> Token.T list -> 'a
12047
e151e66da2d6 added locale_element;
wenzelm
parents: 11792
diff changeset
    14
  val triple1: ('a * 'b) * 'c -> 'a * 'b * 'c
e151e66da2d6 added locale_element;
wenzelm
parents: 11792
diff changeset
    15
  val triple2: 'a * ('b * 'c) -> 'a * 'b * 'c
e151e66da2d6 added locale_element;
wenzelm
parents: 11792
diff changeset
    16
  val triple_swap: ('a * 'b) * 'c -> ('a * 'c) * 'b
36959
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 36955
diff changeset
    17
  val not_eof: Token.T parser
42326
e2d22eb4aeb9 some position reports for 'translations';
wenzelm
parents: 42300
diff changeset
    18
  val position: 'a parser -> ('a * Position.T) parser
e2d22eb4aeb9 some position reports for 'translations';
wenzelm
parents: 42300
diff changeset
    19
  val inner_syntax: 'a parser -> string parser
29310
1a633304fa5e added type 'a parser, simplified signature;
wenzelm
parents: 28965
diff changeset
    20
  val command: string parser
1a633304fa5e added type 'a parser, simplified signature;
wenzelm
parents: 28965
diff changeset
    21
  val keyword: string parser
1a633304fa5e added type 'a parser, simplified signature;
wenzelm
parents: 28965
diff changeset
    22
  val short_ident: string parser
1a633304fa5e added type 'a parser, simplified signature;
wenzelm
parents: 28965
diff changeset
    23
  val long_ident: string parser
1a633304fa5e added type 'a parser, simplified signature;
wenzelm
parents: 28965
diff changeset
    24
  val sym_ident: string parser
1a633304fa5e added type 'a parser, simplified signature;
wenzelm
parents: 28965
diff changeset
    25
  val minus: string parser
1a633304fa5e added type 'a parser, simplified signature;
wenzelm
parents: 28965
diff changeset
    26
  val term_var: string parser
1a633304fa5e added type 'a parser, simplified signature;
wenzelm
parents: 28965
diff changeset
    27
  val type_ident: string parser
1a633304fa5e added type 'a parser, simplified signature;
wenzelm
parents: 28965
diff changeset
    28
  val type_var: string parser
1a633304fa5e added type 'a parser, simplified signature;
wenzelm
parents: 28965
diff changeset
    29
  val number: string parser
40290
47f572aff50a support for floating-point tokens in outer syntax (coinciding with inner syntax version);
wenzelm
parents: 36959
diff changeset
    30
  val float_number: string parser
29310
1a633304fa5e added type 'a parser, simplified signature;
wenzelm
parents: 28965
diff changeset
    31
  val string: string parser
1a633304fa5e added type 'a parser, simplified signature;
wenzelm
parents: 28965
diff changeset
    32
  val alt_string: string parser
1a633304fa5e added type 'a parser, simplified signature;
wenzelm
parents: 28965
diff changeset
    33
  val verbatim: string parser
1a633304fa5e added type 'a parser, simplified signature;
wenzelm
parents: 28965
diff changeset
    34
  val sync: string parser
1a633304fa5e added type 'a parser, simplified signature;
wenzelm
parents: 28965
diff changeset
    35
  val eof: string parser
1a633304fa5e added type 'a parser, simplified signature;
wenzelm
parents: 28965
diff changeset
    36
  val keyword_with: (string -> bool) -> string parser
1a633304fa5e added type 'a parser, simplified signature;
wenzelm
parents: 28965
diff changeset
    37
  val keyword_ident_or_symbolic: string parser
1a633304fa5e added type 'a parser, simplified signature;
wenzelm
parents: 28965
diff changeset
    38
  val $$$ : string -> string parser
1a633304fa5e added type 'a parser, simplified signature;
wenzelm
parents: 28965
diff changeset
    39
  val reserved: string -> string parser
1a633304fa5e added type 'a parser, simplified signature;
wenzelm
parents: 28965
diff changeset
    40
  val semicolon: string parser
1a633304fa5e added type 'a parser, simplified signature;
wenzelm
parents: 28965
diff changeset
    41
  val underscore: string parser
1a633304fa5e added type 'a parser, simplified signature;
wenzelm
parents: 28965
diff changeset
    42
  val maybe: 'a parser -> 'a option parser
1a633304fa5e added type 'a parser, simplified signature;
wenzelm
parents: 28965
diff changeset
    43
  val tag_name: string parser
1a633304fa5e added type 'a parser, simplified signature;
wenzelm
parents: 28965
diff changeset
    44
  val tags: string list parser
1a633304fa5e added type 'a parser, simplified signature;
wenzelm
parents: 28965
diff changeset
    45
  val opt_unit: unit parser
1a633304fa5e added type 'a parser, simplified signature;
wenzelm
parents: 28965
diff changeset
    46
  val opt_keyword: string -> bool parser
1a633304fa5e added type 'a parser, simplified signature;
wenzelm
parents: 28965
diff changeset
    47
  val begin: string parser
1a633304fa5e added type 'a parser, simplified signature;
wenzelm
parents: 28965
diff changeset
    48
  val opt_begin: bool parser
1a633304fa5e added type 'a parser, simplified signature;
wenzelm
parents: 28965
diff changeset
    49
  val nat: int parser
1a633304fa5e added type 'a parser, simplified signature;
wenzelm
parents: 28965
diff changeset
    50
  val int: int parser
40290
47f572aff50a support for floating-point tokens in outer syntax (coinciding with inner syntax version);
wenzelm
parents: 36959
diff changeset
    51
  val real: real parser
29310
1a633304fa5e added type 'a parser, simplified signature;
wenzelm
parents: 28965
diff changeset
    52
  val enum: string -> 'a parser -> 'a list parser
1a633304fa5e added type 'a parser, simplified signature;
wenzelm
parents: 28965
diff changeset
    53
  val enum1: string -> 'a parser -> 'a list parser
1a633304fa5e added type 'a parser, simplified signature;
wenzelm
parents: 28965
diff changeset
    54
  val and_list: 'a parser -> 'a list parser
1a633304fa5e added type 'a parser, simplified signature;
wenzelm
parents: 28965
diff changeset
    55
  val and_list1: 'a parser -> 'a list parser
30511
5c628a39b7cb pervasive types 'a parser and 'a context_parser;
wenzelm
parents: 30339
diff changeset
    56
  val enum': string -> 'a context_parser -> 'a list context_parser
5c628a39b7cb pervasive types 'a parser and 'a context_parser;
wenzelm
parents: 30339
diff changeset
    57
  val enum1': string -> 'a context_parser -> 'a list context_parser
5c628a39b7cb pervasive types 'a parser and 'a context_parser;
wenzelm
parents: 30339
diff changeset
    58
  val and_list': 'a context_parser -> 'a list context_parser
5c628a39b7cb pervasive types 'a parser and 'a context_parser;
wenzelm
parents: 30339
diff changeset
    59
  val and_list1': 'a context_parser -> 'a list context_parser
29310
1a633304fa5e added type 'a parser, simplified signature;
wenzelm
parents: 28965
diff changeset
    60
  val list: 'a parser -> 'a list parser
1a633304fa5e added type 'a parser, simplified signature;
wenzelm
parents: 28965
diff changeset
    61
  val list1: 'a parser -> 'a list parser
1a633304fa5e added type 'a parser, simplified signature;
wenzelm
parents: 28965
diff changeset
    62
  val name: bstring parser
29581
b3b33e0298eb binding is alias for Binding.T
haftmann
parents: 29310
diff changeset
    63
  val binding: binding parser
29310
1a633304fa5e added type 'a parser, simplified signature;
wenzelm
parents: 28965
diff changeset
    64
  val xname: xstring parser
1a633304fa5e added type 'a parser, simplified signature;
wenzelm
parents: 28965
diff changeset
    65
  val text: string parser
1a633304fa5e added type 'a parser, simplified signature;
wenzelm
parents: 28965
diff changeset
    66
  val path: Path.T parser
40800
330eb65c9469 Parse.liberal_name for document antiquotations and attributes;
wenzelm
parents: 40793
diff changeset
    67
  val liberal_name: xstring parser
29310
1a633304fa5e added type 'a parser, simplified signature;
wenzelm
parents: 28965
diff changeset
    68
  val parname: string parser
29581
b3b33e0298eb binding is alias for Binding.T
haftmann
parents: 29310
diff changeset
    69
  val parbinding: binding parser
29310
1a633304fa5e added type 'a parser, simplified signature;
wenzelm
parents: 28965
diff changeset
    70
  val sort: string parser
1a633304fa5e added type 'a parser, simplified signature;
wenzelm
parents: 28965
diff changeset
    71
  val arity: (string * string list * string) parser
1a633304fa5e added type 'a parser, simplified signature;
wenzelm
parents: 28965
diff changeset
    72
  val multi_arity: (string list * string list * string) parser
1a633304fa5e added type 'a parser, simplified signature;
wenzelm
parents: 28965
diff changeset
    73
  val type_args: string list parser
35838
c8bd075c4de8 support type arguments with sort constraints;
wenzelm
parents: 35351
diff changeset
    74
  val type_args_constrained: (string * string option) list parser
29310
1a633304fa5e added type 'a parser, simplified signature;
wenzelm
parents: 28965
diff changeset
    75
  val typ_group: string parser
1a633304fa5e added type 'a parser, simplified signature;
wenzelm
parents: 28965
diff changeset
    76
  val typ: string parser
1a633304fa5e added type 'a parser, simplified signature;
wenzelm
parents: 28965
diff changeset
    77
  val mixfix: mixfix parser
1a633304fa5e added type 'a parser, simplified signature;
wenzelm
parents: 28965
diff changeset
    78
  val mixfix': mixfix parser
1a633304fa5e added type 'a parser, simplified signature;
wenzelm
parents: 28965
diff changeset
    79
  val opt_mixfix: mixfix parser
1a633304fa5e added type 'a parser, simplified signature;
wenzelm
parents: 28965
diff changeset
    80
  val opt_mixfix': mixfix parser
1a633304fa5e added type 'a parser, simplified signature;
wenzelm
parents: 28965
diff changeset
    81
  val where_: string parser
42299
06e93f257d0e tuned signature;
wenzelm
parents: 42297
diff changeset
    82
  val const_decl: (string * string * mixfix) parser
30339
3fc32dd7a647 added const_binding;
wenzelm
parents: 30223
diff changeset
    83
  val const_binding: (binding * string * mixfix) parser
29581
b3b33e0298eb binding is alias for Binding.T
haftmann
parents: 29310
diff changeset
    84
  val params: (binding * string option) list parser
b3b33e0298eb binding is alias for Binding.T
haftmann
parents: 29310
diff changeset
    85
  val simple_fixes: (binding * string option) list parser
b3b33e0298eb binding is alias for Binding.T
haftmann
parents: 29310
diff changeset
    86
  val fixes: (binding * string option * mixfix) list parser
b3b33e0298eb binding is alias for Binding.T
haftmann
parents: 29310
diff changeset
    87
  val for_fixes: (binding * string option * mixfix) list parser
b3b33e0298eb binding is alias for Binding.T
haftmann
parents: 29310
diff changeset
    88
  val for_simple_fixes: (binding * string option) list parser
30573
49899f26fbd1 de-camelized Symbol_Pos;
wenzelm
parents: 30511
diff changeset
    89
  val ML_source: (Symbol_Pos.text * Position.T) parser
49899f26fbd1 de-camelized Symbol_Pos;
wenzelm
parents: 30511
diff changeset
    90
  val doc_source: (Symbol_Pos.text * Position.T) parser
29310
1a633304fa5e added type 'a parser, simplified signature;
wenzelm
parents: 28965
diff changeset
    91
  val term_group: string parser
1a633304fa5e added type 'a parser, simplified signature;
wenzelm
parents: 28965
diff changeset
    92
  val prop_group: string parser
1a633304fa5e added type 'a parser, simplified signature;
wenzelm
parents: 28965
diff changeset
    93
  val term: string parser
1a633304fa5e added type 'a parser, simplified signature;
wenzelm
parents: 28965
diff changeset
    94
  val prop: string parser
42300
0d1cbc1fe579 notation: proper markup for type constructor / constant;
wenzelm
parents: 42299
diff changeset
    95
  val type_const: string parser
0d1cbc1fe579 notation: proper markup for type constructor / constant;
wenzelm
parents: 42299
diff changeset
    96
  val const: string parser
40793
d21aedaa91e7 added Parse.literal_fact with proper inner_syntax markup (source position);
wenzelm
parents: 40296
diff changeset
    97
  val literal_fact: string parser
29310
1a633304fa5e added type 'a parser, simplified signature;
wenzelm
parents: 28965
diff changeset
    98
  val propp: (string * string list) parser
1a633304fa5e added type 'a parser, simplified signature;
wenzelm
parents: 28965
diff changeset
    99
  val termp: (string * string list) parser
1a633304fa5e added type 'a parser, simplified signature;
wenzelm
parents: 28965
diff changeset
   100
  val target: xstring parser
1a633304fa5e added type 'a parser, simplified signature;
wenzelm
parents: 28965
diff changeset
   101
  val opt_target: xstring option parser
5826
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   102
end;
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   103
36949
080e85d46108 renamed structure OuterKeyword to Keyword and OuterParse to Parse, keeping the old names as legacy aliases for some time;
wenzelm
parents: 35838
diff changeset
   104
structure Parse: PARSE =
5826
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   105
struct
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   106
36959
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 36955
diff changeset
   107
type 'a parser = Token.T list -> 'a * Token.T list;
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 36955
diff changeset
   108
type 'a context_parser = Context.generic * Token.T list -> 'a * (Context.generic * Token.T list);
29310
1a633304fa5e added type 'a parser, simplified signature;
wenzelm
parents: 28965
diff changeset
   109
5826
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   110
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   111
(** error handling **)
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   112
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   113
(* group atomic parsers (no cuts!) *)
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   114
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   115
fun fail_with s = Scan.fail_with
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   116
  (fn [] => s ^ " expected (past end-of-file!)"
42519
wenzelm
parents: 42326
diff changeset
   117
    | tok :: _ =>
36959
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 36955
diff changeset
   118
        (case Token.text_of tok of
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 36955
diff changeset
   119
          (txt, "") =>
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 36955
diff changeset
   120
            s ^ " expected,\nbut " ^ txt ^ Token.pos_of tok ^ " was found"
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 36955
diff changeset
   121
        | (txt1, txt2) =>
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 36955
diff changeset
   122
            s ^ " expected,\nbut " ^ txt1 ^ Token.pos_of tok ^ " was found:\n" ^ txt2));
5826
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   123
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   124
fun group s scan = scan || fail_with s;
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   125
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   126
5877
ee214dec5657 removed args, args1, thm_xname;
wenzelm
parents: 5826
diff changeset
   127
(* cut *)
5826
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   128
8581
5c7ed2af8bfb !!!! = cut "Corrupted outer syntax in presentation";
wenzelm
parents: 8350
diff changeset
   129
fun cut kind scan =
5826
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   130
  let
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   131
    fun get_pos [] = " (past end-of-file!)"
36959
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 36955
diff changeset
   132
      | get_pos (tok :: _) = Token.pos_of tok;
5826
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   133
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15456
diff changeset
   134
    fun err (toks, NONE) = kind ^ get_pos toks
25625
35e2aa8b8b03 nested commands: avoid nested errors;
wenzelm
parents: 25541
diff changeset
   135
      | err (toks, SOME msg) =
35e2aa8b8b03 nested commands: avoid nested errors;
wenzelm
parents: 25541
diff changeset
   136
          if String.isPrefix kind msg then msg
35e2aa8b8b03 nested commands: avoid nested errors;
wenzelm
parents: 25541
diff changeset
   137
          else kind ^ get_pos toks ^ ": " ^ msg;
5826
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   138
  in Scan.!! err scan end;
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   139
8586
e451c4865548 made SML/NJ happy;
wenzelm
parents: 8581
diff changeset
   140
fun !!! scan = cut "Outer syntax error" scan;
e451c4865548 made SML/NJ happy;
wenzelm
parents: 8581
diff changeset
   141
fun !!!! scan = cut "Corrupted outer syntax in presentation" scan;
8581
5c7ed2af8bfb !!!! = cut "Corrupted outer syntax in presentation";
wenzelm
parents: 8350
diff changeset
   142
5826
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   143
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   144
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   145
(** basic parsers **)
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   146
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   147
(* utils *)
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   148
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   149
fun triple1 ((x, y), z) = (x, y, z);
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   150
fun triple2 (x, (y, z)) = (x, y, z);
6430
69400c97d3bf triple_swap;
wenzelm
parents: 6398
diff changeset
   151
fun triple_swap ((x, y), z) = ((x, z), y);
5826
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   152
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   153
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   154
(* tokens *)
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   155
27815
2d36632bc5de unified Args.T with OuterLex.token;
wenzelm
parents: 27788
diff changeset
   156
fun RESET_VALUE atom = (*required for all primitive parsers*)
36959
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 36955
diff changeset
   157
  Scan.ahead (Scan.one (K true)) -- atom >> (fn (arg, x) => (Token.assign NONE arg; x));
27815
2d36632bc5de unified Args.T with OuterLex.token;
wenzelm
parents: 27788
diff changeset
   158
2d36632bc5de unified Args.T with OuterLex.token;
wenzelm
parents: 27788
diff changeset
   159
36959
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 36955
diff changeset
   160
val not_eof = RESET_VALUE (Scan.one Token.not_eof);
15703
727ef1b8b3ee *** empty log message ***
wenzelm
parents: 15570
diff changeset
   161
36959
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 36955
diff changeset
   162
fun position scan = (Scan.ahead not_eof >> Token.position_of) -- scan >> Library.swap;
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 36955
diff changeset
   163
fun source_position atom = Scan.ahead atom |-- not_eof >> Token.source_position_of;
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 36955
diff changeset
   164
fun inner_syntax atom = Scan.ahead atom |-- not_eof >> Token.source_of;
5826
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   165
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   166
fun kind k =
36959
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 36955
diff changeset
   167
  group (Token.str_of_kind k) (RESET_VALUE (Scan.one (Token.is_kind k) >> Token.content_of));
5826
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   168
36959
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 36955
diff changeset
   169
val command = kind Token.Command;
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 36955
diff changeset
   170
val keyword = kind Token.Keyword;
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 36955
diff changeset
   171
val short_ident = kind Token.Ident;
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 36955
diff changeset
   172
val long_ident = kind Token.LongIdent;
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 36955
diff changeset
   173
val sym_ident = kind Token.SymIdent;
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 36955
diff changeset
   174
val term_var = kind Token.Var;
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 36955
diff changeset
   175
val type_ident = kind Token.TypeIdent;
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 36955
diff changeset
   176
val type_var = kind Token.TypeVar;
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 36955
diff changeset
   177
val number = kind Token.Nat;
40290
47f572aff50a support for floating-point tokens in outer syntax (coinciding with inner syntax version);
wenzelm
parents: 36959
diff changeset
   178
val float_number = kind Token.Float;
36959
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 36955
diff changeset
   179
val string = kind Token.String;
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 36955
diff changeset
   180
val alt_string = kind Token.AltString;
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 36955
diff changeset
   181
val verbatim = kind Token.Verbatim;
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 36955
diff changeset
   182
val sync = kind Token.Sync;
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 36955
diff changeset
   183
val eof = kind Token.EOF;
5826
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   184
36959
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 36955
diff changeset
   185
fun keyword_with pred = RESET_VALUE (Scan.one (Token.keyword_with pred) >> Token.content_of);
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 36955
diff changeset
   186
val keyword_ident_or_symbolic = keyword_with Token.ident_or_symbolic;
27815
2d36632bc5de unified Args.T with OuterLex.token;
wenzelm
parents: 27788
diff changeset
   187
5826
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   188
fun $$$ x =
36959
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 36955
diff changeset
   189
  group (Token.str_of_kind Token.Keyword ^ " " ^ quote x) (keyword_with (fn y => x = y));
9131
cd17637c917f added semicolon;
wenzelm
parents: 9037
diff changeset
   190
16030
bbfb2f1378b3 added reserved;
wenzelm
parents: 15979
diff changeset
   191
fun reserved x =
27753
94b672153b49 sort/typ/term/prop: inner_syntax markup encodes original source position;
wenzelm
parents: 27737
diff changeset
   192
  group ("reserved identifier " ^ quote x)
36959
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 36955
diff changeset
   193
    (RESET_VALUE (Scan.one (Token.ident_with (fn y => x = y)) >> Token.content_of));
16030
bbfb2f1378b3 added reserved;
wenzelm
parents: 15979
diff changeset
   194
9131
cd17637c917f added semicolon;
wenzelm
parents: 9037
diff changeset
   195
val semicolon = $$$ ";";
5826
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   196
15703
727ef1b8b3ee *** empty log message ***
wenzelm
parents: 15570
diff changeset
   197
val minus = sym_ident :-- (fn "-" => Scan.succeed () | _ => Scan.fail) >> #1;
11792
311eee3d63b6 parser for underscore (actually a symbolic identifier!);
wenzelm
parents: 11651
diff changeset
   198
val underscore = sym_ident :-- (fn "_" => Scan.succeed () | _ => Scan.fail) >> #1;
15703
727ef1b8b3ee *** empty log message ***
wenzelm
parents: 15570
diff changeset
   199
fun maybe scan = underscore >> K NONE || scan >> SOME;
11792
311eee3d63b6 parser for underscore (actually a symbolic identifier!);
wenzelm
parents: 11651
diff changeset
   200
14835
695ee8ad0bb6 Library.read_int; Output.output;
wenzelm
parents: 14646
diff changeset
   201
val nat = number >> (#1 o Library.read_int o Symbol.explode);
27815
2d36632bc5de unified Args.T with OuterLex.token;
wenzelm
parents: 27788
diff changeset
   202
val int = Scan.optional (minus >> K ~1) 1 -- nat >> op *;
40296
ac4d75f86d97 syntax category "real" subsumes plain "int";
wenzelm
parents: 40290
diff changeset
   203
val real = float_number >> (the o Real.fromString) || int >> Real.fromInt;
5826
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   204
17070
3b29a01417f8 added tags parser;
wenzelm
parents: 16736
diff changeset
   205
val tag_name = group "tag name" (short_ident || string);
3b29a01417f8 added tags parser;
wenzelm
parents: 16736
diff changeset
   206
val tags = Scan.repeat ($$$ "%" |-- !!! tag_name);
3b29a01417f8 added tags parser;
wenzelm
parents: 16736
diff changeset
   207
7930
220892918bd1 added opt_unit (from isar_syn.ML);
wenzelm
parents: 7477
diff changeset
   208
val opt_unit = Scan.optional ($$$ "(" -- $$$ ")" >> (K ())) ();
14646
f5f2340398f9 added opt_keyword, mixfix';
wenzelm
parents: 14605
diff changeset
   209
fun opt_keyword s = Scan.optional ($$$ "(" |-- !!! (($$$ s >> K true) --| $$$ ")")) false;
f5f2340398f9 added opt_keyword, mixfix';
wenzelm
parents: 14605
diff changeset
   210
20983
d4500b9b220e added begin parser;
wenzelm
parents: 20961
diff changeset
   211
val begin = $$$ "begin";
d4500b9b220e added begin parser;
wenzelm
parents: 20961
diff changeset
   212
val opt_begin = Scan.optional (begin >> K true) false;
20961
555d27f2c210 added opt_begin;
wenzelm
parents: 20273
diff changeset
   213
5826
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   214
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   215
(* enumerations *)
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   216
25999
f8bcd311d501 added ::: / @@@ scanner combinators;
wenzelm
parents: 25795
diff changeset
   217
fun enum1 sep scan = scan ::: Scan.repeat ($$$ sep |-- !!! scan);
5826
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   218
fun enum sep scan = enum1 sep scan || Scan.succeed [];
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   219
27815
2d36632bc5de unified Args.T with OuterLex.token;
wenzelm
parents: 27788
diff changeset
   220
fun enum1' sep scan = scan ::: Scan.repeat (Scan.lift ($$$ sep) |-- scan);
2d36632bc5de unified Args.T with OuterLex.token;
wenzelm
parents: 27788
diff changeset
   221
fun enum' sep scan = enum1' sep scan || Scan.succeed [];
5826
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   222
6013
6da9ae6d40f5 and_list;
wenzelm
parents: 6003
diff changeset
   223
fun and_list1 scan = enum1 "and" scan;
6da9ae6d40f5 and_list;
wenzelm
parents: 6003
diff changeset
   224
fun and_list scan = enum "and" scan;
6da9ae6d40f5 and_list;
wenzelm
parents: 6003
diff changeset
   225
27815
2d36632bc5de unified Args.T with OuterLex.token;
wenzelm
parents: 27788
diff changeset
   226
fun and_list1' scan = enum1' "and" scan;
2d36632bc5de unified Args.T with OuterLex.token;
wenzelm
parents: 27788
diff changeset
   227
fun and_list' scan = enum' "and" scan;
2d36632bc5de unified Args.T with OuterLex.token;
wenzelm
parents: 27788
diff changeset
   228
2d36632bc5de unified Args.T with OuterLex.token;
wenzelm
parents: 27788
diff changeset
   229
fun list1 scan = enum1 "," scan;
2d36632bc5de unified Args.T with OuterLex.token;
wenzelm
parents: 27788
diff changeset
   230
fun list scan = enum "," scan;
2d36632bc5de unified Args.T with OuterLex.token;
wenzelm
parents: 27788
diff changeset
   231
5826
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   232
5960
2bebd0d0a961 comment parser;
wenzelm
parents: 5940
diff changeset
   233
(* names and text *)
5826
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   234
8146
3243f2261d4b 'name' etc. include 'number';
wenzelm
parents: 8077
diff changeset
   235
val name = group "name declaration" (short_ident || sym_ident || string || number);
30223
24d975352879 renamed Binding.name_pos to Binding.make, renamed Binding.base_name to Binding.name_of, renamed Binding.map_base to Binding.map_name, added mandatory flag to Binding.qualify;
wenzelm
parents: 29581
diff changeset
   236
val binding = position name >> Binding.make;
8146
3243f2261d4b 'name' etc. include 'number';
wenzelm
parents: 8077
diff changeset
   237
val xname = group "name reference" (short_ident || long_ident || sym_ident || string || number);
3243f2261d4b 'name' etc. include 'number';
wenzelm
parents: 8077
diff changeset
   238
val text = group "text" (short_ident || long_ident || sym_ident || string || number || verbatim);
21858
05f57309170c avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents: 21609
diff changeset
   239
val path = group "file name/path specification" name >> Path.explode;
6553
dc962d157a63 comment, interest;
wenzelm
parents: 6511
diff changeset
   240
40800
330eb65c9469 Parse.liberal_name for document antiquotations and attributes;
wenzelm
parents: 40793
diff changeset
   241
val liberal_name = keyword_ident_or_symbolic || xname;
330eb65c9469 Parse.liberal_name for document antiquotations and attributes;
wenzelm
parents: 40793
diff changeset
   242
18898
e3d2aa8ba0e1 added parname;
wenzelm
parents: 18669
diff changeset
   243
val parname = Scan.optional ($$$ "(" |-- name --| $$$ ")") "";
28965
1de908189869 cleaned up binding module and related code
haftmann
parents: 28941
diff changeset
   244
val parbinding = Scan.optional ($$$ "(" |-- binding --| $$$ ")") Binding.empty;
18898
e3d2aa8ba0e1 added parname;
wenzelm
parents: 18669
diff changeset
   245
6553
dc962d157a63 comment, interest;
wenzelm
parents: 6511
diff changeset
   246
6372
44b104595441 added simple_arity, spec_name, spec_opt_name;
wenzelm
parents: 6355
diff changeset
   247
(* sorts and arities *)
5826
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   248
27753
94b672153b49 sort/typ/term/prop: inner_syntax markup encodes original source position;
wenzelm
parents: 27737
diff changeset
   249
val sort = group "sort" (inner_syntax xname);
5826
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   250
22331
7df6bc8cf0b0 unified arity parser/arguments;
wenzelm
parents: 22119
diff changeset
   251
val arity = xname -- ($$$ "::" |-- !!!
7df6bc8cf0b0 unified arity parser/arguments;
wenzelm
parents: 22119
diff changeset
   252
  (Scan.optional ($$$ "(" |-- !!! (list1 sort --| $$$ ")")) [] -- sort)) >> triple2;
5826
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   253
25541
68de88c7e877 added parser for multi_arity
haftmann
parents: 24910
diff changeset
   254
val multi_arity = and_list1 xname -- ($$$ "::" |-- !!!
68de88c7e877 added parser for multi_arity
haftmann
parents: 24910
diff changeset
   255
  (Scan.optional ($$$ "(" |-- !!! (list1 sort --| $$$ ")")) [] -- sort)) >> triple2;
68de88c7e877 added parser for multi_arity
haftmann
parents: 24910
diff changeset
   256
5826
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   257
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   258
(* types *)
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   259
27753
94b672153b49 sort/typ/term/prop: inner_syntax markup encodes original source position;
wenzelm
parents: 27737
diff changeset
   260
val typ_group = group "type"
8146
3243f2261d4b 'name' etc. include 'number';
wenzelm
parents: 8077
diff changeset
   261
  (short_ident || long_ident || sym_ident || type_ident || type_var || string || number);
5826
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   262
27753
94b672153b49 sort/typ/term/prop: inner_syntax markup encodes original source position;
wenzelm
parents: 27737
diff changeset
   263
val typ = inner_syntax typ_group;
94b672153b49 sort/typ/term/prop: inner_syntax markup encodes original source position;
wenzelm
parents: 27737
diff changeset
   264
35838
c8bd075c4de8 support type arguments with sort constraints;
wenzelm
parents: 35351
diff changeset
   265
fun type_arguments arg =
c8bd075c4de8 support type arguments with sort constraints;
wenzelm
parents: 35351
diff changeset
   266
  arg >> single ||
c8bd075c4de8 support type arguments with sort constraints;
wenzelm
parents: 35351
diff changeset
   267
  $$$ "(" |-- !!! (list1 arg --| $$$ ")") ||
5826
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   268
  Scan.succeed [];
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   269
35838
c8bd075c4de8 support type arguments with sort constraints;
wenzelm
parents: 35351
diff changeset
   270
val type_args = type_arguments type_ident;
c8bd075c4de8 support type arguments with sort constraints;
wenzelm
parents: 35351
diff changeset
   271
val type_args_constrained = type_arguments (type_ident -- Scan.option ($$$ "::" |-- !!! sort));
c8bd075c4de8 support type arguments with sort constraints;
wenzelm
parents: 35351
diff changeset
   272
5826
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   273
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   274
(* mixfix annotations *)
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   275
18669
cd6d6baf0411 uniform handling of fixes;
wenzelm
parents: 18618
diff changeset
   276
val mfix = string --
cd6d6baf0411 uniform handling of fixes;
wenzelm
parents: 18618
diff changeset
   277
  !!! (Scan.optional ($$$ "[" |-- !!! (list nat --| $$$ "]")) [] --
42297
140f283266b7 discontinued Syntax.max_pri, which is not really a symbolic parameter;
wenzelm
parents: 42287
diff changeset
   278
    Scan.optional nat 1000) >> (Mixfix o triple2);
18669
cd6d6baf0411 uniform handling of fixes;
wenzelm
parents: 18618
diff changeset
   279
35130
0991c84e8dcf renamed InfixName to Infix etc.;
wenzelm
parents: 35129
diff changeset
   280
val infx = $$$ "infix" |-- !!! (string -- nat >> Infix);
0991c84e8dcf renamed InfixName to Infix etc.;
wenzelm
parents: 35129
diff changeset
   281
val infxl = $$$ "infixl" |-- !!! (string -- nat >> Infixl);
0991c84e8dcf renamed InfixName to Infix etc.;
wenzelm
parents: 35129
diff changeset
   282
val infxr = $$$ "infixr" |-- !!! (string -- nat >> Infixr);
5826
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   283
18669
cd6d6baf0411 uniform handling of fixes;
wenzelm
parents: 18618
diff changeset
   284
val binder = $$$ "binder" |--
cd6d6baf0411 uniform handling of fixes;
wenzelm
parents: 18618
diff changeset
   285
  !!! (string -- ($$$ "[" |-- nat --| $$$ "]" -- nat || nat >> (fn n => (n, n))))
cd6d6baf0411 uniform handling of fixes;
wenzelm
parents: 18618
diff changeset
   286
  >> (Binder o triple2);
cd6d6baf0411 uniform handling of fixes;
wenzelm
parents: 18618
diff changeset
   287
cd6d6baf0411 uniform handling of fixes;
wenzelm
parents: 18618
diff changeset
   288
fun annotation guard fix = $$$ "(" |-- guard (fix --| $$$ ")");
cd6d6baf0411 uniform handling of fixes;
wenzelm
parents: 18618
diff changeset
   289
fun opt_annotation guard fix = Scan.optional (annotation guard fix) NoSyn;
cd6d6baf0411 uniform handling of fixes;
wenzelm
parents: 18618
diff changeset
   290
cd6d6baf0411 uniform handling of fixes;
wenzelm
parents: 18618
diff changeset
   291
val mixfix = annotation !!! (mfix || binder || infxl || infxr || infx);
21609
5546a48bee93 added mixfix';
wenzelm
parents: 21440
diff changeset
   292
val mixfix' = annotation I (mfix || binder || infxl || infxr || infx);
18669
cd6d6baf0411 uniform handling of fixes;
wenzelm
parents: 18618
diff changeset
   293
val opt_mixfix = opt_annotation !!! (mfix || binder || infxl || infxr || infx);
cd6d6baf0411 uniform handling of fixes;
wenzelm
parents: 18618
diff changeset
   294
val opt_mixfix' = opt_annotation I (mfix || binder || infxl || infxr || infx);
5826
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   295
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   296
18669
cd6d6baf0411 uniform handling of fixes;
wenzelm
parents: 18618
diff changeset
   297
(* fixes *)
5826
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   298
21400
4788fc8e66ea added where_;
wenzelm
parents: 21371
diff changeset
   299
val where_ = $$$ "where";
4788fc8e66ea added where_;
wenzelm
parents: 21371
diff changeset
   300
42299
06e93f257d0e tuned signature;
wenzelm
parents: 42297
diff changeset
   301
val const_decl = name -- ($$$ "::" |-- !!! typ) -- opt_mixfix >> triple1;
30339
3fc32dd7a647 added const_binding;
wenzelm
parents: 30223
diff changeset
   302
val const_binding = binding -- ($$$ "::" |-- !!! typ) -- opt_mixfix >> triple1;
18669
cd6d6baf0411 uniform handling of fixes;
wenzelm
parents: 18618
diff changeset
   303
28081
d664b2c1dfe6 explicit type Name.binding for higher-specification elements;
wenzelm
parents: 28017
diff changeset
   304
val params = Scan.repeat1 binding -- Scan.option ($$$ "::" |-- !!! typ)
18669
cd6d6baf0411 uniform handling of fixes;
wenzelm
parents: 18618
diff changeset
   305
  >> (fn (xs, T) => map (rpair T) xs);
cd6d6baf0411 uniform handling of fixes;
wenzelm
parents: 18618
diff changeset
   306
19482
9f11af8f7ef9 tuned basic list operators (flat, maps, map_filter);
wenzelm
parents: 19284
diff changeset
   307
val simple_fixes = and_list1 params >> flat;
18669
cd6d6baf0411 uniform handling of fixes;
wenzelm
parents: 18618
diff changeset
   308
cd6d6baf0411 uniform handling of fixes;
wenzelm
parents: 18618
diff changeset
   309
val fixes =
28081
d664b2c1dfe6 explicit type Name.binding for higher-specification elements;
wenzelm
parents: 28017
diff changeset
   310
  and_list1 (binding -- Scan.option ($$$ "::" |-- typ) -- mixfix >> (single o triple1) ||
42287
d98eb048a2e4 discontinued special treatment of structure Mixfix;
wenzelm
parents: 40800
diff changeset
   311
    params >> map (fn (x, y) => (x, y, NoSyn))) >> flat;
5826
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   312
19845
b8985bf2ce8b added for_fixes;
wenzelm
parents: 19811
diff changeset
   313
val for_fixes = Scan.optional ($$$ "for" |-- !!! fixes) [];
21371
6717630f080b added for_simple_fixes, specification;
wenzelm
parents: 21314
diff changeset
   314
val for_simple_fixes = Scan.optional ($$$ "for" |-- !!! simple_fixes) [];
19845
b8985bf2ce8b added for_fixes;
wenzelm
parents: 19811
diff changeset
   315
5826
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   316
27877
af9f0adbab1f renamed P.ml_source to P.ML_source;
wenzelm
parents: 27872
diff changeset
   317
(* embedded source text *)
27872
631371a02b8c P.doc_source and P.ml_sorce for proper SymbolPos.text;
wenzelm
parents: 27815
diff changeset
   318
27877
af9f0adbab1f renamed P.ml_source to P.ML_source;
wenzelm
parents: 27872
diff changeset
   319
val ML_source = source_position (group "ML source" text);
27872
631371a02b8c P.doc_source and P.ml_sorce for proper SymbolPos.text;
wenzelm
parents: 27815
diff changeset
   320
val doc_source = source_position (group "document source" text);
631371a02b8c P.doc_source and P.ml_sorce for proper SymbolPos.text;
wenzelm
parents: 27815
diff changeset
   321
631371a02b8c P.doc_source and P.ml_sorce for proper SymbolPos.text;
wenzelm
parents: 27815
diff changeset
   322
5826
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   323
(* terms *)
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   324
40793
d21aedaa91e7 added Parse.literal_fact with proper inner_syntax markup (source position);
wenzelm
parents: 40296
diff changeset
   325
val tm = short_ident || long_ident || sym_ident || term_var || number || string;
5826
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   326
40793
d21aedaa91e7 added Parse.literal_fact with proper inner_syntax markup (source position);
wenzelm
parents: 40296
diff changeset
   327
val term_group = group "term" tm;
d21aedaa91e7 added Parse.literal_fact with proper inner_syntax markup (source position);
wenzelm
parents: 40296
diff changeset
   328
val prop_group = group "proposition" tm;
27753
94b672153b49 sort/typ/term/prop: inner_syntax markup encodes original source position;
wenzelm
parents: 27737
diff changeset
   329
94b672153b49 sort/typ/term/prop: inner_syntax markup encodes original source position;
wenzelm
parents: 27737
diff changeset
   330
val term = inner_syntax term_group;
94b672153b49 sort/typ/term/prop: inner_syntax markup encodes original source position;
wenzelm
parents: 27737
diff changeset
   331
val prop = inner_syntax prop_group;
5826
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   332
42300
0d1cbc1fe579 notation: proper markup for type constructor / constant;
wenzelm
parents: 42299
diff changeset
   333
val type_const = inner_syntax (group "type constructor" xname);
0d1cbc1fe579 notation: proper markup for type constructor / constant;
wenzelm
parents: 42299
diff changeset
   334
val const = inner_syntax (group "constant" xname);
0d1cbc1fe579 notation: proper markup for type constructor / constant;
wenzelm
parents: 42299
diff changeset
   335
40793
d21aedaa91e7 added Parse.literal_fact with proper inner_syntax markup (source position);
wenzelm
parents: 40296
diff changeset
   336
val literal_fact = inner_syntax (group "literal fact" alt_string);
d21aedaa91e7 added Parse.literal_fact with proper inner_syntax markup (source position);
wenzelm
parents: 40296
diff changeset
   337
5826
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   338
6949
a0b34115077f added termp;
wenzelm
parents: 6935
diff changeset
   339
(* patterns *)
6935
a3f3f4128cab propp: 'concl' patterns;
wenzelm
parents: 6860
diff changeset
   340
6949
a0b34115077f added termp;
wenzelm
parents: 6935
diff changeset
   341
val is_terms = Scan.repeat1 ($$$ "is" |-- term);
6935
a3f3f4128cab propp: 'concl' patterns;
wenzelm
parents: 6860
diff changeset
   342
val is_props = Scan.repeat1 ($$$ "is" |-- prop);
a3f3f4128cab propp: 'concl' patterns;
wenzelm
parents: 6860
diff changeset
   343
19585
70a1ce3b23ae removed 'concl is' patterns;
wenzelm
parents: 19482
diff changeset
   344
val propp = prop -- Scan.optional ($$$ "(" |-- !!! (is_props --| $$$ ")")) [];
6949
a0b34115077f added termp;
wenzelm
parents: 6935
diff changeset
   345
val termp = term -- Scan.optional ($$$ "(" |-- !!! (is_terms --| $$$ ")")) [];
6935
a3f3f4128cab propp: 'concl' patterns;
wenzelm
parents: 6860
diff changeset
   346
a3f3f4128cab propp: 'concl' patterns;
wenzelm
parents: 6860
diff changeset
   347
22119
6f1c82c0243c moved parts to spec_parse.ML;
wenzelm
parents: 21858
diff changeset
   348
(* targets *)
19811
46abcbb2da9d added locale_insts;
wenzelm
parents: 19585
diff changeset
   349
22119
6f1c82c0243c moved parts to spec_parse.ML;
wenzelm
parents: 21858
diff changeset
   350
val target = ($$$ "(" -- $$$ "in") |-- !!! (xname --| $$$ ")");
6f1c82c0243c moved parts to spec_parse.ML;
wenzelm
parents: 21858
diff changeset
   351
val opt_target = Scan.option target;
12272
9bc50336dab6 improved locale expression syntax;
wenzelm
parents: 12268
diff changeset
   352
9bc50336dab6 improved locale expression syntax;
wenzelm
parents: 12268
diff changeset
   353
end;
30511
5c628a39b7cb pervasive types 'a parser and 'a context_parser;
wenzelm
parents: 30339
diff changeset
   354
36949
080e85d46108 renamed structure OuterKeyword to Keyword and OuterParse to Parse, keeping the old names as legacy aliases for some time;
wenzelm
parents: 35838
diff changeset
   355
type 'a parser = 'a Parse.parser;
080e85d46108 renamed structure OuterKeyword to Keyword and OuterParse to Parse, keeping the old names as legacy aliases for some time;
wenzelm
parents: 35838
diff changeset
   356
type 'a context_parser = 'a Parse.context_parser;
30511
5c628a39b7cb pervasive types 'a parser and 'a context_parser;
wenzelm
parents: 30339
diff changeset
   357