src/Pure/Isar/outer_parse.ML
author wenzelm
Wed, 30 Jun 1999 12:23:46 +0200
changeset 6860 8dc6a1e6fa13
parent 6726 ac968ce542a8
child 6935 a3f3f4128cab
permissions -rw-r--r--
added sync;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
5826
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/Isar/outer_parse.ML
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
     3
    Author:     Markus Wenzel, TU Muenchen
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
     4
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
     5
Generic parsers for Isabelle/Isar outer syntax.
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
     6
*)
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
     7
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
     8
signature OUTER_PARSE =
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
     9
sig
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
    10
  type token
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
    11
  val group: string -> (token list -> 'a) -> token list -> 'a
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
    12
  val !!! : (token list -> 'a) -> token list -> 'a
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
    13
  val $$$ : string -> token list -> string * token list
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
    14
  val position: (token list -> 'a * 'b) -> token list -> ('a * Position.T) * 'b
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
    15
  val keyword: token list -> string * token list
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
    16
  val short_ident: token list -> string * token list
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
    17
  val long_ident: token list -> string * token list
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
    18
  val sym_ident: token list -> string * token list
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
    19
  val term_var: token list -> string * token list
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
    20
  val text_var: token list -> string * token list
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
    21
  val type_ident: token list -> string * token list
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
    22
  val type_var: token list -> string * token list
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
    23
  val number: token list -> string * token list
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
    24
  val string: token list -> string * token list
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
    25
  val verbatim: token list -> string * token list
6860
8dc6a1e6fa13 added sync;
wenzelm
parents: 6726
diff changeset
    26
  val sync: token list -> string * token list
5826
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
    27
  val eof: token list -> string * token list
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
    28
  val not_eof: token list -> token * token list
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
    29
  val nat: token list -> int * token list
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
    30
  val enum: string -> (token list -> 'a * token list) -> token list -> 'a list * token list
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
    31
  val enum1: string -> (token list -> 'a * token list) -> token list -> 'a list * token list
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
    32
  val list: (token list -> 'a * token list) -> token list -> 'a list * token list
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
    33
  val list1: (token list -> 'a * token list) -> token list -> 'a list * token list
6013
6da9ae6d40f5 and_list;
wenzelm
parents: 6003
diff changeset
    34
  val and_list: (token list -> 'a * token list) -> token list -> 'a list * token list
6da9ae6d40f5 and_list;
wenzelm
parents: 6003
diff changeset
    35
  val and_list1: (token list -> 'a * token list) -> token list -> 'a list * token list
5826
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
    36
  val name: token list -> bstring * token list
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
    37
  val xname: token list -> xstring * token list
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
    38
  val text: token list -> string * token list
6553
dc962d157a63 comment, interest;
wenzelm
parents: 6511
diff changeset
    39
  val comment: token list -> Comment.text * token list
dc962d157a63 comment, interest;
wenzelm
parents: 6511
diff changeset
    40
  val marg_comment: token list -> Comment.text * token list
dc962d157a63 comment, interest;
wenzelm
parents: 6511
diff changeset
    41
  val interest: token list -> Comment.interest * token list
5826
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
    42
  val sort: token list -> xsort * token list
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
    43
  val arity: token list -> (xsort list * xsort) * token list
6372
44b104595441 added simple_arity, spec_name, spec_opt_name;
wenzelm
parents: 6355
diff changeset
    44
  val simple_arity: token list -> (xsort list * xclass) * token list
5826
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
    45
  val type_args: token list -> string list * token list
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
    46
  val typ: token list -> string * token list
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
    47
  val opt_infix: token list -> Syntax.mixfix * token list
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
    48
  val opt_mixfix: token list -> Syntax.mixfix * token list
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
    49
  val const: token list -> (bstring * string * Syntax.mixfix) * token list
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
    50
  val term: token list -> string * token list
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
    51
  val prop: token list -> string * token list
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
    52
  val attribs: token list -> Args.src list * token list
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
    53
  val opt_attribs: token list -> Args.src list * token list
5917
dcb669fda86b generalized (opt_)thm_name;
wenzelm
parents: 5877
diff changeset
    54
  val thm_name: string -> token list -> (bstring * Args.src list) * token list
dcb669fda86b generalized (opt_)thm_name;
wenzelm
parents: 5877
diff changeset
    55
  val opt_thm_name: string -> token list -> (bstring * Args.src list) * token list
6372
44b104595441 added simple_arity, spec_name, spec_opt_name;
wenzelm
parents: 6355
diff changeset
    56
  val spec_name: token list -> ((bstring * string) * Args.src list) * token list
44b104595441 added simple_arity, spec_name, spec_opt_name;
wenzelm
parents: 6355
diff changeset
    57
  val spec_opt_name: token list -> ((bstring * string) * Args.src list) * token list
5917
dcb669fda86b generalized (opt_)thm_name;
wenzelm
parents: 5877
diff changeset
    58
  val xthm: token list -> (xstring * Args.src list) * token list
dcb669fda86b generalized (opt_)thm_name;
wenzelm
parents: 5877
diff changeset
    59
  val xthms1: token list -> (xstring * Args.src list) list * token list
5826
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
    60
  val method: token list -> Method.text * token list
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
    61
  val triple1: ('a * 'b) * 'c -> 'a * 'b * 'c
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
    62
  val triple2: 'a * ('b * 'c) -> 'a * 'b * 'c
6430
69400c97d3bf triple_swap;
wenzelm
parents: 6398
diff changeset
    63
  val triple_swap: ('a * 'b) * 'c -> ('a * 'c) * 'b
5826
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
    64
end;
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
    65
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
    66
structure OuterParse: OUTER_PARSE =
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
    67
struct
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
    68
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
    69
type token = OuterLex.token;
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
    70
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
    71
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
    72
(** error handling **)
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
    73
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
    74
(* group atomic parsers (no cuts!) *)
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
    75
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
    76
fun fail_with s = Scan.fail_with
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
    77
  (fn [] => s ^ " expected (past end-of-file!)"
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
    78
    | (tok :: _) => s ^ " expected,\nbut " ^ OuterLex.name_of tok ^ " " ^
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
    79
      quote (OuterLex.val_of tok) ^ OuterLex.pos_of tok ^ " was found");
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
    80
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
    81
fun group s scan = scan || fail_with s;
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
    82
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
    83
5877
ee214dec5657 removed args, args1, thm_xname;
wenzelm
parents: 5826
diff changeset
    84
(* cut *)
5826
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
    85
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
    86
fun !!! scan =
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
    87
  let
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
    88
    fun get_pos [] = " (past end-of-file!)"
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
    89
      | get_pos (tok :: _) = OuterLex.pos_of tok;
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
    90
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
    91
    fun err (toks, None) = "Outer syntax error" ^ get_pos toks
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
    92
      | err (toks, Some msg) = "Outer syntax error" ^ get_pos toks ^ ": " ^ msg;
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
    93
  in Scan.!! err scan end;
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
    94
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
    95
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
    96
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
    97
(** basic parsers **)
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
    98
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
    99
(* utils *)
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   100
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   101
fun triple1 ((x, y), z) = (x, y, z);
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   102
fun triple2 (x, (y, z)) = (x, y, z);
6430
69400c97d3bf triple_swap;
wenzelm
parents: 6398
diff changeset
   103
fun triple_swap ((x, y), z) = ((x, z), y);
5826
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   104
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   105
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   106
(* tokens *)
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   107
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   108
fun position scan =
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   109
  (Scan.ahead (Scan.one OuterLex.not_eof) >> OuterLex.position_of) -- scan >> Library.swap;
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
fun kind k =
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   112
  group (OuterLex.str_of_kind k)
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   113
    (Scan.one (OuterLex.is_kind k) >> OuterLex.val_of);
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
val keyword = kind OuterLex.Keyword;
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   116
val short_ident = kind OuterLex.Ident;
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   117
val long_ident = kind OuterLex.LongIdent;
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   118
val sym_ident = kind OuterLex.SymIdent;
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   119
val term_var = kind OuterLex.Var;
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   120
val text_var = kind OuterLex.TextVar;
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   121
val type_ident = kind OuterLex.TypeIdent;
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   122
val type_var = kind OuterLex.TypeVar;
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   123
val number = kind OuterLex.Nat;
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   124
val string = kind OuterLex.String;
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   125
val verbatim = kind OuterLex.Verbatim;
6860
8dc6a1e6fa13 added sync;
wenzelm
parents: 6726
diff changeset
   126
val sync = kind OuterLex.Sync;
5826
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   127
val eof = kind OuterLex.EOF;
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   128
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   129
fun $$$ x =
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   130
  group (OuterLex.str_of_kind OuterLex.Keyword ^ " " ^ quote x)
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   131
    (Scan.one (OuterLex.is_kind OuterLex.Keyword andf (equal x o OuterLex.val_of))
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   132
      >> OuterLex.val_of);
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   133
5877
ee214dec5657 removed args, args1, thm_xname;
wenzelm
parents: 5826
diff changeset
   134
val nat = number >> (fst o Term.read_int o Symbol.explode);
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
val not_eof = Scan.one OuterLex.not_eof;
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   137
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   138
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   139
(* enumerations *)
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   140
6003
b382568901f6 enum: !!! after seperator;
wenzelm
parents: 5960
diff changeset
   141
fun enum1 sep scan = scan -- Scan.repeat ($$$ sep |-- !!! scan) >> op ::;
5826
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   142
fun enum sep scan = enum1 sep scan || Scan.succeed [];
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
fun list1 scan = enum1 "," scan;
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   145
fun list scan = enum "," scan;
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   146
6013
6da9ae6d40f5 and_list;
wenzelm
parents: 6003
diff changeset
   147
fun and_list1 scan = enum1 "and" scan;
6da9ae6d40f5 and_list;
wenzelm
parents: 6003
diff changeset
   148
fun and_list scan = enum "and" scan;
6da9ae6d40f5 and_list;
wenzelm
parents: 6003
diff changeset
   149
5826
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   150
5960
2bebd0d0a961 comment parser;
wenzelm
parents: 5940
diff changeset
   151
(* names and text *)
5826
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   152
5877
ee214dec5657 removed args, args1, thm_xname;
wenzelm
parents: 5826
diff changeset
   153
val name = group "name declaration" (short_ident || sym_ident || string);
ee214dec5657 removed args, args1, thm_xname;
wenzelm
parents: 5826
diff changeset
   154
val xname = group "name reference" (short_ident || long_ident || sym_ident || string);
6553
dc962d157a63 comment, interest;
wenzelm
parents: 6511
diff changeset
   155
val text = group "text" (short_ident || long_ident || sym_ident || string || verbatim);
dc962d157a63 comment, interest;
wenzelm
parents: 6511
diff changeset
   156
dc962d157a63 comment, interest;
wenzelm
parents: 6511
diff changeset
   157
dc962d157a63 comment, interest;
wenzelm
parents: 6511
diff changeset
   158
(* formal comments *)
dc962d157a63 comment, interest;
wenzelm
parents: 6511
diff changeset
   159
dc962d157a63 comment, interest;
wenzelm
parents: 6511
diff changeset
   160
val comment = text >> Comment.plain;
6726
ac968ce542a8 renamed Comment.empty to Comment.none;
wenzelm
parents: 6558
diff changeset
   161
val marg_comment = Scan.optional ($$$ "--" |-- comment) Comment.none;
6553
dc962d157a63 comment, interest;
wenzelm
parents: 6511
diff changeset
   162
val interest = Scan.optional ($$$ "%" >> K Comment.no_interest) Comment.default_interest;
5826
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   163
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   164
6372
44b104595441 added simple_arity, spec_name, spec_opt_name;
wenzelm
parents: 6355
diff changeset
   165
(* sorts and arities *)
5826
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
val sort =
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   168
  xname >> single || $$$ "{" |-- !!! (list xname --| $$$ "}");
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   169
6372
44b104595441 added simple_arity, spec_name, spec_opt_name;
wenzelm
parents: 6355
diff changeset
   170
fun gen_arity cod =
44b104595441 added simple_arity, spec_name, spec_opt_name;
wenzelm
parents: 6355
diff changeset
   171
  Scan.optional ($$$ "(" |-- !!! (Scan.repeat1 sort --| $$$ ")")) [] -- cod;
44b104595441 added simple_arity, spec_name, spec_opt_name;
wenzelm
parents: 6355
diff changeset
   172
44b104595441 added simple_arity, spec_name, spec_opt_name;
wenzelm
parents: 6355
diff changeset
   173
val arity = gen_arity sort;
44b104595441 added simple_arity, spec_name, spec_opt_name;
wenzelm
parents: 6355
diff changeset
   174
val simple_arity = gen_arity name;
5826
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   175
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   176
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   177
(* types *)
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   178
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   179
val typ =
6553
dc962d157a63 comment, interest;
wenzelm
parents: 6511
diff changeset
   180
  group "type" (short_ident || long_ident || sym_ident || type_ident || type_var || string);
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
val type_args =
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   183
  type_ident >> single ||
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   184
  $$$ "(" |-- !!! (list1 type_ident --| $$$ ")") ||
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   185
  Scan.succeed [];
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   186
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   187
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   188
(* mixfix annotations *)
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   189
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   190
val infxl = $$$ "infixl" |-- !!! (nat >> Syntax.Infixl || string -- nat >> Syntax.InfixlName);
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   191
val infxr = $$$ "infixr" |-- !!! (nat >> Syntax.Infixr || string -- nat >> Syntax.InfixrName);
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   192
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   193
val binder =
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   194
  $$$ "binder" |--
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   195
    !!! (string -- ($$$ "[" |-- nat --| $$$ "]" -- nat || nat >> (fn n => (n, n))))
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   196
  >> (Syntax.Binder o triple2);
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   197
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   198
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   199
val opt_pris = Scan.optional ($$$ "[" |-- !!! (list nat --| $$$ "]")) [];
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   200
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   201
val mixfix =
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   202
  string -- opt_pris -- Scan.optional nat Syntax.max_pri
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   203
  >> (Syntax.Mixfix o triple1);
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   204
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   205
fun opt_fix fix =
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   206
  Scan.optional ($$$ "(" |-- !!! (fix --| $$$ ")")) Syntax.NoSyn;
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   207
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   208
val opt_infix = opt_fix (infxl || infxr);
6355
f05492a711b1 tuned opt_mixfix failure;
wenzelm
parents: 6013
diff changeset
   209
val opt_mixfix = opt_fix (mixfix || binder || infxl || infxr);
5826
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   210
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   211
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   212
(* consts *)
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   213
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   214
val const =
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   215
  name -- ($$$ "::" |-- !!! (typ -- opt_mixfix)) >> triple2;
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   216
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   217
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   218
(* terms *)
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   219
6553
dc962d157a63 comment, interest;
wenzelm
parents: 6511
diff changeset
   220
val trm = short_ident || long_ident || sym_ident || term_var || text_var || string;
5826
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   221
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   222
val term = group "term" trm;
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   223
val prop = group "proposition" trm;
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   224
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   225
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   226
(* arguments *)
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   227
5877
ee214dec5657 removed args, args1, thm_xname;
wenzelm
parents: 5826
diff changeset
   228
val keyword_symid = Scan.one (OuterLex.keyword_pred OuterLex.is_sid) >> OuterLex.val_of;
5826
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   229
5877
ee214dec5657 removed args, args1, thm_xname;
wenzelm
parents: 5826
diff changeset
   230
fun atom_arg blk =
5826
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   231
  group "argument"
5877
ee214dec5657 removed args, args1, thm_xname;
wenzelm
parents: 5826
diff changeset
   232
    (position (short_ident || long_ident || sym_ident || term_var || text_var ||
ee214dec5657 removed args, args1, thm_xname;
wenzelm
parents: 5826
diff changeset
   233
        type_ident || type_var || number) >> Args.ident ||
ee214dec5657 removed args, args1, thm_xname;
wenzelm
parents: 5826
diff changeset
   234
      position keyword_symid >> Args.keyword ||
ee214dec5657 removed args, args1, thm_xname;
wenzelm
parents: 5826
diff changeset
   235
      position string >> Args.string ||
ee214dec5657 removed args, args1, thm_xname;
wenzelm
parents: 5826
diff changeset
   236
      position (if blk then $$$ "," else Scan.fail) >> Args.keyword);
5826
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   237
5877
ee214dec5657 removed args, args1, thm_xname;
wenzelm
parents: 5826
diff changeset
   238
fun paren_args l r scan = position ($$$ l) -- !!! (scan true -- position ($$$ r))
5826
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   239
  >> (fn (x, (ys, z)) => Args.keyword x :: ys @ [Args.keyword z]);
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   240
5877
ee214dec5657 removed args, args1, thm_xname;
wenzelm
parents: 5826
diff changeset
   241
fun args blk x = Scan.optional (args1 blk) [] x
ee214dec5657 removed args, args1, thm_xname;
wenzelm
parents: 5826
diff changeset
   242
and args1 blk x =
5826
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   243
  ((Scan.repeat1
5877
ee214dec5657 removed args, args1, thm_xname;
wenzelm
parents: 5826
diff changeset
   244
    (Scan.repeat1 (atom_arg blk) ||
5826
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   245
      paren_args "(" ")" args ||
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   246
      paren_args "{" "}" args ||
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   247
      paren_args "[" "]" args)) >> flat) x;
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   248
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   249
6372
44b104595441 added simple_arity, spec_name, spec_opt_name;
wenzelm
parents: 6355
diff changeset
   250
(* theorem specifications *)
5826
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   251
5877
ee214dec5657 removed args, args1, thm_xname;
wenzelm
parents: 5826
diff changeset
   252
val attrib = position (xname -- !!! (args false)) >> Args.src;
5826
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   253
val attribs = $$$ "[" |-- !!! (list attrib --| $$$ "]");
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   254
val opt_attribs = Scan.optional attribs [];
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   255
6398
e6f0c192ef88 fixed thm_name again;
wenzelm
parents: 6372
diff changeset
   256
fun thm_name s = name -- opt_attribs --| $$$ s;
6511
11b07125422e opt_thm_name: name optional;
wenzelm
parents: 6430
diff changeset
   257
fun opt_thm_name s =
11b07125422e opt_thm_name: name optional;
wenzelm
parents: 6430
diff changeset
   258
  Scan.optional ((name -- opt_attribs || (attribs >> pair "")) --| $$$ s) ("", []);;
5917
dcb669fda86b generalized (opt_)thm_name;
wenzelm
parents: 5877
diff changeset
   259
6372
44b104595441 added simple_arity, spec_name, spec_opt_name;
wenzelm
parents: 6355
diff changeset
   260
val spec_name = thm_name ":" -- prop >> (fn ((x, y), z) => ((x, z), y));
44b104595441 added simple_arity, spec_name, spec_opt_name;
wenzelm
parents: 6355
diff changeset
   261
val spec_opt_name = opt_thm_name ":" -- prop >> (fn ((x, y), z) => ((x, z), y));
44b104595441 added simple_arity, spec_name, spec_opt_name;
wenzelm
parents: 6355
diff changeset
   262
5917
dcb669fda86b generalized (opt_)thm_name;
wenzelm
parents: 5877
diff changeset
   263
val xthm = xname -- opt_attribs;
6372
44b104595441 added simple_arity, spec_name, spec_opt_name;
wenzelm
parents: 6355
diff changeset
   264
val xthms1 = Scan.repeat1 xthm;
5826
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   265
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   266
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   267
(* proof methods *)
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   268
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   269
fun meth4 x =
5877
ee214dec5657 removed args, args1, thm_xname;
wenzelm
parents: 5826
diff changeset
   270
 (position (xname >> rpair []) >> (Method.Source o Args.src) ||
5826
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   271
  $$$ "(" |-- meth0 --| $$$ ")") x
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   272
and meth3 x =
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   273
 (meth4 --| $$$ "?" >> Method.Try ||
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   274
  meth4 --| $$$ "*" >> Method.Repeat ||
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   275
  meth4 --| $$$ "+" >> Method.Repeat1 ||
5940
33bdc03bba7e fixed method syntax;
wenzelm
parents: 5917
diff changeset
   276
  meth4) x
33bdc03bba7e fixed method syntax;
wenzelm
parents: 5917
diff changeset
   277
and meth2 x =
33bdc03bba7e fixed method syntax;
wenzelm
parents: 5917
diff changeset
   278
 (position (xname -- args1 false) >> (Method.Source o Args.src) ||
5826
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   279
  meth3) x
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   280
and meth1 x = (enum1 "," meth2 >> (fn [m] => m | ms => Method.Then ms)) x
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   281
and meth0 x = (enum1 "|" meth1 >> (fn [m] => m | ms => Method.Orelse ms)) x;
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   282
6558
120ff48e8618 method = meth3 (again);
wenzelm
parents: 6553
diff changeset
   283
val method = meth3;
5826
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   284
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   285
977f789566b7 Generic parsers for Isabelle/Isar outer syntax.
wenzelm
parents:
diff changeset
   286
end;