src/Pure/Isar/parse.ML
author wenzelm
Fri, 03 Apr 2015 20:04:16 +0200
changeset 59918 d01e6d159c33
parent 59917 9830c944670f
child 59924 801b979ec0c2
permissions -rw-r--r--
unused;
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
44357
5f5649ac8235 tuned Parse.group: delayed failure message;
wenzelm
parents: 43947
diff changeset
     9
  val group: (unit -> string) -> (Token.T list -> 'a) -> Token.T list -> 'a
36959
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 36955
diff changeset
    10
  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
    11
  val !!!! : (Token.T list -> 'a) -> Token.T list -> 'a
12047
e151e66da2d6 added locale_element;
wenzelm
parents: 11792
diff changeset
    12
  val triple1: ('a * 'b) * 'c -> 'a * 'b * 'c
e151e66da2d6 added locale_element;
wenzelm
parents: 11792
diff changeset
    13
  val triple2: 'a * ('b * 'c) -> 'a * 'b * 'c
e151e66da2d6 added locale_element;
wenzelm
parents: 11792
diff changeset
    14
  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
    15
  val not_eof: Token.T parser
56201
dd2df97b379b tuned signature;
wenzelm
parents: 56063
diff changeset
    16
  val token: 'a parser -> Token.T parser
59029
c907cbe36713 more careful ML source positions, for improved PIDE markup;
wenzelm
parents: 58908
diff changeset
    17
  val range: 'a parser -> ('a * Position.range) parser
42326
e2d22eb4aeb9 some position reports for 'translations';
wenzelm
parents: 42300
diff changeset
    18
  val position: 'a parser -> ('a * Position.T) parser
59809
87641097d0f3 tuned signature;
wenzelm
parents: 59784
diff changeset
    19
  val input: 'a parser -> Input.source parser
42326
e2d22eb4aeb9 some position reports for 'translations';
wenzelm
parents: 42300
diff changeset
    20
  val inner_syntax: 'a parser -> string parser
58908
58bedbc18915 tuned signature;
wenzelm
parents: 58861
diff changeset
    21
  val command_: string parser
29310
1a633304fa5e added type 'a parser, simplified signature;
wenzelm
parents: 28965
diff changeset
    22
  val keyword: string parser
1a633304fa5e added type 'a parser, simplified signature;
wenzelm
parents: 28965
diff changeset
    23
  val short_ident: string parser
1a633304fa5e added type 'a parser, simplified signature;
wenzelm
parents: 28965
diff changeset
    24
  val long_ident: string parser
1a633304fa5e added type 'a parser, simplified signature;
wenzelm
parents: 28965
diff changeset
    25
  val sym_ident: string parser
1a633304fa5e added type 'a parser, simplified signature;
wenzelm
parents: 28965
diff changeset
    26
  val minus: string parser
1a633304fa5e added type 'a parser, simplified signature;
wenzelm
parents: 28965
diff changeset
    27
  val term_var: string parser
1a633304fa5e added type 'a parser, simplified signature;
wenzelm
parents: 28965
diff changeset
    28
  val type_ident: string parser
1a633304fa5e added type 'a parser, simplified signature;
wenzelm
parents: 28965
diff changeset
    29
  val type_var: string parser
1a633304fa5e added type 'a parser, simplified signature;
wenzelm
parents: 28965
diff changeset
    30
  val number: string parser
40290
47f572aff50a support for floating-point tokens in outer syntax (coinciding with inner syntax version);
wenzelm
parents: 36959
diff changeset
    31
  val float_number: string parser
29310
1a633304fa5e added type 'a parser, simplified signature;
wenzelm
parents: 28965
diff changeset
    32
  val string: string parser
1a633304fa5e added type 'a parser, simplified signature;
wenzelm
parents: 28965
diff changeset
    33
  val alt_string: string parser
1a633304fa5e added type 'a parser, simplified signature;
wenzelm
parents: 28965
diff changeset
    34
  val verbatim: string parser
55033
8e8243975860 support for nested text cartouches;
wenzelm
parents: 51988
diff changeset
    35
  val cartouche: string parser
29310
1a633304fa5e added type 'a parser, simplified signature;
wenzelm
parents: 28965
diff changeset
    36
  val eof: string parser
58908
58bedbc18915 tuned signature;
wenzelm
parents: 58861
diff changeset
    37
  val command: string -> string parser
29310
1a633304fa5e added type 'a parser, simplified signature;
wenzelm
parents: 28965
diff changeset
    38
  val keyword_with: (string -> bool) -> string parser
56202
0a11d17eeeff more markup for improper elements;
wenzelm
parents: 56201
diff changeset
    39
  val keyword_markup: bool * Markup.T -> string -> string parser
0a11d17eeeff more markup for improper elements;
wenzelm
parents: 56201
diff changeset
    40
  val keyword_improper: string -> string parser
29310
1a633304fa5e added type 'a parser, simplified signature;
wenzelm
parents: 28965
diff changeset
    41
  val $$$ : string -> string parser
1a633304fa5e added type 'a parser, simplified signature;
wenzelm
parents: 28965
diff changeset
    42
  val reserved: string -> string parser
1a633304fa5e added type 'a parser, simplified signature;
wenzelm
parents: 28965
diff changeset
    43
  val underscore: string parser
1a633304fa5e added type 'a parser, simplified signature;
wenzelm
parents: 28965
diff changeset
    44
  val maybe: 'a parser -> 'a option parser
1a633304fa5e added type 'a parser, simplified signature;
wenzelm
parents: 28965
diff changeset
    45
  val tag_name: string parser
1a633304fa5e added type 'a parser, simplified signature;
wenzelm
parents: 28965
diff changeset
    46
  val tags: string list parser
1a633304fa5e added type 'a parser, simplified signature;
wenzelm
parents: 28965
diff changeset
    47
  val opt_keyword: string -> bool parser
59917
9830c944670f more uniform "verbose" option to print name space;
wenzelm
parents: 59809
diff changeset
    48
  val opt_bang: bool parser
29310
1a633304fa5e added type 'a parser, simplified signature;
wenzelm
parents: 28965
diff changeset
    49
  val begin: string parser
1a633304fa5e added type 'a parser, simplified signature;
wenzelm
parents: 28965
diff changeset
    50
  val opt_begin: bool parser
1a633304fa5e added type 'a parser, simplified signature;
wenzelm
parents: 28965
diff changeset
    51
  val nat: int parser
1a633304fa5e added type 'a parser, simplified signature;
wenzelm
parents: 28965
diff changeset
    52
  val int: int parser
40290
47f572aff50a support for floating-point tokens in outer syntax (coinciding with inner syntax version);
wenzelm
parents: 36959
diff changeset
    53
  val real: real parser
55764
wenzelm
parents: 55708
diff changeset
    54
  val enum_positions: string -> 'a parser -> ('a list * Position.T list) parser
wenzelm
parents: 55708
diff changeset
    55
  val enum1_positions: string -> 'a parser -> ('a list * Position.T list) parser
29310
1a633304fa5e added type 'a parser, simplified signature;
wenzelm
parents: 28965
diff changeset
    56
  val enum: string -> 'a parser -> 'a list parser
1a633304fa5e added type 'a parser, simplified signature;
wenzelm
parents: 28965
diff changeset
    57
  val enum1: string -> 'a parser -> 'a list parser
1a633304fa5e added type 'a parser, simplified signature;
wenzelm
parents: 28965
diff changeset
    58
  val and_list: 'a parser -> 'a list parser
1a633304fa5e added type 'a parser, simplified signature;
wenzelm
parents: 28965
diff changeset
    59
  val and_list1: 'a parser -> 'a list parser
30511
5c628a39b7cb pervasive types 'a parser and 'a context_parser;
wenzelm
parents: 30339
diff changeset
    60
  val enum': string -> 'a context_parser -> 'a list context_parser
5c628a39b7cb pervasive types 'a parser and 'a context_parser;
wenzelm
parents: 30339
diff changeset
    61
  val enum1': string -> 'a context_parser -> 'a list context_parser
5c628a39b7cb pervasive types 'a parser and 'a context_parser;
wenzelm
parents: 30339
diff changeset
    62
  val and_list': 'a context_parser -> 'a list context_parser
5c628a39b7cb pervasive types 'a parser and 'a context_parser;
wenzelm
parents: 30339
diff changeset
    63
  val and_list1': 'a context_parser -> 'a list context_parser
29310
1a633304fa5e added type 'a parser, simplified signature;
wenzelm
parents: 28965
diff changeset
    64
  val list: 'a parser -> 'a list parser
1a633304fa5e added type 'a parser, simplified signature;
wenzelm
parents: 28965
diff changeset
    65
  val list1: 'a parser -> 'a list parser
43775
b361c7d184e7 added Parse.properties (again) -- allow empty list like Parse_Value.properties but unlike Parse.properties of ef86de9c98aa;
wenzelm
parents: 42657
diff changeset
    66
  val properties: Properties.T parser
29310
1a633304fa5e added type 'a parser, simplified signature;
wenzelm
parents: 28965
diff changeset
    67
  val name: bstring parser
29581
b3b33e0298eb binding is alias for Binding.T
haftmann
parents: 29310
diff changeset
    68
  val binding: binding parser
29310
1a633304fa5e added type 'a parser, simplified signature;
wenzelm
parents: 28965
diff changeset
    69
  val xname: xstring parser
1a633304fa5e added type 'a parser, simplified signature;
wenzelm
parents: 28965
diff changeset
    70
  val text: string parser
48881
46e053eda5dd clarified Parse.path vs. Parse.explode -- prefer errors in proper transaction context;
wenzelm
parents: 46922
diff changeset
    71
  val path: string parser
59693
d96cb03caf9e tunes signature -- more uniform ML vs. Scala;
wenzelm
parents: 59081
diff changeset
    72
  val theory_name: bstring parser
d96cb03caf9e tunes signature -- more uniform ML vs. Scala;
wenzelm
parents: 59081
diff changeset
    73
  val theory_xname: xstring parser
40800
330eb65c9469 Parse.liberal_name for document antiquotations and attributes;
wenzelm
parents: 40793
diff changeset
    74
  val liberal_name: xstring parser
29310
1a633304fa5e added type 'a parser, simplified signature;
wenzelm
parents: 28965
diff changeset
    75
  val parname: string parser
29581
b3b33e0298eb binding is alias for Binding.T
haftmann
parents: 29310
diff changeset
    76
  val parbinding: binding parser
46922
3717f3878714 source positions for locale and class expressions;
wenzelm
parents: 45596
diff changeset
    77
  val class: string parser
29310
1a633304fa5e added type 'a parser, simplified signature;
wenzelm
parents: 28965
diff changeset
    78
  val sort: string parser
46922
3717f3878714 source positions for locale and class expressions;
wenzelm
parents: 45596
diff changeset
    79
  val type_const: string parser
29310
1a633304fa5e added type 'a parser, simplified signature;
wenzelm
parents: 28965
diff changeset
    80
  val arity: (string * string list * string) parser
1a633304fa5e added type 'a parser, simplified signature;
wenzelm
parents: 28965
diff changeset
    81
  val multi_arity: (string list * string list * string) parser
1a633304fa5e added type 'a parser, simplified signature;
wenzelm
parents: 28965
diff changeset
    82
  val type_args: string list parser
35838
c8bd075c4de8 support type arguments with sort constraints;
wenzelm
parents: 35351
diff changeset
    83
  val type_args_constrained: (string * string option) list parser
29310
1a633304fa5e added type 'a parser, simplified signature;
wenzelm
parents: 28965
diff changeset
    84
  val typ_group: string parser
1a633304fa5e added type 'a parser, simplified signature;
wenzelm
parents: 28965
diff changeset
    85
  val typ: string parser
1a633304fa5e added type 'a parser, simplified signature;
wenzelm
parents: 28965
diff changeset
    86
  val mixfix: mixfix parser
1a633304fa5e added type 'a parser, simplified signature;
wenzelm
parents: 28965
diff changeset
    87
  val mixfix': mixfix parser
1a633304fa5e added type 'a parser, simplified signature;
wenzelm
parents: 28965
diff changeset
    88
  val opt_mixfix: mixfix parser
1a633304fa5e added type 'a parser, simplified signature;
wenzelm
parents: 28965
diff changeset
    89
  val opt_mixfix': mixfix parser
1a633304fa5e added type 'a parser, simplified signature;
wenzelm
parents: 28965
diff changeset
    90
  val where_: string parser
42299
06e93f257d0e tuned signature;
wenzelm
parents: 42297
diff changeset
    91
  val const_decl: (string * string * mixfix) parser
30339
3fc32dd7a647 added const_binding;
wenzelm
parents: 30223
diff changeset
    92
  val const_binding: (binding * string * mixfix) parser
29581
b3b33e0298eb binding is alias for Binding.T
haftmann
parents: 29310
diff changeset
    93
  val params: (binding * string option) list parser
b3b33e0298eb binding is alias for Binding.T
haftmann
parents: 29310
diff changeset
    94
  val fixes: (binding * string option * mixfix) list parser
b3b33e0298eb binding is alias for Binding.T
haftmann
parents: 29310
diff changeset
    95
  val for_fixes: (binding * string option * mixfix) list parser
59064
a8bcb5a446c8 more abstract type Input.source;
wenzelm
parents: 59029
diff changeset
    96
  val ML_source: Input.source parser
a8bcb5a446c8 more abstract type Input.source;
wenzelm
parents: 59029
diff changeset
    97
  val document_source: Input.source parser
29310
1a633304fa5e added type 'a parser, simplified signature;
wenzelm
parents: 28965
diff changeset
    98
  val term_group: string parser
1a633304fa5e added type 'a parser, simplified signature;
wenzelm
parents: 28965
diff changeset
    99
  val prop_group: string parser
1a633304fa5e added type 'a parser, simplified signature;
wenzelm
parents: 28965
diff changeset
   100
  val term: string parser
1a633304fa5e added type 'a parser, simplified signature;
wenzelm
parents: 28965
diff changeset
   101
  val prop: string parser
42300
0d1cbc1fe579 notation: proper markup for type constructor / constant;
wenzelm
parents: 42299
diff changeset
   102
  val const: string parser
40793
d21aedaa91e7 added Parse.literal_fact with proper inner_syntax markup (source position);
wenzelm
parents: 40296
diff changeset
   103
  val literal_fact: string parser
29310
1a633304fa5e added type 'a parser, simplified signature;
wenzelm
parents: 28965
diff changeset
   104
  val propp: (string * string list) parser
1a633304fa5e added type 'a parser, simplified signature;
wenzelm
parents: 28965
diff changeset
   105
  val termp: (string * string list) parser
45488
6d71d9e52369 pass positions for named targets, for formal links in the document model;
wenzelm
parents: 45331
diff changeset
   106
  val target: (xstring * Position.T) parser
6d71d9e52369 pass positions for named targets, for formal links in the document model;
wenzelm
parents: 45331
diff changeset
   107
  val opt_target: (xstring * Position.T) option parser
56201
dd2df97b379b tuned signature;
wenzelm
parents: 56063
diff changeset
   108
  val args: Token.T list parser
dd2df97b379b tuned signature;
wenzelm
parents: 56063
diff changeset
   109
  val args1: (string -> bool) -> Token.T list parser
58028
e4250d370657 tuned signature -- define some elementary operations earlier;
wenzelm
parents: 58011
diff changeset
   110
  val attribs: Token.src list parser
e4250d370657 tuned signature -- define some elementary operations earlier;
wenzelm
parents: 58011
diff changeset
   111
  val opt_attribs: Token.src list parser
e4250d370657 tuned signature -- define some elementary operations earlier;
wenzelm
parents: 58011
diff changeset
   112
  val thm_sel: Facts.interval list parser
e4250d370657 tuned signature -- define some elementary operations earlier;
wenzelm
parents: 58011
diff changeset
   113
  val xthm: (Facts.ref * Token.src list) parser
e4250d370657 tuned signature -- define some elementary operations earlier;
wenzelm
parents: 58011
diff changeset
   114
  val xthms1: (Facts.ref * Token.src list) list parser
5826
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   115
end;
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   116
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
   117
structure Parse: PARSE =
5826
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   118
struct
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   119
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   120
(** error handling **)
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   121
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   122
(* group atomic parsers (no cuts!) *)
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   123
44357
5f5649ac8235 tuned Parse.group: delayed failure message;
wenzelm
parents: 43947
diff changeset
   124
fun group s scan = scan || Scan.fail_with
48911
5debc3e4fa81 tuned messages: end-of-input rarely means physical end-of-file from the past;
wenzelm
parents: 48881
diff changeset
   125
  (fn [] => (fn () => s () ^ " expected,\nbut end-of-input was found")
42519
wenzelm
parents: 42326
diff changeset
   126
    | tok :: _ =>
43947
9b00f09f7721 defer evaluation of Scan.message, for improved performance in the frequent situation where failure is handled later (e.g. via ||);
wenzelm
parents: 43775
diff changeset
   127
        (fn () =>
9b00f09f7721 defer evaluation of Scan.message, for improved performance in the frequent situation where failure is handled later (e.g. via ||);
wenzelm
parents: 43775
diff changeset
   128
          (case Token.text_of tok of
9b00f09f7721 defer evaluation of Scan.message, for improved performance in the frequent situation where failure is handled later (e.g. via ||);
wenzelm
parents: 43775
diff changeset
   129
            (txt, "") =>
55708
f4b114070675 tuned signature;
wenzelm
parents: 55111
diff changeset
   130
              s () ^ " expected,\nbut " ^ txt ^ Position.here (Token.pos_of tok) ^
f4b114070675 tuned signature;
wenzelm
parents: 55111
diff changeset
   131
              " was found"
43947
9b00f09f7721 defer evaluation of Scan.message, for improved performance in the frequent situation where failure is handled later (e.g. via ||);
wenzelm
parents: 43775
diff changeset
   132
          | (txt1, txt2) =>
55708
f4b114070675 tuned signature;
wenzelm
parents: 55111
diff changeset
   133
              s () ^ " expected,\nbut " ^ txt1 ^ Position.here (Token.pos_of tok) ^
f4b114070675 tuned signature;
wenzelm
parents: 55111
diff changeset
   134
              " was found:\n" ^ txt2)));
5826
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   135
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   136
5877
ee214dec5657 removed args, args1, thm_xname;
wenzelm
parents: 5826
diff changeset
   137
(* cut *)
5826
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   138
8581
5c7ed2af8bfb !!!! = cut "Corrupted outer syntax in presentation";
wenzelm
parents: 8350
diff changeset
   139
fun cut kind scan =
5826
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   140
  let
48911
5debc3e4fa81 tuned messages: end-of-input rarely means physical end-of-file from the past;
wenzelm
parents: 48881
diff changeset
   141
    fun get_pos [] = " (end-of-input)"
55708
f4b114070675 tuned signature;
wenzelm
parents: 55111
diff changeset
   142
      | get_pos (tok :: _) = Position.here (Token.pos_of tok);
5826
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   143
43947
9b00f09f7721 defer evaluation of Scan.message, for improved performance in the frequent situation where failure is handled later (e.g. via ||);
wenzelm
parents: 43775
diff changeset
   144
    fun err (toks, NONE) = (fn () => kind ^ get_pos toks)
25625
35e2aa8b8b03 nested commands: avoid nested errors;
wenzelm
parents: 25541
diff changeset
   145
      | err (toks, SOME msg) =
43947
9b00f09f7721 defer evaluation of Scan.message, for improved performance in the frequent situation where failure is handled later (e.g. via ||);
wenzelm
parents: 43775
diff changeset
   146
          (fn () =>
9b00f09f7721 defer evaluation of Scan.message, for improved performance in the frequent situation where failure is handled later (e.g. via ||);
wenzelm
parents: 43775
diff changeset
   147
            let val s = msg () in
9b00f09f7721 defer evaluation of Scan.message, for improved performance in the frequent situation where failure is handled later (e.g. via ||);
wenzelm
parents: 43775
diff changeset
   148
              if String.isPrefix kind s then s
9b00f09f7721 defer evaluation of Scan.message, for improved performance in the frequent situation where failure is handled later (e.g. via ||);
wenzelm
parents: 43775
diff changeset
   149
              else kind ^ get_pos toks ^ ": " ^ s
9b00f09f7721 defer evaluation of Scan.message, for improved performance in the frequent situation where failure is handled later (e.g. via ||);
wenzelm
parents: 43775
diff changeset
   150
            end);
5826
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   151
  in Scan.!! err scan end;
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   152
8586
e451c4865548 made SML/NJ happy;
wenzelm
parents: 8581
diff changeset
   153
fun !!! scan = cut "Outer syntax error" scan;
e451c4865548 made SML/NJ happy;
wenzelm
parents: 8581
diff changeset
   154
fun !!!! scan = cut "Corrupted outer syntax in presentation" scan;
8581
5c7ed2af8bfb !!!! = cut "Corrupted outer syntax in presentation";
wenzelm
parents: 8350
diff changeset
   155
5826
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   156
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   157
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   158
(** basic parsers **)
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   159
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   160
(* utils *)
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   161
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   162
fun triple1 ((x, y), z) = (x, y, z);
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   163
fun triple2 (x, (y, z)) = (x, y, z);
6430
69400c97d3bf triple_swap;
wenzelm
parents: 6398
diff changeset
   164
fun triple_swap ((x, y), z) = ((x, z), y);
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
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   167
(* tokens *)
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   168
27815
2d36632bc5de unified Args.T with OuterLex.token;
wenzelm
parents: 27788
diff changeset
   169
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
   170
  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
   171
2d36632bc5de unified Args.T with OuterLex.token;
wenzelm
parents: 27788
diff changeset
   172
36959
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 not_eof = RESET_VALUE (Scan.one Token.not_eof);
15703
727ef1b8b3ee *** empty log message ***
wenzelm
parents: 15570
diff changeset
   174
56201
dd2df97b379b tuned signature;
wenzelm
parents: 56063
diff changeset
   175
fun token atom = Scan.ahead not_eof --| atom;
dd2df97b379b tuned signature;
wenzelm
parents: 56063
diff changeset
   176
59029
c907cbe36713 more careful ML source positions, for improved PIDE markup;
wenzelm
parents: 58908
diff changeset
   177
fun range scan = (Scan.ahead not_eof >> (Token.range_of o single)) -- scan >> Library.swap;
55708
f4b114070675 tuned signature;
wenzelm
parents: 55111
diff changeset
   178
fun position scan = (Scan.ahead not_eof >> Token.pos_of) -- scan >> Library.swap;
59809
87641097d0f3 tuned signature;
wenzelm
parents: 59784
diff changeset
   179
fun input atom = Scan.ahead atom |-- not_eof >> Token.input_of;
55111
5792f5106c40 tuned signature;
wenzelm
parents: 55033
diff changeset
   180
fun inner_syntax atom = Scan.ahead atom |-- not_eof >> Token.inner_syntax_of;
5826
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   181
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   182
fun kind k =
44357
5f5649ac8235 tuned Parse.group: delayed failure message;
wenzelm
parents: 43947
diff changeset
   183
  group (fn () => Token.str_of_kind k)
5f5649ac8235 tuned Parse.group: delayed failure message;
wenzelm
parents: 43947
diff changeset
   184
    (RESET_VALUE (Scan.one (Token.is_kind k) >> Token.content_of));
5826
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   185
58908
58bedbc18915 tuned signature;
wenzelm
parents: 58861
diff changeset
   186
val command_ = kind Token.Command;
36959
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 36955
diff changeset
   187
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
   188
val short_ident = kind Token.Ident;
59081
2ceb05ee0331 clarified token kind;
wenzelm
parents: 59064
diff changeset
   189
val long_ident = kind Token.Long_Ident;
2ceb05ee0331 clarified token kind;
wenzelm
parents: 59064
diff changeset
   190
val sym_ident = kind Token.Sym_Ident;
36959
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 36955
diff changeset
   191
val term_var = kind Token.Var;
59081
2ceb05ee0331 clarified token kind;
wenzelm
parents: 59064
diff changeset
   192
val type_ident = kind Token.Type_Ident;
2ceb05ee0331 clarified token kind;
wenzelm
parents: 59064
diff changeset
   193
val type_var = kind Token.Type_Var;
36959
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 36955
diff changeset
   194
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
   195
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
   196
val string = kind Token.String;
59081
2ceb05ee0331 clarified token kind;
wenzelm
parents: 59064
diff changeset
   197
val alt_string = kind Token.Alt_String;
36959
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 36955
diff changeset
   198
val verbatim = kind Token.Verbatim;
55033
8e8243975860 support for nested text cartouches;
wenzelm
parents: 51988
diff changeset
   199
val cartouche = kind Token.Cartouche;
36959
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 36955
diff changeset
   200
val eof = kind Token.EOF;
5826
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   201
58908
58bedbc18915 tuned signature;
wenzelm
parents: 58861
diff changeset
   202
fun command x =
48927
ef462b5558eb theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents: 48911
diff changeset
   203
  group (fn () => Token.str_of_kind Token.Command ^ " " ^ quote x)
ef462b5558eb theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents: 48911
diff changeset
   204
    (RESET_VALUE (Scan.one (fn tok => Token.is_command tok andalso Token.content_of tok = x)))
ef462b5558eb theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents: 48911
diff changeset
   205
  >> Token.content_of;
ef462b5558eb theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents: 48911
diff changeset
   206
56202
0a11d17eeeff more markup for improper elements;
wenzelm
parents: 56201
diff changeset
   207
fun keyword_with pred = RESET_VALUE (Scan.one (Token.keyword_with pred) >> Token.content_of);
0a11d17eeeff more markup for improper elements;
wenzelm
parents: 56201
diff changeset
   208
0a11d17eeeff more markup for improper elements;
wenzelm
parents: 56201
diff changeset
   209
fun keyword_markup markup x =
44357
5f5649ac8235 tuned Parse.group: delayed failure message;
wenzelm
parents: 43947
diff changeset
   210
  group (fn () => Token.str_of_kind Token.Keyword ^ " " ^ quote x)
56063
38f13d055107 more explicit markup for Token.Literal;
wenzelm
parents: 55828
diff changeset
   211
    (Scan.ahead not_eof -- keyword_with (fn y => x = y))
56202
0a11d17eeeff more markup for improper elements;
wenzelm
parents: 56201
diff changeset
   212
  >> (fn (tok, x) => (Token.assign (SOME (Token.Literal markup)) tok; x));
0a11d17eeeff more markup for improper elements;
wenzelm
parents: 56201
diff changeset
   213
0a11d17eeeff more markup for improper elements;
wenzelm
parents: 56201
diff changeset
   214
val keyword_improper = keyword_markup (true, Markup.improper);
0a11d17eeeff more markup for improper elements;
wenzelm
parents: 56201
diff changeset
   215
val $$$ = keyword_markup (false, Markup.quasi_keyword);
9131
cd17637c917f added semicolon;
wenzelm
parents: 9037
diff changeset
   216
16030
bbfb2f1378b3 added reserved;
wenzelm
parents: 15979
diff changeset
   217
fun reserved x =
44357
5f5649ac8235 tuned Parse.group: delayed failure message;
wenzelm
parents: 43947
diff changeset
   218
  group (fn () => "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
   219
    (RESET_VALUE (Scan.one (Token.ident_with (fn y => x = y)) >> Token.content_of));
16030
bbfb2f1378b3 added reserved;
wenzelm
parents: 15979
diff changeset
   220
15703
727ef1b8b3ee *** empty log message ***
wenzelm
parents: 15570
diff changeset
   221
val minus = sym_ident :-- (fn "-" => Scan.succeed () | _ => Scan.fail) >> #1;
11792
311eee3d63b6 parser for underscore (actually a symbolic identifier!);
wenzelm
parents: 11651
diff changeset
   222
val underscore = sym_ident :-- (fn "_" => Scan.succeed () | _ => Scan.fail) >> #1;
15703
727ef1b8b3ee *** empty log message ***
wenzelm
parents: 15570
diff changeset
   223
fun maybe scan = underscore >> K NONE || scan >> SOME;
11792
311eee3d63b6 parser for underscore (actually a symbolic identifier!);
wenzelm
parents: 11651
diff changeset
   224
14835
695ee8ad0bb6 Library.read_int; Output.output;
wenzelm
parents: 14646
diff changeset
   225
val nat = number >> (#1 o Library.read_int o Symbol.explode);
27815
2d36632bc5de unified Args.T with OuterLex.token;
wenzelm
parents: 27788
diff changeset
   226
val int = Scan.optional (minus >> K ~1) 1 -- nat >> op *;
51988
a9725750c53a more uniform Markup.parse_real;
wenzelm
parents: 51654
diff changeset
   227
val real = float_number >> Markup.parse_real || int >> Real.fromInt;
5826
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   228
44357
5f5649ac8235 tuned Parse.group: delayed failure message;
wenzelm
parents: 43947
diff changeset
   229
val tag_name = group (fn () => "tag name") (short_ident || string);
17070
3b29a01417f8 added tags parser;
wenzelm
parents: 16736
diff changeset
   230
val tags = Scan.repeat ($$$ "%" |-- !!! tag_name);
3b29a01417f8 added tags parser;
wenzelm
parents: 16736
diff changeset
   231
14646
f5f2340398f9 added opt_keyword, mixfix';
wenzelm
parents: 14605
diff changeset
   232
fun opt_keyword s = Scan.optional ($$$ "(" |-- !!! (($$$ s >> K true) --| $$$ ")")) false;
59917
9830c944670f more uniform "verbose" option to print name space;
wenzelm
parents: 59809
diff changeset
   233
val opt_bang = Scan.optional ($$$ "!" >> K true) false;
14646
f5f2340398f9 added opt_keyword, mixfix';
wenzelm
parents: 14605
diff changeset
   234
20983
d4500b9b220e added begin parser;
wenzelm
parents: 20961
diff changeset
   235
val begin = $$$ "begin";
d4500b9b220e added begin parser;
wenzelm
parents: 20961
diff changeset
   236
val opt_begin = Scan.optional (begin >> K true) false;
20961
555d27f2c210 added opt_begin;
wenzelm
parents: 20273
diff changeset
   237
5826
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   238
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   239
(* enumerations *)
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   240
55764
wenzelm
parents: 55708
diff changeset
   241
fun enum1_positions sep scan =
wenzelm
parents: 55708
diff changeset
   242
  scan -- Scan.repeat (position ($$$ sep) -- !!! scan) >>
wenzelm
parents: 55708
diff changeset
   243
    (fn (x, ys) => (x :: map #2 ys, map (#2 o #1) ys));
wenzelm
parents: 55708
diff changeset
   244
fun enum_positions sep scan =
wenzelm
parents: 55708
diff changeset
   245
  enum1_positions sep scan || Scan.succeed ([], []);
wenzelm
parents: 55708
diff changeset
   246
25999
f8bcd311d501 added ::: / @@@ scanner combinators;
wenzelm
parents: 25795
diff changeset
   247
fun enum1 sep scan = scan ::: Scan.repeat ($$$ sep |-- !!! scan);
5826
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   248
fun enum sep scan = enum1 sep scan || Scan.succeed [];
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   249
27815
2d36632bc5de unified Args.T with OuterLex.token;
wenzelm
parents: 27788
diff changeset
   250
fun enum1' sep scan = scan ::: Scan.repeat (Scan.lift ($$$ sep) |-- scan);
2d36632bc5de unified Args.T with OuterLex.token;
wenzelm
parents: 27788
diff changeset
   251
fun enum' sep scan = enum1' sep scan || Scan.succeed [];
5826
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   252
6013
6da9ae6d40f5 and_list;
wenzelm
parents: 6003
diff changeset
   253
fun and_list1 scan = enum1 "and" scan;
6da9ae6d40f5 and_list;
wenzelm
parents: 6003
diff changeset
   254
fun and_list scan = enum "and" scan;
6da9ae6d40f5 and_list;
wenzelm
parents: 6003
diff changeset
   255
27815
2d36632bc5de unified Args.T with OuterLex.token;
wenzelm
parents: 27788
diff changeset
   256
fun and_list1' scan = enum1' "and" scan;
2d36632bc5de unified Args.T with OuterLex.token;
wenzelm
parents: 27788
diff changeset
   257
fun and_list' scan = enum' "and" scan;
2d36632bc5de unified Args.T with OuterLex.token;
wenzelm
parents: 27788
diff changeset
   258
2d36632bc5de unified Args.T with OuterLex.token;
wenzelm
parents: 27788
diff changeset
   259
fun list1 scan = enum1 "," scan;
2d36632bc5de unified Args.T with OuterLex.token;
wenzelm
parents: 27788
diff changeset
   260
fun list scan = enum "," scan;
2d36632bc5de unified Args.T with OuterLex.token;
wenzelm
parents: 27788
diff changeset
   261
43775
b361c7d184e7 added Parse.properties (again) -- allow empty list like Parse_Value.properties but unlike Parse.properties of ef86de9c98aa;
wenzelm
parents: 42657
diff changeset
   262
val properties = $$$ "(" |-- !!! (list (string -- ($$$ "=" |-- string)) --| $$$ ")");
b361c7d184e7 added Parse.properties (again) -- allow empty list like Parse_Value.properties but unlike Parse.properties of ef86de9c98aa;
wenzelm
parents: 42657
diff changeset
   263
5826
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   264
5960
2bebd0d0a961 comment parser;
wenzelm
parents: 5940
diff changeset
   265
(* names and text *)
5826
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   266
44357
5f5649ac8235 tuned Parse.group: delayed failure message;
wenzelm
parents: 43947
diff changeset
   267
val name = group (fn () => "name declaration") (short_ident || sym_ident || string || number);
5f5649ac8235 tuned Parse.group: delayed failure message;
wenzelm
parents: 43947
diff changeset
   268
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
   269
val binding = position name >> Binding.make;
44357
5f5649ac8235 tuned Parse.group: delayed failure message;
wenzelm
parents: 43947
diff changeset
   270
5f5649ac8235 tuned Parse.group: delayed failure message;
wenzelm
parents: 43947
diff changeset
   271
val xname = group (fn () => "name reference")
5f5649ac8235 tuned Parse.group: delayed failure message;
wenzelm
parents: 43947
diff changeset
   272
  (short_ident || long_ident || sym_ident || string || number);
5f5649ac8235 tuned Parse.group: delayed failure message;
wenzelm
parents: 43947
diff changeset
   273
5f5649ac8235 tuned Parse.group: delayed failure message;
wenzelm
parents: 43947
diff changeset
   274
val text = group (fn () => "text")
56499
7e0178c84994 allow text cartouches in regular outer syntax categories "text" and "altstring";
wenzelm
parents: 56202
diff changeset
   275
  (short_ident || long_ident || sym_ident || string || number || verbatim || cartouche);
44357
5f5649ac8235 tuned Parse.group: delayed failure message;
wenzelm
parents: 43947
diff changeset
   276
48881
46e053eda5dd clarified Parse.path vs. Parse.explode -- prefer errors in proper transaction context;
wenzelm
parents: 46922
diff changeset
   277
val path = group (fn () => "file name/path specification") name;
6553
dc962d157a63 comment, interest;
wenzelm
parents: 6511
diff changeset
   278
59693
d96cb03caf9e tunes signature -- more uniform ML vs. Scala;
wenzelm
parents: 59081
diff changeset
   279
val theory_name = group (fn () => "theory name") name;
d96cb03caf9e tunes signature -- more uniform ML vs. Scala;
wenzelm
parents: 59081
diff changeset
   280
val theory_xname = group (fn () => "theory name reference") xname;
d96cb03caf9e tunes signature -- more uniform ML vs. Scala;
wenzelm
parents: 59081
diff changeset
   281
56063
38f13d055107 more explicit markup for Token.Literal;
wenzelm
parents: 55828
diff changeset
   282
val liberal_name = keyword_with Token.ident_or_symbolic || xname;
40800
330eb65c9469 Parse.liberal_name for document antiquotations and attributes;
wenzelm
parents: 40793
diff changeset
   283
18898
e3d2aa8ba0e1 added parname;
wenzelm
parents: 18669
diff changeset
   284
val parname = Scan.optional ($$$ "(" |-- name --| $$$ ")") "";
28965
1de908189869 cleaned up binding module and related code
haftmann
parents: 28941
diff changeset
   285
val parbinding = Scan.optional ($$$ "(" |-- binding --| $$$ ")") Binding.empty;
18898
e3d2aa8ba0e1 added parname;
wenzelm
parents: 18669
diff changeset
   286
6553
dc962d157a63 comment, interest;
wenzelm
parents: 6511
diff changeset
   287
46922
3717f3878714 source positions for locale and class expressions;
wenzelm
parents: 45596
diff changeset
   288
(* type classes *)
3717f3878714 source positions for locale and class expressions;
wenzelm
parents: 45596
diff changeset
   289
3717f3878714 source positions for locale and class expressions;
wenzelm
parents: 45596
diff changeset
   290
val class = group (fn () => "type class") (inner_syntax xname);
5826
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   291
44357
5f5649ac8235 tuned Parse.group: delayed failure message;
wenzelm
parents: 43947
diff changeset
   292
val sort = group (fn () => "sort") (inner_syntax xname);
5826
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   293
46922
3717f3878714 source positions for locale and class expressions;
wenzelm
parents: 45596
diff changeset
   294
val type_const = inner_syntax (group (fn () => "type constructor") xname);
3717f3878714 source positions for locale and class expressions;
wenzelm
parents: 45596
diff changeset
   295
3717f3878714 source positions for locale and class expressions;
wenzelm
parents: 45596
diff changeset
   296
val arity = type_const -- ($$$ "::" |-- !!!
22331
7df6bc8cf0b0 unified arity parser/arguments;
wenzelm
parents: 22119
diff changeset
   297
  (Scan.optional ($$$ "(" |-- !!! (list1 sort --| $$$ ")")) [] -- sort)) >> triple2;
5826
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   298
46922
3717f3878714 source positions for locale and class expressions;
wenzelm
parents: 45596
diff changeset
   299
val multi_arity = and_list1 type_const -- ($$$ "::" |-- !!!
25541
68de88c7e877 added parser for multi_arity
haftmann
parents: 24910
diff changeset
   300
  (Scan.optional ($$$ "(" |-- !!! (list1 sort --| $$$ ")")) [] -- sort)) >> triple2;
68de88c7e877 added parser for multi_arity
haftmann
parents: 24910
diff changeset
   301
5826
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   302
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   303
(* types *)
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   304
44357
5f5649ac8235 tuned Parse.group: delayed failure message;
wenzelm
parents: 43947
diff changeset
   305
val typ_group =
5f5649ac8235 tuned Parse.group: delayed failure message;
wenzelm
parents: 43947
diff changeset
   306
  group (fn () => "type")
5f5649ac8235 tuned Parse.group: delayed failure message;
wenzelm
parents: 43947
diff changeset
   307
    (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
   308
27753
94b672153b49 sort/typ/term/prop: inner_syntax markup encodes original source position;
wenzelm
parents: 27737
diff changeset
   309
val typ = inner_syntax typ_group;
94b672153b49 sort/typ/term/prop: inner_syntax markup encodes original source position;
wenzelm
parents: 27737
diff changeset
   310
35838
c8bd075c4de8 support type arguments with sort constraints;
wenzelm
parents: 35351
diff changeset
   311
fun type_arguments arg =
c8bd075c4de8 support type arguments with sort constraints;
wenzelm
parents: 35351
diff changeset
   312
  arg >> single ||
c8bd075c4de8 support type arguments with sort constraints;
wenzelm
parents: 35351
diff changeset
   313
  $$$ "(" |-- !!! (list1 arg --| $$$ ")") ||
5826
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   314
  Scan.succeed [];
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   315
35838
c8bd075c4de8 support type arguments with sort constraints;
wenzelm
parents: 35351
diff changeset
   316
val type_args = type_arguments type_ident;
c8bd075c4de8 support type arguments with sort constraints;
wenzelm
parents: 35351
diff changeset
   317
val type_args_constrained = type_arguments (type_ident -- Scan.option ($$$ "::" |-- !!! sort));
c8bd075c4de8 support type arguments with sort constraints;
wenzelm
parents: 35351
diff changeset
   318
5826
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   319
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   320
(* mixfix annotations *)
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   321
51654
8450b944e58a just one syntax category "mixfix" -- check structure annotation semantically;
wenzelm
parents: 51627
diff changeset
   322
local
8450b944e58a just one syntax category "mixfix" -- check structure annotation semantically;
wenzelm
parents: 51627
diff changeset
   323
18669
cd6d6baf0411 uniform handling of fixes;
wenzelm
parents: 18618
diff changeset
   324
val mfix = string --
cd6d6baf0411 uniform handling of fixes;
wenzelm
parents: 18618
diff changeset
   325
  !!! (Scan.optional ($$$ "[" |-- !!! (list nat --| $$$ "]")) [] --
42297
140f283266b7 discontinued Syntax.max_pri, which is not really a symbolic parameter;
wenzelm
parents: 42287
diff changeset
   326
    Scan.optional nat 1000) >> (Mixfix o triple2);
18669
cd6d6baf0411 uniform handling of fixes;
wenzelm
parents: 18618
diff changeset
   327
35130
0991c84e8dcf renamed InfixName to Infix etc.;
wenzelm
parents: 35129
diff changeset
   328
val infx = $$$ "infix" |-- !!! (string -- nat >> Infix);
0991c84e8dcf renamed InfixName to Infix etc.;
wenzelm
parents: 35129
diff changeset
   329
val infxl = $$$ "infixl" |-- !!! (string -- nat >> Infixl);
0991c84e8dcf renamed InfixName to Infix etc.;
wenzelm
parents: 35129
diff changeset
   330
val infxr = $$$ "infixr" |-- !!! (string -- nat >> Infixr);
51654
8450b944e58a just one syntax category "mixfix" -- check structure annotation semantically;
wenzelm
parents: 51627
diff changeset
   331
val strcture = $$$ "structure" >> K Structure;
5826
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   332
18669
cd6d6baf0411 uniform handling of fixes;
wenzelm
parents: 18618
diff changeset
   333
val binder = $$$ "binder" |--
cd6d6baf0411 uniform handling of fixes;
wenzelm
parents: 18618
diff changeset
   334
  !!! (string -- ($$$ "[" |-- nat --| $$$ "]" -- nat || nat >> (fn n => (n, n))))
cd6d6baf0411 uniform handling of fixes;
wenzelm
parents: 18618
diff changeset
   335
  >> (Binder o triple2);
cd6d6baf0411 uniform handling of fixes;
wenzelm
parents: 18618
diff changeset
   336
51654
8450b944e58a just one syntax category "mixfix" -- check structure annotation semantically;
wenzelm
parents: 51627
diff changeset
   337
val mixfix_body = mfix || strcture || binder || infxl || infxr || infx;
8450b944e58a just one syntax category "mixfix" -- check structure annotation semantically;
wenzelm
parents: 51627
diff changeset
   338
8450b944e58a just one syntax category "mixfix" -- check structure annotation semantically;
wenzelm
parents: 51627
diff changeset
   339
fun annotation guard body = $$$ "(" |-- guard (body --| $$$ ")");
8450b944e58a just one syntax category "mixfix" -- check structure annotation semantically;
wenzelm
parents: 51627
diff changeset
   340
fun opt_annotation guard body = Scan.optional (annotation guard body) NoSyn;
8450b944e58a just one syntax category "mixfix" -- check structure annotation semantically;
wenzelm
parents: 51627
diff changeset
   341
8450b944e58a just one syntax category "mixfix" -- check structure annotation semantically;
wenzelm
parents: 51627
diff changeset
   342
in
18669
cd6d6baf0411 uniform handling of fixes;
wenzelm
parents: 18618
diff changeset
   343
51654
8450b944e58a just one syntax category "mixfix" -- check structure annotation semantically;
wenzelm
parents: 51627
diff changeset
   344
val mixfix = annotation !!! mixfix_body;
8450b944e58a just one syntax category "mixfix" -- check structure annotation semantically;
wenzelm
parents: 51627
diff changeset
   345
val mixfix' = annotation I mixfix_body;
8450b944e58a just one syntax category "mixfix" -- check structure annotation semantically;
wenzelm
parents: 51627
diff changeset
   346
val opt_mixfix = opt_annotation !!! mixfix_body;
8450b944e58a just one syntax category "mixfix" -- check structure annotation semantically;
wenzelm
parents: 51627
diff changeset
   347
val opt_mixfix' = opt_annotation I mixfix_body;
8450b944e58a just one syntax category "mixfix" -- check structure annotation semantically;
wenzelm
parents: 51627
diff changeset
   348
8450b944e58a just one syntax category "mixfix" -- check structure annotation semantically;
wenzelm
parents: 51627
diff changeset
   349
end;
5826
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   350
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   351
18669
cd6d6baf0411 uniform handling of fixes;
wenzelm
parents: 18618
diff changeset
   352
(* fixes *)
5826
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   353
21400
4788fc8e66ea added where_;
wenzelm
parents: 21371
diff changeset
   354
val where_ = $$$ "where";
4788fc8e66ea added where_;
wenzelm
parents: 21371
diff changeset
   355
42299
06e93f257d0e tuned signature;
wenzelm
parents: 42297
diff changeset
   356
val const_decl = name -- ($$$ "::" |-- !!! typ) -- opt_mixfix >> triple1;
30339
3fc32dd7a647 added const_binding;
wenzelm
parents: 30223
diff changeset
   357
val const_binding = binding -- ($$$ "::" |-- !!! typ) -- opt_mixfix >> triple1;
18669
cd6d6baf0411 uniform handling of fixes;
wenzelm
parents: 18618
diff changeset
   358
28081
d664b2c1dfe6 explicit type Name.binding for higher-specification elements;
wenzelm
parents: 28017
diff changeset
   359
val params = Scan.repeat1 binding -- Scan.option ($$$ "::" |-- !!! typ)
18669
cd6d6baf0411 uniform handling of fixes;
wenzelm
parents: 18618
diff changeset
   360
  >> (fn (xs, T) => map (rpair T) xs);
cd6d6baf0411 uniform handling of fixes;
wenzelm
parents: 18618
diff changeset
   361
cd6d6baf0411 uniform handling of fixes;
wenzelm
parents: 18618
diff changeset
   362
val fixes =
45331
6e0a8aba99ec more liberal Parse.fixes, to avoid overlap of mixfix with is-pattern (notably in 'obtain' syntax);
wenzelm
parents: 44357
diff changeset
   363
  and_list1 (binding -- Scan.option ($$$ "::" |-- typ) -- mixfix' >> (single o triple1) ||
42287
d98eb048a2e4 discontinued special treatment of structure Mixfix;
wenzelm
parents: 40800
diff changeset
   364
    params >> map (fn (x, y) => (x, y, NoSyn))) >> flat;
5826
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   365
19845
b8985bf2ce8b added for_fixes;
wenzelm
parents: 19811
diff changeset
   366
val for_fixes = Scan.optional ($$$ "for" |-- !!! fixes) [];
b8985bf2ce8b added for_fixes;
wenzelm
parents: 19811
diff changeset
   367
5826
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   368
27877
af9f0adbab1f renamed P.ml_source to P.ML_source;
wenzelm
parents: 27872
diff changeset
   369
(* embedded source text *)
27872
631371a02b8c P.doc_source and P.ml_sorce for proper SymbolPos.text;
wenzelm
parents: 27815
diff changeset
   370
59809
87641097d0f3 tuned signature;
wenzelm
parents: 59784
diff changeset
   371
val ML_source = input (group (fn () => "ML source") text);
87641097d0f3 tuned signature;
wenzelm
parents: 59784
diff changeset
   372
val document_source = input (group (fn () => "document source") text);
27872
631371a02b8c P.doc_source and P.ml_sorce for proper SymbolPos.text;
wenzelm
parents: 27815
diff changeset
   373
631371a02b8c P.doc_source and P.ml_sorce for proper SymbolPos.text;
wenzelm
parents: 27815
diff changeset
   374
5826
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   375
(* terms *)
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   376
40793
d21aedaa91e7 added Parse.literal_fact with proper inner_syntax markup (source position);
wenzelm
parents: 40296
diff changeset
   377
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
   378
44357
5f5649ac8235 tuned Parse.group: delayed failure message;
wenzelm
parents: 43947
diff changeset
   379
val term_group = group (fn () => "term") tm;
5f5649ac8235 tuned Parse.group: delayed failure message;
wenzelm
parents: 43947
diff changeset
   380
val prop_group = group (fn () => "proposition") tm;
27753
94b672153b49 sort/typ/term/prop: inner_syntax markup encodes original source position;
wenzelm
parents: 27737
diff changeset
   381
94b672153b49 sort/typ/term/prop: inner_syntax markup encodes original source position;
wenzelm
parents: 27737
diff changeset
   382
val term = inner_syntax term_group;
94b672153b49 sort/typ/term/prop: inner_syntax markup encodes original source position;
wenzelm
parents: 27737
diff changeset
   383
val prop = inner_syntax prop_group;
5826
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   384
44357
5f5649ac8235 tuned Parse.group: delayed failure message;
wenzelm
parents: 43947
diff changeset
   385
val const = inner_syntax (group (fn () => "constant") xname);
42300
0d1cbc1fe579 notation: proper markup for type constructor / constant;
wenzelm
parents: 42299
diff changeset
   386
56499
7e0178c84994 allow text cartouches in regular outer syntax categories "text" and "altstring";
wenzelm
parents: 56202
diff changeset
   387
val literal_fact = inner_syntax (group (fn () => "literal fact") (alt_string || cartouche));
40793
d21aedaa91e7 added Parse.literal_fact with proper inner_syntax markup (source position);
wenzelm
parents: 40296
diff changeset
   388
5826
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   389
6949
a0b34115077f added termp;
wenzelm
parents: 6935
diff changeset
   390
(* patterns *)
6935
a3f3f4128cab propp: 'concl' patterns;
wenzelm
parents: 6860
diff changeset
   391
6949
a0b34115077f added termp;
wenzelm
parents: 6935
diff changeset
   392
val is_terms = Scan.repeat1 ($$$ "is" |-- term);
6935
a3f3f4128cab propp: 'concl' patterns;
wenzelm
parents: 6860
diff changeset
   393
val is_props = Scan.repeat1 ($$$ "is" |-- prop);
a3f3f4128cab propp: 'concl' patterns;
wenzelm
parents: 6860
diff changeset
   394
19585
70a1ce3b23ae removed 'concl is' patterns;
wenzelm
parents: 19482
diff changeset
   395
val propp = prop -- Scan.optional ($$$ "(" |-- !!! (is_props --| $$$ ")")) [];
6949
a0b34115077f added termp;
wenzelm
parents: 6935
diff changeset
   396
val termp = term -- Scan.optional ($$$ "(" |-- !!! (is_terms --| $$$ ")")) [];
6935
a3f3f4128cab propp: 'concl' patterns;
wenzelm
parents: 6860
diff changeset
   397
a3f3f4128cab propp: 'concl' patterns;
wenzelm
parents: 6860
diff changeset
   398
22119
6f1c82c0243c moved parts to spec_parse.ML;
wenzelm
parents: 21858
diff changeset
   399
(* targets *)
19811
46abcbb2da9d added locale_insts;
wenzelm
parents: 19585
diff changeset
   400
45488
6d71d9e52369 pass positions for named targets, for formal links in the document model;
wenzelm
parents: 45331
diff changeset
   401
val target = ($$$ "(" -- $$$ "in") |-- !!! (position xname --| $$$ ")");
22119
6f1c82c0243c moved parts to spec_parse.ML;
wenzelm
parents: 21858
diff changeset
   402
val opt_target = Scan.option target;
12272
9bc50336dab6 improved locale expression syntax;
wenzelm
parents: 12268
diff changeset
   403
56201
dd2df97b379b tuned signature;
wenzelm
parents: 56063
diff changeset
   404
dd2df97b379b tuned signature;
wenzelm
parents: 56063
diff changeset
   405
(* arguments within outer syntax *)
dd2df97b379b tuned signature;
wenzelm
parents: 56063
diff changeset
   406
dd2df97b379b tuned signature;
wenzelm
parents: 56063
diff changeset
   407
local
dd2df97b379b tuned signature;
wenzelm
parents: 56063
diff changeset
   408
dd2df97b379b tuned signature;
wenzelm
parents: 56063
diff changeset
   409
val argument_kinds =
59081
2ceb05ee0331 clarified token kind;
wenzelm
parents: 59064
diff changeset
   410
 [Token.Ident, Token.Long_Ident, Token.Sym_Ident, Token.Var, Token.Type_Ident, Token.Type_Var,
2ceb05ee0331 clarified token kind;
wenzelm
parents: 59064
diff changeset
   411
  Token.Nat, Token.Float, Token.String, Token.Alt_String, Token.Cartouche, Token.Verbatim];
56201
dd2df97b379b tuned signature;
wenzelm
parents: 56063
diff changeset
   412
dd2df97b379b tuned signature;
wenzelm
parents: 56063
diff changeset
   413
fun arguments is_symid =
dd2df97b379b tuned signature;
wenzelm
parents: 56063
diff changeset
   414
  let
dd2df97b379b tuned signature;
wenzelm
parents: 56063
diff changeset
   415
    fun argument blk =
dd2df97b379b tuned signature;
wenzelm
parents: 56063
diff changeset
   416
      group (fn () => "argument")
dd2df97b379b tuned signature;
wenzelm
parents: 56063
diff changeset
   417
        (Scan.one (fn tok =>
dd2df97b379b tuned signature;
wenzelm
parents: 56063
diff changeset
   418
          let val kind = Token.kind_of tok in
dd2df97b379b tuned signature;
wenzelm
parents: 56063
diff changeset
   419
            member (op =) argument_kinds kind orelse
dd2df97b379b tuned signature;
wenzelm
parents: 56063
diff changeset
   420
            Token.keyword_with is_symid tok orelse
dd2df97b379b tuned signature;
wenzelm
parents: 56063
diff changeset
   421
            (blk andalso Token.keyword_with (fn s => s = ",") tok)
dd2df97b379b tuned signature;
wenzelm
parents: 56063
diff changeset
   422
          end));
dd2df97b379b tuned signature;
wenzelm
parents: 56063
diff changeset
   423
dd2df97b379b tuned signature;
wenzelm
parents: 56063
diff changeset
   424
    fun args blk x = Scan.optional (args1 blk) [] x
dd2df97b379b tuned signature;
wenzelm
parents: 56063
diff changeset
   425
    and args1 blk x =
dd2df97b379b tuned signature;
wenzelm
parents: 56063
diff changeset
   426
      ((Scan.repeat1
dd2df97b379b tuned signature;
wenzelm
parents: 56063
diff changeset
   427
        (Scan.repeat1 (argument blk) ||
dd2df97b379b tuned signature;
wenzelm
parents: 56063
diff changeset
   428
          argsp "(" ")" ||
dd2df97b379b tuned signature;
wenzelm
parents: 56063
diff changeset
   429
          argsp "[" "]")) >> flat) x
dd2df97b379b tuned signature;
wenzelm
parents: 56063
diff changeset
   430
    and argsp l r x = (token ($$$ l) ::: !!! (args true @@@ (token ($$$ r) >> single))) x;
dd2df97b379b tuned signature;
wenzelm
parents: 56063
diff changeset
   431
  in (args, args1) end;
dd2df97b379b tuned signature;
wenzelm
parents: 56063
diff changeset
   432
dd2df97b379b tuned signature;
wenzelm
parents: 56063
diff changeset
   433
in
dd2df97b379b tuned signature;
wenzelm
parents: 56063
diff changeset
   434
dd2df97b379b tuned signature;
wenzelm
parents: 56063
diff changeset
   435
val args = #1 (arguments Token.ident_or_symbolic) false;
dd2df97b379b tuned signature;
wenzelm
parents: 56063
diff changeset
   436
fun args1 is_symid = #2 (arguments is_symid) false;
dd2df97b379b tuned signature;
wenzelm
parents: 56063
diff changeset
   437
dd2df97b379b tuned signature;
wenzelm
parents: 56063
diff changeset
   438
end;
dd2df97b379b tuned signature;
wenzelm
parents: 56063
diff changeset
   439
58028
e4250d370657 tuned signature -- define some elementary operations earlier;
wenzelm
parents: 58011
diff changeset
   440
e4250d370657 tuned signature -- define some elementary operations earlier;
wenzelm
parents: 58011
diff changeset
   441
(* attributes *)
e4250d370657 tuned signature -- define some elementary operations earlier;
wenzelm
parents: 58011
diff changeset
   442
e4250d370657 tuned signature -- define some elementary operations earlier;
wenzelm
parents: 58011
diff changeset
   443
val attrib = position liberal_name -- !!! args >> uncurry Token.src;
e4250d370657 tuned signature -- define some elementary operations earlier;
wenzelm
parents: 58011
diff changeset
   444
val attribs = $$$ "[" |-- list attrib --| $$$ "]";
e4250d370657 tuned signature -- define some elementary operations earlier;
wenzelm
parents: 58011
diff changeset
   445
val opt_attribs = Scan.optional attribs [];
e4250d370657 tuned signature -- define some elementary operations earlier;
wenzelm
parents: 58011
diff changeset
   446
e4250d370657 tuned signature -- define some elementary operations earlier;
wenzelm
parents: 58011
diff changeset
   447
e4250d370657 tuned signature -- define some elementary operations earlier;
wenzelm
parents: 58011
diff changeset
   448
(* theorem references *)
e4250d370657 tuned signature -- define some elementary operations earlier;
wenzelm
parents: 58011
diff changeset
   449
e4250d370657 tuned signature -- define some elementary operations earlier;
wenzelm
parents: 58011
diff changeset
   450
val thm_sel = $$$ "(" |-- list1
e4250d370657 tuned signature -- define some elementary operations earlier;
wenzelm
parents: 58011
diff changeset
   451
 (nat --| minus -- nat >> Facts.FromTo ||
e4250d370657 tuned signature -- define some elementary operations earlier;
wenzelm
parents: 58011
diff changeset
   452
  nat --| minus >> Facts.From ||
e4250d370657 tuned signature -- define some elementary operations earlier;
wenzelm
parents: 58011
diff changeset
   453
  nat >> Facts.Single) --| $$$ ")";
e4250d370657 tuned signature -- define some elementary operations earlier;
wenzelm
parents: 58011
diff changeset
   454
e4250d370657 tuned signature -- define some elementary operations earlier;
wenzelm
parents: 58011
diff changeset
   455
val xthm =
e4250d370657 tuned signature -- define some elementary operations earlier;
wenzelm
parents: 58011
diff changeset
   456
  $$$ "[" |-- attribs --| $$$ "]" >> pair (Facts.named "") ||
e4250d370657 tuned signature -- define some elementary operations earlier;
wenzelm
parents: 58011
diff changeset
   457
  (literal_fact >> Facts.Fact ||
e4250d370657 tuned signature -- define some elementary operations earlier;
wenzelm
parents: 58011
diff changeset
   458
    position xname -- Scan.option thm_sel >> Facts.Named) -- opt_attribs;
e4250d370657 tuned signature -- define some elementary operations earlier;
wenzelm
parents: 58011
diff changeset
   459
e4250d370657 tuned signature -- define some elementary operations earlier;
wenzelm
parents: 58011
diff changeset
   460
val xthms1 = Scan.repeat1 xthm;
e4250d370657 tuned signature -- define some elementary operations earlier;
wenzelm
parents: 58011
diff changeset
   461
12272
9bc50336dab6 improved locale expression syntax;
wenzelm
parents: 12268
diff changeset
   462
end;