src/Pure/Isar/outer_lex.ML
author wenzelm
Sat, 08 Dec 2007 21:20:05 +0100
changeset 25582 655453e635c4
parent 25579 22869d9d545b
child 25642 ebdff0dca2a5
permissions -rw-r--r--
text_of: make double sure that result is well-formed, to avoid recurrent failures;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
5825
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/Isar/outer_lex.ML
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
     3
    Author:     Markus Wenzel, TU Muenchen
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
     4
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
     5
Outer lexical syntax for Isabelle/Isar.
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
     6
*)
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
     7
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
     8
signature OUTER_LEX =
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
     9
sig
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
    10
  datatype token_kind =
23729
d1ba656978c5 separated Malformed (symbolic char) from Error (bad input);
wenzelm
parents: 23721
diff changeset
    11
    Command | Keyword | Ident | LongIdent | SymIdent | Var | TypeIdent | TypeVar | Nat |
23788
54ce229dc858 Symbol.not_eof/sync is superceded by Symbol.is_regular (rules out further control symbols);
wenzelm
parents: 23729
diff changeset
    12
    String | AltString | Verbatim | Space | Comment | Malformed | Error of string | Sync | EOF
15143
05b5995f214e Make token an eqtype to assist reconstructing input
aspinall
parents: 14991
diff changeset
    13
  eqtype token
5825
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
    14
  val str_of_kind: token_kind -> string
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
    15
  val stopper: token * (token -> bool)
6859
2b3db2b6c129 sync token;
wenzelm
parents: 6743
diff changeset
    16
  val not_sync: token -> bool
5825
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
    17
  val not_eof: token -> bool
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
    18
  val position_of: token -> Position.T
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
    19
  val pos_of: token -> string
23721
aa088ef9237c added kind_of;
wenzelm
parents: 23682
diff changeset
    20
  val kind_of: token -> token_kind
5825
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
    21
  val is_kind: token_kind -> token -> bool
7026
69724548fad1 separate command tokens;
wenzelm
parents: 6859
diff changeset
    22
  val keyword_with: (string -> bool) -> token -> bool
16029
070ed43b86f8 added ident_with;
wenzelm
parents: 15531
diff changeset
    23
  val ident_with: (string -> bool) -> token -> bool
5825
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
    24
  val is_proper: token -> bool
9130
ff8789b49d2e added !!!;
wenzelm
parents: 9051
diff changeset
    25
  val is_semicolon: token -> bool
17069
ee08b2466a09 clarify is_newline vs. is_blank;
wenzelm
parents: 16029
diff changeset
    26
  val is_comment: token -> bool
8580
e79ee31d3936 added is_begin/end_ignore;
wenzelm
parents: 8231
diff changeset
    27
  val is_begin_ignore: token -> bool
e79ee31d3936 added is_begin/end_ignore;
wenzelm
parents: 8231
diff changeset
    28
  val is_end_ignore: token -> bool
17069
ee08b2466a09 clarify is_newline vs. is_blank;
wenzelm
parents: 16029
diff changeset
    29
  val is_blank: token -> bool
8651
f095f3b8181a added is_newline;
wenzelm
parents: 8580
diff changeset
    30
  val is_newline: token -> bool
14991
26fb63c4acb5 added unparse;
wenzelm
parents: 14981
diff changeset
    31
  val unparse: token -> string
23788
54ce229dc858 Symbol.not_eof/sync is superceded by Symbol.is_regular (rules out further control symbols);
wenzelm
parents: 23729
diff changeset
    32
  val text_of: token -> string * string
5825
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
    33
  val val_of: token -> string
5876
273056b673ec replaced is_symid by is_sid;
wenzelm
parents: 5825
diff changeset
    34
  val is_sid: string -> bool
9130
ff8789b49d2e added !!!;
wenzelm
parents: 9051
diff changeset
    35
  val !!! : string -> (Position.T * 'a -> 'b) -> Position.T * 'a -> 'b
ff8789b49d2e added !!!;
wenzelm
parents: 9051
diff changeset
    36
  val incr_line: ('a -> 'b * 'c) -> Position.T * 'a -> 'b * (Position.T * 'c)
ff8789b49d2e added !!!;
wenzelm
parents: 9051
diff changeset
    37
  val keep_line: ('a -> 'b * 'c) -> Position.T * 'a -> 'b * (Position.T * 'c)
ff8789b49d2e added !!!;
wenzelm
parents: 9051
diff changeset
    38
  val scan_blank: Position.T * Symbol.symbol list
ff8789b49d2e added !!!;
wenzelm
parents: 9051
diff changeset
    39
    -> Symbol.symbol * (Position.T * Symbol.symbol list)
ff8789b49d2e added !!!;
wenzelm
parents: 9051
diff changeset
    40
  val scan_string: Position.T * Symbol.symbol list -> string * (Position.T * Symbol.symbol list)
7026
69724548fad1 separate command tokens;
wenzelm
parents: 6859
diff changeset
    41
  val scan: (Scan.lexicon * Scan.lexicon) ->
5825
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
    42
    Position.T * Symbol.symbol list -> token * (Position.T * Symbol.symbol list)
23721
aa088ef9237c added kind_of;
wenzelm
parents: 23682
diff changeset
    43
  val source: bool option -> (unit -> Scan.lexicon * Scan.lexicon) ->
7026
69724548fad1 separate command tokens;
wenzelm
parents: 6859
diff changeset
    44
    Position.T -> (Symbol.symbol, 'a) Source.source ->
7682
46de8064c93c added Space, Comment token kinds (keep actual text);
wenzelm
parents: 7477
diff changeset
    45
    (token, Position.T * (Symbol.symbol, 'a) Source.source) Source.source
17164
a786e1a1ce02 added AltString token (delimited by ASCII back-quotes);
wenzelm
parents: 17069
diff changeset
    46
  val source_proper: (token, 'a) Source.source ->
a786e1a1ce02 added AltString token (delimited by ASCII back-quotes);
wenzelm
parents: 17069
diff changeset
    47
    (token, (token, 'a) Source.source) Source.source
5825
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
    48
end;
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
    49
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
    50
structure OuterLex: OUTER_LEX =
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
    51
struct
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
    52
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
    53
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
    54
(** tokens **)
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
    55
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
    56
(* datatype token *)
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
    57
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
    58
datatype token_kind =
23729
d1ba656978c5 separated Malformed (symbolic char) from Error (bad input);
wenzelm
parents: 23721
diff changeset
    59
  Command | Keyword | Ident | LongIdent | SymIdent | Var | TypeIdent | TypeVar | Nat |
23788
54ce229dc858 Symbol.not_eof/sync is superceded by Symbol.is_regular (rules out further control symbols);
wenzelm
parents: 23729
diff changeset
    60
  String | AltString | Verbatim | Space | Comment | Malformed | Error of string | Sync | EOF;
5825
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
    61
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
    62
datatype token = Token of Position.T * (token_kind * string);
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
    63
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
    64
val str_of_kind =
7026
69724548fad1 separate command tokens;
wenzelm
parents: 6859
diff changeset
    65
 fn Command => "command"
69724548fad1 separate command tokens;
wenzelm
parents: 6859
diff changeset
    66
  | Keyword => "keyword"
5825
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
    67
  | Ident => "identifier"
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
    68
  | LongIdent => "long identifier"
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
    69
  | SymIdent => "symbolic identifier"
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
    70
  | Var => "schematic variable"
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
    71
  | TypeIdent => "type variable"
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
    72
  | TypeVar => "schematic type variable"
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
    73
  | Nat => "number"
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
    74
  | String => "string"
17164
a786e1a1ce02 added AltString token (delimited by ASCII back-quotes);
wenzelm
parents: 17069
diff changeset
    75
  | AltString => "back-quoted string"
5825
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
    76
  | Verbatim => "verbatim text"
7682
46de8064c93c added Space, Comment token kinds (keep actual text);
wenzelm
parents: 7477
diff changeset
    77
  | Space => "white space"
46de8064c93c added Space, Comment token kinds (keep actual text);
wenzelm
parents: 7477
diff changeset
    78
  | Comment => "comment text"
23729
d1ba656978c5 separated Malformed (symbolic char) from Error (bad input);
wenzelm
parents: 23721
diff changeset
    79
  | Malformed => "malformed symbolic character"
d1ba656978c5 separated Malformed (symbolic char) from Error (bad input);
wenzelm
parents: 23721
diff changeset
    80
  | Error _ => "bad input"
23788
54ce229dc858 Symbol.not_eof/sync is superceded by Symbol.is_regular (rules out further control symbols);
wenzelm
parents: 23729
diff changeset
    81
  | Sync => "sync marker"
5825
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
    82
  | EOF => "end-of-file";
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
    83
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
    84
10748
74ed77fa5310 recover: malformed result;
wenzelm
parents: 9195
diff changeset
    85
(* control tokens *)
6859
2b3db2b6c129 sync token;
wenzelm
parents: 6743
diff changeset
    86
5825
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
    87
val eof = Token (Position.none, (EOF, ""));
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
    88
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
    89
fun is_eof (Token (_, (EOF, _))) = true
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
    90
  | is_eof _ = false;
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
    91
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
    92
val stopper = (eof, is_eof);
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
    93
val not_eof = not o is_eof;
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
    94
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
    95
23678
f5d315390edc Malformed token: error msg;
wenzelm
parents: 22873
diff changeset
    96
fun not_sync (Token (_, (Sync, _))) = false
f5d315390edc Malformed token: error msg;
wenzelm
parents: 22873
diff changeset
    97
  | not_sync _ = true;
f5d315390edc Malformed token: error msg;
wenzelm
parents: 22873
diff changeset
    98
f5d315390edc Malformed token: error msg;
wenzelm
parents: 22873
diff changeset
    99
5825
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   100
(* get position *)
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   101
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   102
fun position_of (Token (pos, _)) = pos;
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   103
val pos_of = Position.str_of o position_of;
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   104
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   105
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   106
(* kind of token *)
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   107
23721
aa088ef9237c added kind_of;
wenzelm
parents: 23682
diff changeset
   108
fun kind_of (Token (_, (k, _))) = k;
aa088ef9237c added kind_of;
wenzelm
parents: 23682
diff changeset
   109
5825
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   110
fun is_kind k (Token (_, (k', _))) = k = k';
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   111
7026
69724548fad1 separate command tokens;
wenzelm
parents: 6859
diff changeset
   112
fun keyword_with pred (Token (_, (Keyword, x))) = pred x
69724548fad1 separate command tokens;
wenzelm
parents: 6859
diff changeset
   113
  | keyword_with _ _ = false;
5825
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   114
16029
070ed43b86f8 added ident_with;
wenzelm
parents: 15531
diff changeset
   115
fun ident_with pred (Token (_, (Ident, x))) = pred x
070ed43b86f8 added ident_with;
wenzelm
parents: 15531
diff changeset
   116
  | ident_with _ _ = false;
070ed43b86f8 added ident_with;
wenzelm
parents: 15531
diff changeset
   117
7682
46de8064c93c added Space, Comment token kinds (keep actual text);
wenzelm
parents: 7477
diff changeset
   118
fun is_proper (Token (_, (Space, _))) = false
46de8064c93c added Space, Comment token kinds (keep actual text);
wenzelm
parents: 7477
diff changeset
   119
  | is_proper (Token (_, (Comment, _))) = false
5825
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   120
  | is_proper _ = true;
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   121
9195
29f1e53f9937 fixed is_semicolon (keyword instead of command!);
wenzelm
parents: 9155
diff changeset
   122
fun is_semicolon (Token (_, (Keyword, ";"))) = true
9130
ff8789b49d2e added !!!;
wenzelm
parents: 9051
diff changeset
   123
  | is_semicolon _ = false;
ff8789b49d2e added !!!;
wenzelm
parents: 9051
diff changeset
   124
17069
ee08b2466a09 clarify is_newline vs. is_blank;
wenzelm
parents: 16029
diff changeset
   125
fun is_comment (Token (_, (Comment, _))) = true
ee08b2466a09 clarify is_newline vs. is_blank;
wenzelm
parents: 16029
diff changeset
   126
  | is_comment _ = false;
ee08b2466a09 clarify is_newline vs. is_blank;
wenzelm
parents: 16029
diff changeset
   127
8580
e79ee31d3936 added is_begin/end_ignore;
wenzelm
parents: 8231
diff changeset
   128
fun is_begin_ignore (Token (_, (Comment, "<"))) = true
e79ee31d3936 added is_begin/end_ignore;
wenzelm
parents: 8231
diff changeset
   129
  | is_begin_ignore _ = false;
e79ee31d3936 added is_begin/end_ignore;
wenzelm
parents: 8231
diff changeset
   130
e79ee31d3936 added is_begin/end_ignore;
wenzelm
parents: 8231
diff changeset
   131
fun is_end_ignore (Token (_, (Comment, ">"))) = true
e79ee31d3936 added is_begin/end_ignore;
wenzelm
parents: 8231
diff changeset
   132
  | is_end_ignore _ = false;
e79ee31d3936 added is_begin/end_ignore;
wenzelm
parents: 8231
diff changeset
   133
8651
f095f3b8181a added is_newline;
wenzelm
parents: 8580
diff changeset
   134
17069
ee08b2466a09 clarify is_newline vs. is_blank;
wenzelm
parents: 16029
diff changeset
   135
(* blanks and newlines -- space tokens obey lines *)
8651
f095f3b8181a added is_newline;
wenzelm
parents: 8580
diff changeset
   136
23678
f5d315390edc Malformed token: error msg;
wenzelm
parents: 22873
diff changeset
   137
fun is_blank (Token (_, (Space, x))) = not (String.isSuffix "\n" x)
17069
ee08b2466a09 clarify is_newline vs. is_blank;
wenzelm
parents: 16029
diff changeset
   138
  | is_blank _ = false;
ee08b2466a09 clarify is_newline vs. is_blank;
wenzelm
parents: 16029
diff changeset
   139
23678
f5d315390edc Malformed token: error msg;
wenzelm
parents: 22873
diff changeset
   140
fun is_newline (Token (_, (Space, x))) = String.isSuffix "\n" x
8651
f095f3b8181a added is_newline;
wenzelm
parents: 8580
diff changeset
   141
  | is_newline _ = false;
f095f3b8181a added is_newline;
wenzelm
parents: 8580
diff changeset
   142
5825
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   143
14991
26fb63c4acb5 added unparse;
wenzelm
parents: 14981
diff changeset
   144
(* token content *)
9155
adfa40218e06 OuterLex.name_of: include val;
wenzelm
parents: 9130
diff changeset
   145
18547
d1978038b945 unparse String/AltString: escape quotes;
wenzelm
parents: 17164
diff changeset
   146
fun escape q =
d1978038b945 unparse String/AltString: escape quotes;
wenzelm
parents: 17164
diff changeset
   147
  implode o map (fn s => if s = q orelse s = "\\" then "\\" ^ s else s) o Symbol.explode;
d1978038b945 unparse String/AltString: escape quotes;
wenzelm
parents: 17164
diff changeset
   148
14991
26fb63c4acb5 added unparse;
wenzelm
parents: 14981
diff changeset
   149
fun unparse (Token (_, (kind, x))) =
26fb63c4acb5 added unparse;
wenzelm
parents: 14981
diff changeset
   150
  (case kind of
18547
d1978038b945 unparse String/AltString: escape quotes;
wenzelm
parents: 17164
diff changeset
   151
    String => x |> quote o escape "\""
d1978038b945 unparse String/AltString: escape quotes;
wenzelm
parents: 17164
diff changeset
   152
  | AltString => x |> enclose "`" "`" o escape "`"
14991
26fb63c4acb5 added unparse;
wenzelm
parents: 14981
diff changeset
   153
  | Verbatim => x |> enclose "{*" "*}"
26fb63c4acb5 added unparse;
wenzelm
parents: 14981
diff changeset
   154
  | Comment => x |> enclose "(*" "*)"
23788
54ce229dc858 Symbol.not_eof/sync is superceded by Symbol.is_regular (rules out further control symbols);
wenzelm
parents: 23729
diff changeset
   155
  | Malformed => Output.escape_malformed x
23729
d1ba656978c5 separated Malformed (symbolic char) from Error (bad input);
wenzelm
parents: 23721
diff changeset
   156
  | Sync => ""
d1ba656978c5 separated Malformed (symbolic char) from Error (bad input);
wenzelm
parents: 23721
diff changeset
   157
  | EOF => ""
14991
26fb63c4acb5 added unparse;
wenzelm
parents: 14981
diff changeset
   158
  | _ => x);
26fb63c4acb5 added unparse;
wenzelm
parents: 14981
diff changeset
   159
23788
54ce229dc858 Symbol.not_eof/sync is superceded by Symbol.is_regular (rules out further control symbols);
wenzelm
parents: 23729
diff changeset
   160
fun text_of tok =
54ce229dc858 Symbol.not_eof/sync is superceded by Symbol.is_regular (rules out further control symbols);
wenzelm
parents: 23729
diff changeset
   161
  if is_semicolon tok then ("terminator", "")
23729
d1ba656978c5 separated Malformed (symbolic char) from Error (bad input);
wenzelm
parents: 23721
diff changeset
   162
  else
23788
54ce229dc858 Symbol.not_eof/sync is superceded by Symbol.is_regular (rules out further control symbols);
wenzelm
parents: 23729
diff changeset
   163
    let
54ce229dc858 Symbol.not_eof/sync is superceded by Symbol.is_regular (rules out further control symbols);
wenzelm
parents: 23729
diff changeset
   164
      val k = str_of_kind (kind_of tok);
25582
655453e635c4 text_of: make double sure that result is well-formed, to avoid recurrent failures;
wenzelm
parents: 25579
diff changeset
   165
      val txt = unparse tok;
655453e635c4 text_of: make double sure that result is well-formed, to avoid recurrent failures;
wenzelm
parents: 25579
diff changeset
   166
      val s =
655453e635c4 text_of: make double sure that result is well-formed, to avoid recurrent failures;
wenzelm
parents: 25579
diff changeset
   167
        if can Symbol.explode txt
655453e635c4 text_of: make double sure that result is well-formed, to avoid recurrent failures;
wenzelm
parents: 25579
diff changeset
   168
        then txt else Output.escape_malformed txt;
23788
54ce229dc858 Symbol.not_eof/sync is superceded by Symbol.is_regular (rules out further control symbols);
wenzelm
parents: 23729
diff changeset
   169
    in
54ce229dc858 Symbol.not_eof/sync is superceded by Symbol.is_regular (rules out further control symbols);
wenzelm
parents: 23729
diff changeset
   170
      if s = "" then (k, "")
54ce229dc858 Symbol.not_eof/sync is superceded by Symbol.is_regular (rules out further control symbols);
wenzelm
parents: 23729
diff changeset
   171
      else if size s < 40 andalso not (exists_string (fn c => c = "\n") s) then (k ^ " " ^ s, "")
54ce229dc858 Symbol.not_eof/sync is superceded by Symbol.is_regular (rules out further control symbols);
wenzelm
parents: 23729
diff changeset
   172
      else (k, s)
54ce229dc858 Symbol.not_eof/sync is superceded by Symbol.is_regular (rules out further control symbols);
wenzelm
parents: 23729
diff changeset
   173
    end;
23729
d1ba656978c5 separated Malformed (symbolic char) from Error (bad input);
wenzelm
parents: 23721
diff changeset
   174
5825
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   175
fun val_of (Token (_, (_, x))) = x;
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   176
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   177
fun token_leq (Token (_, (_, x)), Token (_, (_, x'))) = x <= x';
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   178
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   179
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   180
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   181
(** scanners **)
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   182
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   183
fun change_prompt scan = Scan.prompt "# " scan;
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   184
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   185
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   186
(* diagnostics *)
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   187
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   188
fun lex_err msg ((pos, cs), _) = "Outer lexical error" ^ Position.str_of pos ^ ": " ^ msg cs;
9130
ff8789b49d2e added !!!;
wenzelm
parents: 9051
diff changeset
   189
fun !!! msg scan = Scan.!! (lex_err (K msg)) scan;
5825
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   190
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   191
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   192
(* line numbering *)
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   193
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   194
fun incr_line scan = Scan.depend (fn pos => scan >> pair (Position.inc pos));
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   195
val keep_line = Scan.lift;
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   196
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   197
val scan_blank =
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   198
  incr_line ($$ "\n") ||
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   199
  keep_line (Scan.one Symbol.is_blank);
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   200
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   201
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   202
(* scan symbolic idents *)
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   203
20664
ffbc5a57191a member (op =);
wenzelm
parents: 20112
diff changeset
   204
val is_sym_char = member (op =) (explode "!#$%&*+-/<=>?@^_|~");
5825
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   205
8231
fa93309ff27e symid: include single symbolic char;
wenzelm
parents: 7902
diff changeset
   206
val scan_symid =
21858
05f57309170c avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents: 20982
diff changeset
   207
  Scan.many1 is_sym_char >> implode ||
8231
fa93309ff27e symid: include single symbolic char;
wenzelm
parents: 7902
diff changeset
   208
  Scan.one Symbol.is_symbolic;
5825
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   209
8231
fa93309ff27e symid: include single symbolic char;
wenzelm
parents: 7902
diff changeset
   210
fun is_symid str =
fa93309ff27e symid: include single symbolic char;
wenzelm
parents: 7902
diff changeset
   211
  (case try Symbol.explode str of
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15224
diff changeset
   212
    SOME [s] => Symbol.is_symbolic s orelse is_sym_char s
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15224
diff changeset
   213
  | SOME ss => forall is_sym_char ss
8231
fa93309ff27e symid: include single symbolic char;
wenzelm
parents: 7902
diff changeset
   214
  | _ => false);
fa93309ff27e symid: include single symbolic char;
wenzelm
parents: 7902
diff changeset
   215
20982
fade54fde622 is_sid: disallow 'begin' keyword as identifier;
wenzelm
parents: 20664
diff changeset
   216
fun is_sid "begin" = false
fade54fde622 is_sid: disallow 'begin' keyword as identifier;
wenzelm
parents: 20664
diff changeset
   217
  | is_sid ":" = true
22873
decd2ff5f503 is_sid: include '::';
wenzelm
parents: 21966
diff changeset
   218
  | is_sid "::" = true
20982
fade54fde622 is_sid: disallow 'begin' keyword as identifier;
wenzelm
parents: 20664
diff changeset
   219
  | is_sid s = is_symid s orelse Syntax.is_identifier s;
5825
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   220
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   221
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   222
(* scan strings *)
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   223
17164
a786e1a1ce02 added AltString token (delimited by ASCII back-quotes);
wenzelm
parents: 17069
diff changeset
   224
local
a786e1a1ce02 added AltString token (delimited by ASCII back-quotes);
wenzelm
parents: 17069
diff changeset
   225
25579
22869d9d545b (alt)string: allow explicit character codes (as in ML);
wenzelm
parents: 24577
diff changeset
   226
val char_code =
22869d9d545b (alt)string: allow explicit character codes (as in ML);
wenzelm
parents: 24577
diff changeset
   227
  Scan.one Symbol.is_ascii_digit --
22869d9d545b (alt)string: allow explicit character codes (as in ML);
wenzelm
parents: 24577
diff changeset
   228
  Scan.one Symbol.is_ascii_digit --
22869d9d545b (alt)string: allow explicit character codes (as in ML);
wenzelm
parents: 24577
diff changeset
   229
  Scan.one Symbol.is_ascii_digit :|-- (fn ((a, b), c) =>
22869d9d545b (alt)string: allow explicit character codes (as in ML);
wenzelm
parents: 24577
diff changeset
   230
    let val (n, _) = Library.read_int [a, b, c]
22869d9d545b (alt)string: allow explicit character codes (as in ML);
wenzelm
parents: 24577
diff changeset
   231
    in if n <= 255 then Scan.succeed (chr n) else Scan.fail end);
22869d9d545b (alt)string: allow explicit character codes (as in ML);
wenzelm
parents: 24577
diff changeset
   232
17164
a786e1a1ce02 added AltString token (delimited by ASCII back-quotes);
wenzelm
parents: 17069
diff changeset
   233
fun scan_str q =
7682
46de8064c93c added Space, Comment token kinds (keep actual text);
wenzelm
parents: 7477
diff changeset
   234
  scan_blank ||
9130
ff8789b49d2e added !!!;
wenzelm
parents: 9051
diff changeset
   235
  keep_line ($$ "\\") |-- !!! "bad escape character in string"
25579
22869d9d545b (alt)string: allow explicit character codes (as in ML);
wenzelm
parents: 24577
diff changeset
   236
      (scan_blank || keep_line ($$ q || $$ "\\" || char_code)) ||
23788
54ce229dc858 Symbol.not_eof/sync is superceded by Symbol.is_regular (rules out further control symbols);
wenzelm
parents: 23729
diff changeset
   237
  keep_line (Scan.one (fn s => s <> q andalso s <> "\\" andalso Symbol.is_regular s));
5825
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   238
17164
a786e1a1ce02 added AltString token (delimited by ASCII back-quotes);
wenzelm
parents: 17069
diff changeset
   239
fun scan_strs q =
a786e1a1ce02 added AltString token (delimited by ASCII back-quotes);
wenzelm
parents: 17069
diff changeset
   240
  keep_line ($$ q) |--
9130
ff8789b49d2e added !!!;
wenzelm
parents: 9051
diff changeset
   241
    !!! "missing quote at end of string"
17164
a786e1a1ce02 added AltString token (delimited by ASCII back-quotes);
wenzelm
parents: 17069
diff changeset
   242
      (change_prompt ((Scan.repeat (scan_str q) >> implode) --| keep_line ($$ q)));
a786e1a1ce02 added AltString token (delimited by ASCII back-quotes);
wenzelm
parents: 17069
diff changeset
   243
a786e1a1ce02 added AltString token (delimited by ASCII back-quotes);
wenzelm
parents: 17069
diff changeset
   244
in
a786e1a1ce02 added AltString token (delimited by ASCII back-quotes);
wenzelm
parents: 17069
diff changeset
   245
a786e1a1ce02 added AltString token (delimited by ASCII back-quotes);
wenzelm
parents: 17069
diff changeset
   246
val scan_string = scan_strs "\"";
a786e1a1ce02 added AltString token (delimited by ASCII back-quotes);
wenzelm
parents: 17069
diff changeset
   247
val scan_alt_string = scan_strs "`";
a786e1a1ce02 added AltString token (delimited by ASCII back-quotes);
wenzelm
parents: 17069
diff changeset
   248
a786e1a1ce02 added AltString token (delimited by ASCII back-quotes);
wenzelm
parents: 17069
diff changeset
   249
end;
5825
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   250
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   251
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   252
(* scan verbatim text *)
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   253
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   254
val scan_verb =
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   255
  scan_blank ||
19305
5c16895d548b avoid polymorphic equality;
wenzelm
parents: 18547
diff changeset
   256
  keep_line ($$ "*" --| Scan.ahead (~$$ "}")) ||
23788
54ce229dc858 Symbol.not_eof/sync is superceded by Symbol.is_regular (rules out further control symbols);
wenzelm
parents: 23729
diff changeset
   257
  keep_line (Scan.one (fn s => s <> "*" andalso Symbol.is_regular s));
5825
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   258
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   259
val scan_verbatim =
6743
5d50225637c8 changed {| |} verbatim syntax to {* *} in order to simplify ProofGeneral setup;
wenzelm
parents: 5876
diff changeset
   260
  keep_line ($$ "{" -- $$ "*") |--
9130
ff8789b49d2e added !!!;
wenzelm
parents: 9051
diff changeset
   261
    !!! "missing end of verbatim text"
6743
5d50225637c8 changed {| |} verbatim syntax to {* *} in order to simplify ProofGeneral setup;
wenzelm
parents: 5876
diff changeset
   262
      (change_prompt ((Scan.repeat scan_verb >> implode) --| keep_line ($$ "*" -- $$ "}")));
5825
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   263
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   264
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   265
(* scan space *)
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   266
19305
5c16895d548b avoid polymorphic equality;
wenzelm
parents: 18547
diff changeset
   267
fun is_space s = Symbol.is_blank s andalso s <> "\n";
5825
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   268
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   269
val scan_space =
21858
05f57309170c avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents: 20982
diff changeset
   270
  (keep_line (Scan.many1 is_space) -- Scan.optional (incr_line ($$ "\n")) "" ||
05f57309170c avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents: 20982
diff changeset
   271
    keep_line (Scan.many is_space) -- incr_line ($$ "\n")) >> (fn (cs, c) => implode cs ^ c);
5825
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   272
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   273
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   274
(* scan nested comments *)
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   275
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   276
val scan_cmt =
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   277
  Scan.lift scan_blank ||
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   278
  Scan.depend (fn d => keep_line ($$ "(" ^^ $$ "*") >> pair (d + 1)) ||
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   279
  Scan.depend (fn 0 => Scan.fail | d => keep_line ($$ "*" ^^ $$ ")") >> pair (d - 1)) ||
19305
5c16895d548b avoid polymorphic equality;
wenzelm
parents: 18547
diff changeset
   280
  Scan.lift (keep_line ($$ "*" --| Scan.ahead (~$$ ")"))) ||
23788
54ce229dc858 Symbol.not_eof/sync is superceded by Symbol.is_regular (rules out further control symbols);
wenzelm
parents: 23729
diff changeset
   281
  Scan.lift (keep_line (Scan.one (fn s => s <> "*" andalso Symbol.is_regular s)));
5825
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   282
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   283
val scan_comment =
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   284
  keep_line ($$ "(" -- $$ "*") |--
9130
ff8789b49d2e added !!!;
wenzelm
parents: 9051
diff changeset
   285
    !!! "missing end of comment"
5825
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   286
      (change_prompt
7682
46de8064c93c added Space, Comment token kinds (keep actual text);
wenzelm
parents: 7477
diff changeset
   287
        (Scan.pass 0 (Scan.repeat scan_cmt >> implode) --| keep_line ($$ "*" -- $$ ")")));
5825
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   288
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   289
23678
f5d315390edc Malformed token: error msg;
wenzelm
parents: 22873
diff changeset
   290
(* scan malformed symbols *)
f5d315390edc Malformed token: error msg;
wenzelm
parents: 22873
diff changeset
   291
f5d315390edc Malformed token: error msg;
wenzelm
parents: 22873
diff changeset
   292
local
f5d315390edc Malformed token: error msg;
wenzelm
parents: 22873
diff changeset
   293
f5d315390edc Malformed token: error msg;
wenzelm
parents: 22873
diff changeset
   294
val scan_mal =
f5d315390edc Malformed token: error msg;
wenzelm
parents: 22873
diff changeset
   295
  scan_blank ||
23788
54ce229dc858 Symbol.not_eof/sync is superceded by Symbol.is_regular (rules out further control symbols);
wenzelm
parents: 23729
diff changeset
   296
  keep_line (Scan.one Symbol.is_regular);
23678
f5d315390edc Malformed token: error msg;
wenzelm
parents: 22873
diff changeset
   297
f5d315390edc Malformed token: error msg;
wenzelm
parents: 22873
diff changeset
   298
in
f5d315390edc Malformed token: error msg;
wenzelm
parents: 22873
diff changeset
   299
f5d315390edc Malformed token: error msg;
wenzelm
parents: 22873
diff changeset
   300
val scan_malformed =
f5d315390edc Malformed token: error msg;
wenzelm
parents: 22873
diff changeset
   301
  keep_line ($$ Symbol.malformed) |--
23729
d1ba656978c5 separated Malformed (symbolic char) from Error (bad input);
wenzelm
parents: 23721
diff changeset
   302
    change_prompt (Scan.repeat scan_mal >> implode)
23678
f5d315390edc Malformed token: error msg;
wenzelm
parents: 22873
diff changeset
   303
      --| keep_line (Scan.option ($$ Symbol.end_malformed));
f5d315390edc Malformed token: error msg;
wenzelm
parents: 22873
diff changeset
   304
f5d315390edc Malformed token: error msg;
wenzelm
parents: 22873
diff changeset
   305
end;
f5d315390edc Malformed token: error msg;
wenzelm
parents: 22873
diff changeset
   306
f5d315390edc Malformed token: error msg;
wenzelm
parents: 22873
diff changeset
   307
5825
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   308
(* scan token *)
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   309
9130
ff8789b49d2e added !!!;
wenzelm
parents: 9051
diff changeset
   310
fun scan (lex1, lex2) =
5825
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   311
  let
24022
wenzelm
parents: 23788
diff changeset
   312
    val scanner = Scan.state :|-- (fn pos =>
9130
ff8789b49d2e added !!!;
wenzelm
parents: 9051
diff changeset
   313
      let
ff8789b49d2e added !!!;
wenzelm
parents: 9051
diff changeset
   314
        fun token k x = Token (pos, (k, x));
ff8789b49d2e added !!!;
wenzelm
parents: 9051
diff changeset
   315
        fun sync _ = token Sync Symbol.sync;
ff8789b49d2e added !!!;
wenzelm
parents: 9051
diff changeset
   316
      in
ff8789b49d2e added !!!;
wenzelm
parents: 9051
diff changeset
   317
        scan_string >> token String ||
17164
a786e1a1ce02 added AltString token (delimited by ASCII back-quotes);
wenzelm
parents: 17069
diff changeset
   318
        scan_alt_string >> token AltString ||
9130
ff8789b49d2e added !!!;
wenzelm
parents: 9051
diff changeset
   319
        scan_verbatim >> token Verbatim ||
ff8789b49d2e added !!!;
wenzelm
parents: 9051
diff changeset
   320
        scan_space >> token Space ||
ff8789b49d2e added !!!;
wenzelm
parents: 9051
diff changeset
   321
        scan_comment >> token Comment ||
23729
d1ba656978c5 separated Malformed (symbolic char) from Error (bad input);
wenzelm
parents: 23721
diff changeset
   322
        scan_malformed >> token Malformed ||
9130
ff8789b49d2e added !!!;
wenzelm
parents: 9051
diff changeset
   323
        keep_line (Scan.one Symbol.is_sync >> sync) ||
ff8789b49d2e added !!!;
wenzelm
parents: 9051
diff changeset
   324
        keep_line (Scan.max token_leq
ff8789b49d2e added !!!;
wenzelm
parents: 9051
diff changeset
   325
          (Scan.max token_leq
ff8789b49d2e added !!!;
wenzelm
parents: 9051
diff changeset
   326
            (Scan.literal lex1 >> (token Keyword o implode))
ff8789b49d2e added !!!;
wenzelm
parents: 9051
diff changeset
   327
            (Scan.literal lex2 >> (token Command o implode)))
ff8789b49d2e added !!!;
wenzelm
parents: 9051
diff changeset
   328
          (Syntax.scan_longid >> token LongIdent ||
ff8789b49d2e added !!!;
wenzelm
parents: 9051
diff changeset
   329
            Syntax.scan_id >> token Ident ||
ff8789b49d2e added !!!;
wenzelm
parents: 9051
diff changeset
   330
            Syntax.scan_var >> token Var ||
ff8789b49d2e added !!!;
wenzelm
parents: 9051
diff changeset
   331
            Syntax.scan_tid >> token TypeIdent ||
ff8789b49d2e added !!!;
wenzelm
parents: 9051
diff changeset
   332
            Syntax.scan_tvar >> token TypeVar ||
ff8789b49d2e added !!!;
wenzelm
parents: 9051
diff changeset
   333
            Syntax.scan_nat >> token Nat ||
ff8789b49d2e added !!!;
wenzelm
parents: 9051
diff changeset
   334
            scan_symid >> token SymIdent))
24022
wenzelm
parents: 23788
diff changeset
   335
      end);
14729
0e987111a17e changed Symbol.beginning;
wenzelm
parents: 10748
diff changeset
   336
  in !! (lex_err (fn cs => "bad input " ^ quote (Symbol.beginning 10 cs))) scanner end;
5825
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   337
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   338
9130
ff8789b49d2e added !!!;
wenzelm
parents: 9051
diff changeset
   339
(* token sources *)
5825
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   340
23678
f5d315390edc Malformed token: error msg;
wenzelm
parents: 22873
diff changeset
   341
local
f5d315390edc Malformed token: error msg;
wenzelm
parents: 22873
diff changeset
   342
23788
54ce229dc858 Symbol.not_eof/sync is superceded by Symbol.is_regular (rules out further control symbols);
wenzelm
parents: 23729
diff changeset
   343
val is_junk = (not o Symbol.is_blank) andf Symbol.is_regular;
23678
f5d315390edc Malformed token: error msg;
wenzelm
parents: 22873
diff changeset
   344
24022
wenzelm
parents: 23788
diff changeset
   345
fun recover msg = Scan.state :|-- (fn pos =>
wenzelm
parents: 23788
diff changeset
   346
  keep_line (Scan.many is_junk) >> (fn xs => [Token (pos, (Error msg, implode xs))]));
23678
f5d315390edc Malformed token: error msg;
wenzelm
parents: 22873
diff changeset
   347
f5d315390edc Malformed token: error msg;
wenzelm
parents: 22873
diff changeset
   348
in
5825
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   349
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   350
fun source do_recover get_lex pos src =
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   351
  Source.source' pos Symbol.stopper (Scan.bulk (fn xs => scan (get_lex ()) xs))
23682
cf4773532006 nested source: explicit interactive flag for recover avoids duplicate errors;
wenzelm
parents: 23678
diff changeset
   352
    (Option.map (rpair recover) do_recover) src;
23678
f5d315390edc Malformed token: error msg;
wenzelm
parents: 22873
diff changeset
   353
f5d315390edc Malformed token: error msg;
wenzelm
parents: 22873
diff changeset
   354
end;
5825
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   355
9130
ff8789b49d2e added !!!;
wenzelm
parents: 9051
diff changeset
   356
fun source_proper src = src |> Source.filter is_proper;
ff8789b49d2e added !!!;
wenzelm
parents: 9051
diff changeset
   357
ff8789b49d2e added !!!;
wenzelm
parents: 9051
diff changeset
   358
5825
24e4b1780d33 Outer lexical syntax for Isabelle/Isar.
wenzelm
parents:
diff changeset
   359
end;