src/Pure/ML/ml_lex.ML
author wenzelm
Fri, 20 Mar 2009 20:22:13 +0100
changeset 30614 845bcfd3e9cd
parent 30600 de241396389c
child 30636 bd8813d7774d
permissions -rw-r--r--
report markup for ML tokens;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
24579
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/ML/ml_lex.ML
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
     3
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
     4
Lexical syntax for SML.
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
     5
*)
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
     6
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
     7
signature ML_LEX =
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
     8
sig
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
     9
  datatype token_kind =
24596
f1333a841b26 removed obsolete Selector token;
wenzelm
parents: 24579
diff changeset
    10
    Keyword | Ident | LongIdent | TypeVar | Word | Int | Real | Char | String |
24579
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
    11
    Space | Comment | Error of string | EOF
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
    12
  eqtype token
27732
8dbf5761a24a abstract type Scan.stopper;
wenzelm
parents: 24596
diff changeset
    13
  val stopper: token Scan.stopper
24596
f1333a841b26 removed obsolete Selector token;
wenzelm
parents: 24579
diff changeset
    14
  val is_regular: token -> bool
f1333a841b26 removed obsolete Selector token;
wenzelm
parents: 24579
diff changeset
    15
  val is_improper: token -> bool
f1333a841b26 removed obsolete Selector token;
wenzelm
parents: 24579
diff changeset
    16
  val pos_of: token -> string
24579
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
    17
  val kind_of: token -> token_kind
27817
78cae5cca09e renamed ML_Lex.val_of to content_of;
wenzelm
parents: 27799
diff changeset
    18
  val content_of: token -> string
30614
845bcfd3e9cd report markup for ML tokens;
wenzelm
parents: 30600
diff changeset
    19
  val markup_of: token -> Markup.T
845bcfd3e9cd report markup for ML tokens;
wenzelm
parents: 30600
diff changeset
    20
  val report_token: token -> unit
24579
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
    21
  val keywords: string list
30593
495672058d97 added scan_antiq;
wenzelm
parents: 30591
diff changeset
    22
  val scan_antiq: Symbol_Pos.T list -> token Antiquote.antiquote * Symbol_Pos.T list
24596
f1333a841b26 removed obsolete Selector token;
wenzelm
parents: 24579
diff changeset
    23
  val source: (Symbol.symbol, 'a) Source.source ->
30573
49899f26fbd1 de-camelized Symbol_Pos;
wenzelm
parents: 29606
diff changeset
    24
    (token, (Symbol_Pos.T, Position.T * (Symbol.symbol, 'a) Source.source)
27772
b933c997eab3 improved position handling due to SymbolPos.T;
wenzelm
parents: 27732
diff changeset
    25
      Source.source) Source.source
30591
6c9c00ea4ae6 added tokenize;
wenzelm
parents: 30573
diff changeset
    26
  val tokenize: string -> token list
24579
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
    27
end;
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
    28
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
    29
structure ML_Lex: ML_LEX =
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
    30
struct
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
    31
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
    32
(** tokens **)
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
    33
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
    34
(* datatype token *)
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
    35
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
    36
datatype token_kind =
24596
f1333a841b26 removed obsolete Selector token;
wenzelm
parents: 24579
diff changeset
    37
  Keyword | Ident | LongIdent | TypeVar | Word | Int | Real | Char | String |
24579
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
    38
  Space | Comment | Error of string | EOF;
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
    39
27772
b933c997eab3 improved position handling due to SymbolPos.T;
wenzelm
parents: 27732
diff changeset
    40
datatype token = Token of Position.range * (token_kind * string);
b933c997eab3 improved position handling due to SymbolPos.T;
wenzelm
parents: 27732
diff changeset
    41
b933c997eab3 improved position handling due to SymbolPos.T;
wenzelm
parents: 27732
diff changeset
    42
b933c997eab3 improved position handling due to SymbolPos.T;
wenzelm
parents: 27732
diff changeset
    43
(* position *)
b933c997eab3 improved position handling due to SymbolPos.T;
wenzelm
parents: 27732
diff changeset
    44
b933c997eab3 improved position handling due to SymbolPos.T;
wenzelm
parents: 27732
diff changeset
    45
fun position_of (Token ((pos, _), _)) = pos;
b933c997eab3 improved position handling due to SymbolPos.T;
wenzelm
parents: 27732
diff changeset
    46
fun end_position_of (Token ((_, pos), _)) = pos;
b933c997eab3 improved position handling due to SymbolPos.T;
wenzelm
parents: 27732
diff changeset
    47
b933c997eab3 improved position handling due to SymbolPos.T;
wenzelm
parents: 27732
diff changeset
    48
val pos_of = Position.str_of o position_of;
24579
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
    49
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
    50
24596
f1333a841b26 removed obsolete Selector token;
wenzelm
parents: 24579
diff changeset
    51
(* control tokens *)
24579
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
    52
27772
b933c997eab3 improved position handling due to SymbolPos.T;
wenzelm
parents: 27732
diff changeset
    53
fun mk_eof pos = Token ((pos, Position.none), (EOF, ""));
b933c997eab3 improved position handling due to SymbolPos.T;
wenzelm
parents: 27732
diff changeset
    54
val eof = mk_eof Position.none;
24579
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
    55
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
    56
fun is_eof (Token (_, (EOF, _))) = true
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
    57
  | is_eof _ = false;
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
    58
27772
b933c997eab3 improved position handling due to SymbolPos.T;
wenzelm
parents: 27732
diff changeset
    59
val stopper =
b933c997eab3 improved position handling due to SymbolPos.T;
wenzelm
parents: 27732
diff changeset
    60
  Scan.stopper (fn [] => eof | toks => mk_eof (end_position_of (List.last toks))) is_eof;
b933c997eab3 improved position handling due to SymbolPos.T;
wenzelm
parents: 27732
diff changeset
    61
24579
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
    62
27772
b933c997eab3 improved position handling due to SymbolPos.T;
wenzelm
parents: 27732
diff changeset
    63
(* token content *)
b933c997eab3 improved position handling due to SymbolPos.T;
wenzelm
parents: 27732
diff changeset
    64
27817
78cae5cca09e renamed ML_Lex.val_of to content_of;
wenzelm
parents: 27799
diff changeset
    65
fun content_of (Token (_, (_, x))) = x;
78cae5cca09e renamed ML_Lex.val_of to content_of;
wenzelm
parents: 27799
diff changeset
    66
fun token_leq (tok, tok') = content_of tok <= content_of tok';
27772
b933c997eab3 improved position handling due to SymbolPos.T;
wenzelm
parents: 27732
diff changeset
    67
b933c997eab3 improved position handling due to SymbolPos.T;
wenzelm
parents: 27732
diff changeset
    68
fun kind_of (Token (_, (k, _))) = k;
24579
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
    69
24596
f1333a841b26 removed obsolete Selector token;
wenzelm
parents: 24579
diff changeset
    70
fun is_regular (Token (_, (Error _, _))) = false
f1333a841b26 removed obsolete Selector token;
wenzelm
parents: 24579
diff changeset
    71
  | is_regular (Token (_, (EOF, _))) = false
f1333a841b26 removed obsolete Selector token;
wenzelm
parents: 24579
diff changeset
    72
  | is_regular _ = true;
f1333a841b26 removed obsolete Selector token;
wenzelm
parents: 24579
diff changeset
    73
f1333a841b26 removed obsolete Selector token;
wenzelm
parents: 24579
diff changeset
    74
fun is_improper (Token (_, (Space, _))) = true
f1333a841b26 removed obsolete Selector token;
wenzelm
parents: 24579
diff changeset
    75
  | is_improper (Token (_, (Comment, _))) = true
f1333a841b26 removed obsolete Selector token;
wenzelm
parents: 24579
diff changeset
    76
  | is_improper _ = false;
f1333a841b26 removed obsolete Selector token;
wenzelm
parents: 24579
diff changeset
    77
f1333a841b26 removed obsolete Selector token;
wenzelm
parents: 24579
diff changeset
    78
30614
845bcfd3e9cd report markup for ML tokens;
wenzelm
parents: 30600
diff changeset
    79
(* markup *)
845bcfd3e9cd report markup for ML tokens;
wenzelm
parents: 30600
diff changeset
    80
845bcfd3e9cd report markup for ML tokens;
wenzelm
parents: 30600
diff changeset
    81
val markup_of = kind_of #>
845bcfd3e9cd report markup for ML tokens;
wenzelm
parents: 30600
diff changeset
    82
  (fn Keyword   => Markup.ML_keyword
845bcfd3e9cd report markup for ML tokens;
wenzelm
parents: 30600
diff changeset
    83
    | Ident     => Markup.ML_ident
845bcfd3e9cd report markup for ML tokens;
wenzelm
parents: 30600
diff changeset
    84
    | LongIdent => Markup.ML_ident
845bcfd3e9cd report markup for ML tokens;
wenzelm
parents: 30600
diff changeset
    85
    | TypeVar   => Markup.ML_tvar
845bcfd3e9cd report markup for ML tokens;
wenzelm
parents: 30600
diff changeset
    86
    | Word      => Markup.ML_numeral
845bcfd3e9cd report markup for ML tokens;
wenzelm
parents: 30600
diff changeset
    87
    | Int       => Markup.ML_numeral
845bcfd3e9cd report markup for ML tokens;
wenzelm
parents: 30600
diff changeset
    88
    | Real      => Markup.ML_numeral
845bcfd3e9cd report markup for ML tokens;
wenzelm
parents: 30600
diff changeset
    89
    | Char      => Markup.ML_char
845bcfd3e9cd report markup for ML tokens;
wenzelm
parents: 30600
diff changeset
    90
    | String    => Markup.ML_string
845bcfd3e9cd report markup for ML tokens;
wenzelm
parents: 30600
diff changeset
    91
    | Space     => Markup.none
845bcfd3e9cd report markup for ML tokens;
wenzelm
parents: 30600
diff changeset
    92
    | Comment   => Markup.ML_comment
845bcfd3e9cd report markup for ML tokens;
wenzelm
parents: 30600
diff changeset
    93
    | Error _   => Markup.ML_malformed
845bcfd3e9cd report markup for ML tokens;
wenzelm
parents: 30600
diff changeset
    94
    | EOF       => Markup.none);
845bcfd3e9cd report markup for ML tokens;
wenzelm
parents: 30600
diff changeset
    95
845bcfd3e9cd report markup for ML tokens;
wenzelm
parents: 30600
diff changeset
    96
fun report_token tok = Position.report (markup_of tok) (position_of tok);
845bcfd3e9cd report markup for ML tokens;
wenzelm
parents: 30600
diff changeset
    97
845bcfd3e9cd report markup for ML tokens;
wenzelm
parents: 30600
diff changeset
    98
24579
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
    99
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
   100
(** scanners **)
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
   101
30573
49899f26fbd1 de-camelized Symbol_Pos;
wenzelm
parents: 29606
diff changeset
   102
open Basic_Symbol_Pos;
24579
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
   103
30573
49899f26fbd1 de-camelized Symbol_Pos;
wenzelm
parents: 29606
diff changeset
   104
fun !!! msg = Symbol_Pos.!!! ("SML lexical error: " ^ msg);
24579
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
   105
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
   106
27772
b933c997eab3 improved position handling due to SymbolPos.T;
wenzelm
parents: 27732
diff changeset
   107
(* blanks *)
24579
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
   108
27772
b933c997eab3 improved position handling due to SymbolPos.T;
wenzelm
parents: 27732
diff changeset
   109
val scan_blank = Scan.one (Symbol.is_ascii_blank o symbol);
b933c997eab3 improved position handling due to SymbolPos.T;
wenzelm
parents: 27732
diff changeset
   110
val scan_blanks1 = Scan.repeat1 scan_blank;
24579
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
   111
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
   112
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
   113
(* keywords *)
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
   114
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
   115
val keywords = ["#", "(", ")", ",", "->", "...", ":", ":>", ";", "=",
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
   116
  "=>", "[", "]", "_", "{", "|", "}", "abstype", "and", "andalso", "as",
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
   117
  "case", "datatype", "do", "else", "end", "eqtype", "exception", "fn",
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
   118
  "fun", "functor", "handle", "if", "in", "include", "infix", "infixr",
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
   119
  "let", "local", "nonfix", "of", "op", "open", "orelse", "raise", "rec",
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
   120
  "sharing", "sig", "signature", "struct", "structure", "then", "type",
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
   121
  "val", "where", "while", "with", "withtype"];
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
   122
27772
b933c997eab3 improved position handling due to SymbolPos.T;
wenzelm
parents: 27732
diff changeset
   123
val lex = Scan.make_lexicon (map explode keywords);
b933c997eab3 improved position handling due to SymbolPos.T;
wenzelm
parents: 27732
diff changeset
   124
fun scan_keyword x = Scan.literal lex x;
24579
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
   125
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
   126
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
   127
(* identifiers *)
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
   128
24596
f1333a841b26 removed obsolete Selector token;
wenzelm
parents: 24579
diff changeset
   129
local
f1333a841b26 removed obsolete Selector token;
wenzelm
parents: 24579
diff changeset
   130
24579
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
   131
val scan_letdigs =
27772
b933c997eab3 improved position handling due to SymbolPos.T;
wenzelm
parents: 27732
diff changeset
   132
  Scan.many ((Symbol.is_ascii_letter orf Symbol.is_ascii_digit orf Symbol.is_ascii_quasi) o symbol);
24579
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
   133
27772
b933c997eab3 improved position handling due to SymbolPos.T;
wenzelm
parents: 27732
diff changeset
   134
val scan_alphanumeric = Scan.one (Symbol.is_ascii_letter o symbol) -- scan_letdigs >> op ::;
24579
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
   135
27772
b933c997eab3 improved position handling due to SymbolPos.T;
wenzelm
parents: 27732
diff changeset
   136
val scan_symbolic = Scan.many1 (member (op =) (explode "!#$%&*+-/:<=>?@\\^`|~") o symbol);
24579
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
   137
24596
f1333a841b26 removed obsolete Selector token;
wenzelm
parents: 24579
diff changeset
   138
in
f1333a841b26 removed obsolete Selector token;
wenzelm
parents: 24579
diff changeset
   139
24579
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
   140
val scan_ident = scan_alphanumeric || scan_symbolic;
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
   141
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
   142
val scan_longident =
27772
b933c997eab3 improved position handling due to SymbolPos.T;
wenzelm
parents: 27732
diff changeset
   143
  (Scan.repeat1 (scan_alphanumeric @@@ $$$ ".") >> flat) @@@ (scan_ident || $$$ "=");
24579
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
   144
27772
b933c997eab3 improved position handling due to SymbolPos.T;
wenzelm
parents: 27732
diff changeset
   145
val scan_typevar = $$$ "'" @@@ scan_letdigs;
24579
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
   146
24596
f1333a841b26 removed obsolete Selector token;
wenzelm
parents: 24579
diff changeset
   147
end;
24579
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
   148
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
   149
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
   150
(* numerals *)
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
   151
24596
f1333a841b26 removed obsolete Selector token;
wenzelm
parents: 24579
diff changeset
   152
local
f1333a841b26 removed obsolete Selector token;
wenzelm
parents: 24579
diff changeset
   153
27772
b933c997eab3 improved position handling due to SymbolPos.T;
wenzelm
parents: 27732
diff changeset
   154
val scan_dec = Scan.many1 (Symbol.is_ascii_digit o symbol);
b933c997eab3 improved position handling due to SymbolPos.T;
wenzelm
parents: 27732
diff changeset
   155
val scan_hex = Scan.many1 (Symbol.is_ascii_hex o symbol);
b933c997eab3 improved position handling due to SymbolPos.T;
wenzelm
parents: 27732
diff changeset
   156
val scan_sign = Scan.optional ($$$ "~") [];
b933c997eab3 improved position handling due to SymbolPos.T;
wenzelm
parents: 27732
diff changeset
   157
val scan_decint = scan_sign @@@ scan_dec;
24579
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
   158
24596
f1333a841b26 removed obsolete Selector token;
wenzelm
parents: 24579
diff changeset
   159
in
f1333a841b26 removed obsolete Selector token;
wenzelm
parents: 24579
diff changeset
   160
27772
b933c997eab3 improved position handling due to SymbolPos.T;
wenzelm
parents: 27732
diff changeset
   161
val scan_word =
b933c997eab3 improved position handling due to SymbolPos.T;
wenzelm
parents: 27732
diff changeset
   162
  $$$ "0" @@@ $$$ "w" @@@ $$$ "x" @@@ scan_hex ||
b933c997eab3 improved position handling due to SymbolPos.T;
wenzelm
parents: 27732
diff changeset
   163
  $$$ "0" @@@ $$$ "w" @@@ scan_dec;
24579
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
   164
27772
b933c997eab3 improved position handling due to SymbolPos.T;
wenzelm
parents: 27732
diff changeset
   165
val scan_int = scan_sign @@@ ($$$ "0" @@@ $$$ "x" @@@ scan_hex || scan_dec);
24579
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
   166
27772
b933c997eab3 improved position handling due to SymbolPos.T;
wenzelm
parents: 27732
diff changeset
   167
val scan_exp = ($$$ "E" || $$$ "e") @@@ scan_decint;
24579
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
   168
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
   169
val scan_real =
27772
b933c997eab3 improved position handling due to SymbolPos.T;
wenzelm
parents: 27732
diff changeset
   170
  scan_decint @@@ $$$ "." @@@ scan_dec @@@ Scan.optional scan_exp [] ||
b933c997eab3 improved position handling due to SymbolPos.T;
wenzelm
parents: 27732
diff changeset
   171
  scan_decint @@@ scan_exp;
24579
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
   172
24596
f1333a841b26 removed obsolete Selector token;
wenzelm
parents: 24579
diff changeset
   173
end;
f1333a841b26 removed obsolete Selector token;
wenzelm
parents: 24579
diff changeset
   174
24579
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
   175
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
   176
(* chars and strings *)
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
   177
24596
f1333a841b26 removed obsolete Selector token;
wenzelm
parents: 24579
diff changeset
   178
local
f1333a841b26 removed obsolete Selector token;
wenzelm
parents: 24579
diff changeset
   179
f1333a841b26 removed obsolete Selector token;
wenzelm
parents: 24579
diff changeset
   180
val scan_escape =
27772
b933c997eab3 improved position handling due to SymbolPos.T;
wenzelm
parents: 27732
diff changeset
   181
  Scan.one (member (op =) (explode "\"\\abtnvfr") o symbol) >> single ||
b933c997eab3 improved position handling due to SymbolPos.T;
wenzelm
parents: 27732
diff changeset
   182
  $$$ "^" @@@ (Scan.one (fn (s, _) => ord "@" <= ord s andalso ord s <= ord "_") >> single) ||
b933c997eab3 improved position handling due to SymbolPos.T;
wenzelm
parents: 27732
diff changeset
   183
  Scan.one (Symbol.is_ascii_digit o symbol) --
b933c997eab3 improved position handling due to SymbolPos.T;
wenzelm
parents: 27732
diff changeset
   184
    Scan.one (Symbol.is_ascii_digit o symbol) --
b933c997eab3 improved position handling due to SymbolPos.T;
wenzelm
parents: 27732
diff changeset
   185
    Scan.one (Symbol.is_ascii_digit o symbol) >> (fn ((a, b), c) => [a, b, c]);
24596
f1333a841b26 removed obsolete Selector token;
wenzelm
parents: 24579
diff changeset
   186
f1333a841b26 removed obsolete Selector token;
wenzelm
parents: 24579
diff changeset
   187
val scan_str =
30600
de241396389c allow non-printable symbols within string tokens;
wenzelm
parents: 30593
diff changeset
   188
  Scan.one (fn (s, _) => Symbol.is_regular s andalso s <> "\"" andalso s <> "\\" andalso
de241396389c allow non-printable symbols within string tokens;
wenzelm
parents: 30593
diff changeset
   189
    (not (Symbol.is_char s) orelse Symbol.is_printable s)) >> single ||
27772
b933c997eab3 improved position handling due to SymbolPos.T;
wenzelm
parents: 27732
diff changeset
   190
  $$$ "\\" @@@ !!! "bad escape character in string" scan_escape;
24596
f1333a841b26 removed obsolete Selector token;
wenzelm
parents: 24579
diff changeset
   191
27772
b933c997eab3 improved position handling due to SymbolPos.T;
wenzelm
parents: 27732
diff changeset
   192
val scan_gap = $$$ "\\" @@@ scan_blanks1 @@@ $$$ "\\";
b933c997eab3 improved position handling due to SymbolPos.T;
wenzelm
parents: 27732
diff changeset
   193
val scan_gaps = Scan.repeat scan_gap >> flat;
24579
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
   194
24596
f1333a841b26 removed obsolete Selector token;
wenzelm
parents: 24579
diff changeset
   195
in
24579
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
   196
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
   197
val scan_char =
27772
b933c997eab3 improved position handling due to SymbolPos.T;
wenzelm
parents: 27732
diff changeset
   198
  $$$ "#" @@@ $$$ "\"" @@@ scan_gaps @@@ scan_str @@@ scan_gaps @@@ $$$ "\"";
24579
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
   199
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
   200
val scan_string =
27772
b933c997eab3 improved position handling due to SymbolPos.T;
wenzelm
parents: 27732
diff changeset
   201
  $$$ "\"" @@@ !!! "missing quote at end of string"
b933c997eab3 improved position handling due to SymbolPos.T;
wenzelm
parents: 27732
diff changeset
   202
    ((Scan.repeat (scan_gap || scan_str) >> flat) @@@ $$$ "\"");
24596
f1333a841b26 removed obsolete Selector token;
wenzelm
parents: 24579
diff changeset
   203
f1333a841b26 removed obsolete Selector token;
wenzelm
parents: 24579
diff changeset
   204
end;
24579
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
   205
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
   206
24596
f1333a841b26 removed obsolete Selector token;
wenzelm
parents: 24579
diff changeset
   207
(* token source *)
24579
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
   208
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
   209
local
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
   210
30593
495672058d97 added scan_antiq;
wenzelm
parents: 30591
diff changeset
   211
fun token k ss = Token (Symbol_Pos.range ss, (k, Symbol_Pos.content ss));
24579
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
   212
30593
495672058d97 added scan_antiq;
wenzelm
parents: 30591
diff changeset
   213
val scan_ml =
27772
b933c997eab3 improved position handling due to SymbolPos.T;
wenzelm
parents: 27732
diff changeset
   214
 (scan_char >> token Char ||
b933c997eab3 improved position handling due to SymbolPos.T;
wenzelm
parents: 27732
diff changeset
   215
  scan_string >> token String ||
b933c997eab3 improved position handling due to SymbolPos.T;
wenzelm
parents: 27732
diff changeset
   216
  scan_blanks1 >> token Space ||
30573
49899f26fbd1 de-camelized Symbol_Pos;
wenzelm
parents: 29606
diff changeset
   217
  Symbol_Pos.scan_comment !!! >> token Comment ||
27772
b933c997eab3 improved position handling due to SymbolPos.T;
wenzelm
parents: 27732
diff changeset
   218
  Scan.max token_leq
b933c997eab3 improved position handling due to SymbolPos.T;
wenzelm
parents: 27732
diff changeset
   219
   (scan_keyword >> token Keyword)
b933c997eab3 improved position handling due to SymbolPos.T;
wenzelm
parents: 27732
diff changeset
   220
   (scan_word >> token Word ||
b933c997eab3 improved position handling due to SymbolPos.T;
wenzelm
parents: 27732
diff changeset
   221
    scan_real >> token Real ||
b933c997eab3 improved position handling due to SymbolPos.T;
wenzelm
parents: 27732
diff changeset
   222
    scan_int >> token Int ||
b933c997eab3 improved position handling due to SymbolPos.T;
wenzelm
parents: 27732
diff changeset
   223
    scan_longident >> token LongIdent ||
b933c997eab3 improved position handling due to SymbolPos.T;
wenzelm
parents: 27732
diff changeset
   224
    scan_ident >> token Ident ||
b933c997eab3 improved position handling due to SymbolPos.T;
wenzelm
parents: 27732
diff changeset
   225
    scan_typevar >> token TypeVar));
b933c997eab3 improved position handling due to SymbolPos.T;
wenzelm
parents: 27732
diff changeset
   226
b933c997eab3 improved position handling due to SymbolPos.T;
wenzelm
parents: 27732
diff changeset
   227
fun recover msg =
b933c997eab3 improved position handling due to SymbolPos.T;
wenzelm
parents: 27732
diff changeset
   228
  Scan.many (((not o Symbol.is_blank) andf Symbol.is_regular) o symbol)
b933c997eab3 improved position handling due to SymbolPos.T;
wenzelm
parents: 27732
diff changeset
   229
  >> (fn cs => [token (Error msg) cs]);
24579
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
   230
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
   231
in
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
   232
30593
495672058d97 added scan_antiq;
wenzelm
parents: 30591
diff changeset
   233
val scan_antiq = Antiquote.scan || scan_ml >> Antiquote.Text;
495672058d97 added scan_antiq;
wenzelm
parents: 30591
diff changeset
   234
24596
f1333a841b26 removed obsolete Selector token;
wenzelm
parents: 24579
diff changeset
   235
fun source src =
30573
49899f26fbd1 de-camelized Symbol_Pos;
wenzelm
parents: 29606
diff changeset
   236
  Symbol_Pos.source (Position.line 1) src
30593
495672058d97 added scan_antiq;
wenzelm
parents: 30591
diff changeset
   237
  |> Source.source Symbol_Pos.stopper (Scan.bulk (!!! "bad input" scan_ml)) (SOME (false, recover));
30591
6c9c00ea4ae6 added tokenize;
wenzelm
parents: 30573
diff changeset
   238
6c9c00ea4ae6 added tokenize;
wenzelm
parents: 30573
diff changeset
   239
val tokenize = Source.of_string #> source #> Source.exhaust;
24579
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
   240
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
   241
end;
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
   242
24596
f1333a841b26 removed obsolete Selector token;
wenzelm
parents: 24579
diff changeset
   243
end;
24579
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
   244