src/Pure/ML/ml_lex.ML
author wenzelm
Wed, 03 Nov 2010 13:54:23 +0100
changeset 40319 daaa0b236a3f
parent 39507 839873937ddd
child 40337 d25bbb5f1c9e
permissions -rw-r--r--
explicit warning about opaque signature matching -- saves extra paragraph in implementation manual;
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
30683
e8ac1f9d9469 datatype antiquote: maintain original Position.range, which is eventually attached to the resulting ML tokens;
wenzelm
parents: 30645
diff changeset
    16
  val set_range: Position.range -> token -> token
30636
bd8813d7774d ML_Lex.pos_of: regular position;
wenzelm
parents: 30614
diff changeset
    17
  val pos_of: token -> Position.T
31474
0ae32184bde0 export end_pos_of;
wenzelm
parents: 31426
diff changeset
    18
  val end_pos_of: token -> Position.T
24579
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
    19
  val kind_of: token -> token_kind
27817
78cae5cca09e renamed ML_Lex.val_of to content_of;
wenzelm
parents: 27799
diff changeset
    20
  val content_of: token -> string
31426
5c9dbd511510 tuned signature;
wenzelm
parents: 31332
diff changeset
    21
  val check_content_of: token -> string
31332
9639a6d4d714 added flatten;
wenzelm
parents: 30683
diff changeset
    22
  val flatten: token list -> string
30614
845bcfd3e9cd report markup for ML tokens;
wenzelm
parents: 30600
diff changeset
    23
  val report_token: token -> unit
24579
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
    24
  val keywords: string list
24596
f1333a841b26 removed obsolete Selector token;
wenzelm
parents: 24579
diff changeset
    25
  val source: (Symbol.symbol, 'a) Source.source ->
30573
49899f26fbd1 de-camelized Symbol_Pos;
wenzelm
parents: 29606
diff changeset
    26
    (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
    27
      Source.source) Source.source
30591
6c9c00ea4ae6 added tokenize;
wenzelm
parents: 30573
diff changeset
    28
  val tokenize: string -> token list
37198
3af985b10550 replaced ML_Lex.read_antiq by more concise ML_Lex.read, which includes full read/report with explicit position information;
wenzelm
parents: 37195
diff changeset
    29
  val read: Position.T -> Symbol_Pos.text -> token Antiquote.antiquote list
24579
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
    30
end;
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
    31
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
    32
structure ML_Lex: ML_LEX =
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
    33
struct
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
    34
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
    35
(** tokens **)
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
    36
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
    37
(* datatype token *)
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
    38
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
    39
datatype token_kind =
24596
f1333a841b26 removed obsolete Selector token;
wenzelm
parents: 24579
diff changeset
    40
  Keyword | Ident | LongIdent | TypeVar | Word | Int | Real | Char | String |
24579
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
    41
  Space | Comment | Error of string | EOF;
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
    42
27772
b933c997eab3 improved position handling due to SymbolPos.T;
wenzelm
parents: 27732
diff changeset
    43
datatype token = Token of Position.range * (token_kind * string);
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
b933c997eab3 improved position handling due to SymbolPos.T;
wenzelm
parents: 27732
diff changeset
    46
(* position *)
b933c997eab3 improved position handling due to SymbolPos.T;
wenzelm
parents: 27732
diff changeset
    47
30683
e8ac1f9d9469 datatype antiquote: maintain original Position.range, which is eventually attached to the resulting ML tokens;
wenzelm
parents: 30645
diff changeset
    48
fun set_range range (Token (_, x)) = Token (range, x);
e8ac1f9d9469 datatype antiquote: maintain original Position.range, which is eventually attached to the resulting ML tokens;
wenzelm
parents: 30645
diff changeset
    49
30636
bd8813d7774d ML_Lex.pos_of: regular position;
wenzelm
parents: 30614
diff changeset
    50
fun pos_of (Token ((pos, _), _)) = pos;
bd8813d7774d ML_Lex.pos_of: regular position;
wenzelm
parents: 30614
diff changeset
    51
fun end_pos_of (Token ((_, pos), _)) = pos;
24579
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
    52
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
    53
24596
f1333a841b26 removed obsolete Selector token;
wenzelm
parents: 24579
diff changeset
    54
(* control tokens *)
24579
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
    55
27772
b933c997eab3 improved position handling due to SymbolPos.T;
wenzelm
parents: 27732
diff changeset
    56
fun mk_eof pos = Token ((pos, Position.none), (EOF, ""));
b933c997eab3 improved position handling due to SymbolPos.T;
wenzelm
parents: 27732
diff changeset
    57
val eof = mk_eof Position.none;
24579
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
    58
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
    59
fun is_eof (Token (_, (EOF, _))) = true
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
    60
  | is_eof _ = false;
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
    61
27772
b933c997eab3 improved position handling due to SymbolPos.T;
wenzelm
parents: 27732
diff changeset
    62
val stopper =
30636
bd8813d7774d ML_Lex.pos_of: regular position;
wenzelm
parents: 30614
diff changeset
    63
  Scan.stopper (fn [] => eof | toks => mk_eof (end_pos_of (List.last toks))) is_eof;
27772
b933c997eab3 improved position handling due to SymbolPos.T;
wenzelm
parents: 27732
diff changeset
    64
24579
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
    65
27772
b933c997eab3 improved position handling due to SymbolPos.T;
wenzelm
parents: 27732
diff changeset
    66
(* token content *)
b933c997eab3 improved position handling due to SymbolPos.T;
wenzelm
parents: 27732
diff changeset
    67
31426
5c9dbd511510 tuned signature;
wenzelm
parents: 31332
diff changeset
    68
fun kind_of (Token (_, (k, _))) = k;
5c9dbd511510 tuned signature;
wenzelm
parents: 31332
diff changeset
    69
27817
78cae5cca09e renamed ML_Lex.val_of to content_of;
wenzelm
parents: 27799
diff changeset
    70
fun content_of (Token (_, (_, x))) = x;
78cae5cca09e renamed ML_Lex.val_of to content_of;
wenzelm
parents: 27799
diff changeset
    71
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
    72
31426
5c9dbd511510 tuned signature;
wenzelm
parents: 31332
diff changeset
    73
fun check_content_of tok =
30636
bd8813d7774d ML_Lex.pos_of: regular position;
wenzelm
parents: 30614
diff changeset
    74
  (case kind_of tok of
30645
e7943202d177 added read_antiq, with improved error reporting;
wenzelm
parents: 30636
diff changeset
    75
    Error msg => error msg
40319
daaa0b236a3f explicit warning about opaque signature matching -- saves extra paragraph in implementation manual;
wenzelm
parents: 39507
diff changeset
    76
  | _ =>
daaa0b236a3f explicit warning about opaque signature matching -- saves extra paragraph in implementation manual;
wenzelm
parents: 39507
diff changeset
    77
      (case tok of
daaa0b236a3f explicit warning about opaque signature matching -- saves extra paragraph in implementation manual;
wenzelm
parents: 39507
diff changeset
    78
        Token (_, (Keyword, ":>")) =>
daaa0b236a3f explicit warning about opaque signature matching -- saves extra paragraph in implementation manual;
wenzelm
parents: 39507
diff changeset
    79
          warning ("Opaque signature matching (:>) fails to work with ML pretty printing --\n\
daaa0b236a3f explicit warning about opaque signature matching -- saves extra paragraph in implementation manual;
wenzelm
parents: 39507
diff changeset
    80
            \prefer non-opaque matching (:) possibly with abstype" ^
daaa0b236a3f explicit warning about opaque signature matching -- saves extra paragraph in implementation manual;
wenzelm
parents: 39507
diff changeset
    81
            Position.str_of (pos_of tok))
daaa0b236a3f explicit warning about opaque signature matching -- saves extra paragraph in implementation manual;
wenzelm
parents: 39507
diff changeset
    82
      | _ => ();
daaa0b236a3f explicit warning about opaque signature matching -- saves extra paragraph in implementation manual;
wenzelm
parents: 39507
diff changeset
    83
      content_of tok));
30636
bd8813d7774d ML_Lex.pos_of: regular position;
wenzelm
parents: 30614
diff changeset
    84
31426
5c9dbd511510 tuned signature;
wenzelm
parents: 31332
diff changeset
    85
val flatten = implode o map (Symbol.escape o check_content_of);
31332
9639a6d4d714 added flatten;
wenzelm
parents: 30683
diff changeset
    86
24596
f1333a841b26 removed obsolete Selector token;
wenzelm
parents: 24579
diff changeset
    87
fun is_regular (Token (_, (Error _, _))) = false
f1333a841b26 removed obsolete Selector token;
wenzelm
parents: 24579
diff changeset
    88
  | is_regular (Token (_, (EOF, _))) = false
f1333a841b26 removed obsolete Selector token;
wenzelm
parents: 24579
diff changeset
    89
  | is_regular _ = true;
f1333a841b26 removed obsolete Selector token;
wenzelm
parents: 24579
diff changeset
    90
f1333a841b26 removed obsolete Selector token;
wenzelm
parents: 24579
diff changeset
    91
fun is_improper (Token (_, (Space, _))) = true
f1333a841b26 removed obsolete Selector token;
wenzelm
parents: 24579
diff changeset
    92
  | is_improper (Token (_, (Comment, _))) = true
f1333a841b26 removed obsolete Selector token;
wenzelm
parents: 24579
diff changeset
    93
  | is_improper _ = false;
f1333a841b26 removed obsolete Selector token;
wenzelm
parents: 24579
diff changeset
    94
f1333a841b26 removed obsolete Selector token;
wenzelm
parents: 24579
diff changeset
    95
30614
845bcfd3e9cd report markup for ML tokens;
wenzelm
parents: 30600
diff changeset
    96
(* markup *)
845bcfd3e9cd report markup for ML tokens;
wenzelm
parents: 30600
diff changeset
    97
37195
e87d305a4490 separate markup for ML delimiters;
wenzelm
parents: 31543
diff changeset
    98
local
e87d305a4490 separate markup for ML delimiters;
wenzelm
parents: 31543
diff changeset
    99
30645
e7943202d177 added read_antiq, with improved error reporting;
wenzelm
parents: 30636
diff changeset
   100
val token_kind_markup =
e7943202d177 added read_antiq, with improved error reporting;
wenzelm
parents: 30636
diff changeset
   101
 fn Keyword   => Markup.ML_keyword
e7943202d177 added read_antiq, with improved error reporting;
wenzelm
parents: 30636
diff changeset
   102
  | Ident     => Markup.ML_ident
e7943202d177 added read_antiq, with improved error reporting;
wenzelm
parents: 30636
diff changeset
   103
  | LongIdent => Markup.ML_ident
e7943202d177 added read_antiq, with improved error reporting;
wenzelm
parents: 30636
diff changeset
   104
  | TypeVar   => Markup.ML_tvar
e7943202d177 added read_antiq, with improved error reporting;
wenzelm
parents: 30636
diff changeset
   105
  | Word      => Markup.ML_numeral
e7943202d177 added read_antiq, with improved error reporting;
wenzelm
parents: 30636
diff changeset
   106
  | Int       => Markup.ML_numeral
e7943202d177 added read_antiq, with improved error reporting;
wenzelm
parents: 30636
diff changeset
   107
  | Real      => Markup.ML_numeral
e7943202d177 added read_antiq, with improved error reporting;
wenzelm
parents: 30636
diff changeset
   108
  | Char      => Markup.ML_char
e7943202d177 added read_antiq, with improved error reporting;
wenzelm
parents: 30636
diff changeset
   109
  | String    => Markup.ML_string
38474
e498dc2eb576 uniform Markup.empty/Markup.Empty in ML and Scala;
wenzelm
parents: 37209
diff changeset
   110
  | Space     => Markup.empty
30645
e7943202d177 added read_antiq, with improved error reporting;
wenzelm
parents: 30636
diff changeset
   111
  | Comment   => Markup.ML_comment
e7943202d177 added read_antiq, with improved error reporting;
wenzelm
parents: 30636
diff changeset
   112
  | Error _   => Markup.ML_malformed
38474
e498dc2eb576 uniform Markup.empty/Markup.Empty in ML and Scala;
wenzelm
parents: 37209
diff changeset
   113
  | EOF       => Markup.empty;
30614
845bcfd3e9cd report markup for ML tokens;
wenzelm
parents: 30600
diff changeset
   114
37195
e87d305a4490 separate markup for ML delimiters;
wenzelm
parents: 31543
diff changeset
   115
fun token_markup kind x =
e87d305a4490 separate markup for ML delimiters;
wenzelm
parents: 31543
diff changeset
   116
  if kind = Keyword andalso exists_string (not o Symbol.is_ascii_letter) x
e87d305a4490 separate markup for ML delimiters;
wenzelm
parents: 31543
diff changeset
   117
  then Markup.ML_delimiter
e87d305a4490 separate markup for ML delimiters;
wenzelm
parents: 31543
diff changeset
   118
  else token_kind_markup kind;
e87d305a4490 separate markup for ML delimiters;
wenzelm
parents: 31543
diff changeset
   119
e87d305a4490 separate markup for ML delimiters;
wenzelm
parents: 31543
diff changeset
   120
in
e87d305a4490 separate markup for ML delimiters;
wenzelm
parents: 31543
diff changeset
   121
39507
839873937ddd tuned signature of (Context_)Position.report variants;
wenzelm
parents: 38474
diff changeset
   122
fun report_token (Token ((pos, _), (kind, x))) = Position.report pos (token_markup kind x);
37195
e87d305a4490 separate markup for ML delimiters;
wenzelm
parents: 31543
diff changeset
   123
e87d305a4490 separate markup for ML delimiters;
wenzelm
parents: 31543
diff changeset
   124
end;
30614
845bcfd3e9cd report markup for ML tokens;
wenzelm
parents: 30600
diff changeset
   125
845bcfd3e9cd report markup for ML tokens;
wenzelm
parents: 30600
diff changeset
   126
24579
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
   127
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
   128
(** scanners **)
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
   129
30573
49899f26fbd1 de-camelized Symbol_Pos;
wenzelm
parents: 29606
diff changeset
   130
open Basic_Symbol_Pos;
24579
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
   131
30573
49899f26fbd1 de-camelized Symbol_Pos;
wenzelm
parents: 29606
diff changeset
   132
fun !!! msg = Symbol_Pos.!!! ("SML lexical error: " ^ msg);
24579
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
   133
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
   134
27772
b933c997eab3 improved position handling due to SymbolPos.T;
wenzelm
parents: 27732
diff changeset
   135
(* blanks *)
24579
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
   136
27772
b933c997eab3 improved position handling due to SymbolPos.T;
wenzelm
parents: 27732
diff changeset
   137
val scan_blank = Scan.one (Symbol.is_ascii_blank o symbol);
b933c997eab3 improved position handling due to SymbolPos.T;
wenzelm
parents: 27732
diff changeset
   138
val scan_blanks1 = Scan.repeat1 scan_blank;
24579
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
   139
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
   140
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
   141
(* keywords *)
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
   142
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
   143
val keywords = ["#", "(", ")", ",", "->", "...", ":", ":>", ";", "=",
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
   144
  "=>", "[", "]", "_", "{", "|", "}", "abstype", "and", "andalso", "as",
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
   145
  "case", "datatype", "do", "else", "end", "eqtype", "exception", "fn",
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
   146
  "fun", "functor", "handle", "if", "in", "include", "infix", "infixr",
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
   147
  "let", "local", "nonfix", "of", "op", "open", "orelse", "raise", "rec",
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
   148
  "sharing", "sig", "signature", "struct", "structure", "then", "type",
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
   149
  "val", "where", "while", "with", "withtype"];
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
   150
27772
b933c997eab3 improved position handling due to SymbolPos.T;
wenzelm
parents: 27732
diff changeset
   151
val lex = Scan.make_lexicon (map explode keywords);
b933c997eab3 improved position handling due to SymbolPos.T;
wenzelm
parents: 27732
diff changeset
   152
fun scan_keyword x = Scan.literal lex x;
24579
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
   153
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
   154
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
   155
(* identifiers *)
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
   156
24596
f1333a841b26 removed obsolete Selector token;
wenzelm
parents: 24579
diff changeset
   157
local
f1333a841b26 removed obsolete Selector token;
wenzelm
parents: 24579
diff changeset
   158
24579
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
   159
val scan_letdigs =
27772
b933c997eab3 improved position handling due to SymbolPos.T;
wenzelm
parents: 27732
diff changeset
   160
  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
   161
27772
b933c997eab3 improved position handling due to SymbolPos.T;
wenzelm
parents: 27732
diff changeset
   162
val scan_alphanumeric = Scan.one (Symbol.is_ascii_letter o symbol) -- scan_letdigs >> op ::;
24579
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
   163
27772
b933c997eab3 improved position handling due to SymbolPos.T;
wenzelm
parents: 27732
diff changeset
   164
val scan_symbolic = Scan.many1 (member (op =) (explode "!#$%&*+-/:<=>?@\\^`|~") o symbol);
24579
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
   165
24596
f1333a841b26 removed obsolete Selector token;
wenzelm
parents: 24579
diff changeset
   166
in
f1333a841b26 removed obsolete Selector token;
wenzelm
parents: 24579
diff changeset
   167
24579
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
   168
val scan_ident = scan_alphanumeric || scan_symbolic;
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
   169
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
   170
val scan_longident =
27772
b933c997eab3 improved position handling due to SymbolPos.T;
wenzelm
parents: 27732
diff changeset
   171
  (Scan.repeat1 (scan_alphanumeric @@@ $$$ ".") >> flat) @@@ (scan_ident || $$$ "=");
24579
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
   172
27772
b933c997eab3 improved position handling due to SymbolPos.T;
wenzelm
parents: 27732
diff changeset
   173
val scan_typevar = $$$ "'" @@@ scan_letdigs;
24579
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
   174
24596
f1333a841b26 removed obsolete Selector token;
wenzelm
parents: 24579
diff changeset
   175
end;
24579
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
   176
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
   177
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
   178
(* numerals *)
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
   179
24596
f1333a841b26 removed obsolete Selector token;
wenzelm
parents: 24579
diff changeset
   180
local
f1333a841b26 removed obsolete Selector token;
wenzelm
parents: 24579
diff changeset
   181
27772
b933c997eab3 improved position handling due to SymbolPos.T;
wenzelm
parents: 27732
diff changeset
   182
val scan_dec = Scan.many1 (Symbol.is_ascii_digit o symbol);
b933c997eab3 improved position handling due to SymbolPos.T;
wenzelm
parents: 27732
diff changeset
   183
val scan_hex = Scan.many1 (Symbol.is_ascii_hex o symbol);
b933c997eab3 improved position handling due to SymbolPos.T;
wenzelm
parents: 27732
diff changeset
   184
val scan_sign = Scan.optional ($$$ "~") [];
b933c997eab3 improved position handling due to SymbolPos.T;
wenzelm
parents: 27732
diff changeset
   185
val scan_decint = scan_sign @@@ scan_dec;
24579
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
   186
24596
f1333a841b26 removed obsolete Selector token;
wenzelm
parents: 24579
diff changeset
   187
in
f1333a841b26 removed obsolete Selector token;
wenzelm
parents: 24579
diff changeset
   188
27772
b933c997eab3 improved position handling due to SymbolPos.T;
wenzelm
parents: 27732
diff changeset
   189
val scan_word =
b933c997eab3 improved position handling due to SymbolPos.T;
wenzelm
parents: 27732
diff changeset
   190
  $$$ "0" @@@ $$$ "w" @@@ $$$ "x" @@@ scan_hex ||
b933c997eab3 improved position handling due to SymbolPos.T;
wenzelm
parents: 27732
diff changeset
   191
  $$$ "0" @@@ $$$ "w" @@@ scan_dec;
24579
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
   192
27772
b933c997eab3 improved position handling due to SymbolPos.T;
wenzelm
parents: 27732
diff changeset
   193
val scan_int = scan_sign @@@ ($$$ "0" @@@ $$$ "x" @@@ scan_hex || scan_dec);
24579
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
   194
27772
b933c997eab3 improved position handling due to SymbolPos.T;
wenzelm
parents: 27732
diff changeset
   195
val scan_exp = ($$$ "E" || $$$ "e") @@@ scan_decint;
24579
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
   196
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
   197
val scan_real =
27772
b933c997eab3 improved position handling due to SymbolPos.T;
wenzelm
parents: 27732
diff changeset
   198
  scan_decint @@@ $$$ "." @@@ scan_dec @@@ Scan.optional scan_exp [] ||
b933c997eab3 improved position handling due to SymbolPos.T;
wenzelm
parents: 27732
diff changeset
   199
  scan_decint @@@ scan_exp;
24579
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
   200
24596
f1333a841b26 removed obsolete Selector token;
wenzelm
parents: 24579
diff changeset
   201
end;
f1333a841b26 removed obsolete Selector token;
wenzelm
parents: 24579
diff changeset
   202
24579
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
   203
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
   204
(* chars and strings *)
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
   205
24596
f1333a841b26 removed obsolete Selector token;
wenzelm
parents: 24579
diff changeset
   206
local
f1333a841b26 removed obsolete Selector token;
wenzelm
parents: 24579
diff changeset
   207
f1333a841b26 removed obsolete Selector token;
wenzelm
parents: 24579
diff changeset
   208
val scan_escape =
27772
b933c997eab3 improved position handling due to SymbolPos.T;
wenzelm
parents: 27732
diff changeset
   209
  Scan.one (member (op =) (explode "\"\\abtnvfr") o symbol) >> single ||
b933c997eab3 improved position handling due to SymbolPos.T;
wenzelm
parents: 27732
diff changeset
   210
  $$$ "^" @@@ (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
   211
  Scan.one (Symbol.is_ascii_digit o symbol) --
b933c997eab3 improved position handling due to SymbolPos.T;
wenzelm
parents: 27732
diff changeset
   212
    Scan.one (Symbol.is_ascii_digit o symbol) --
b933c997eab3 improved position handling due to SymbolPos.T;
wenzelm
parents: 27732
diff changeset
   213
    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
   214
f1333a841b26 removed obsolete Selector token;
wenzelm
parents: 24579
diff changeset
   215
val scan_str =
30600
de241396389c allow non-printable symbols within string tokens;
wenzelm
parents: 30593
diff changeset
   216
  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
   217
    (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
   218
  $$$ "\\" @@@ !!! "bad escape character in string" scan_escape;
24596
f1333a841b26 removed obsolete Selector token;
wenzelm
parents: 24579
diff changeset
   219
27772
b933c997eab3 improved position handling due to SymbolPos.T;
wenzelm
parents: 27732
diff changeset
   220
val scan_gap = $$$ "\\" @@@ scan_blanks1 @@@ $$$ "\\";
b933c997eab3 improved position handling due to SymbolPos.T;
wenzelm
parents: 27732
diff changeset
   221
val scan_gaps = Scan.repeat scan_gap >> flat;
24579
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
   222
24596
f1333a841b26 removed obsolete Selector token;
wenzelm
parents: 24579
diff changeset
   223
in
24579
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
   224
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
   225
val scan_char =
27772
b933c997eab3 improved position handling due to SymbolPos.T;
wenzelm
parents: 27732
diff changeset
   226
  $$$ "#" @@@ $$$ "\"" @@@ scan_gaps @@@ scan_str @@@ scan_gaps @@@ $$$ "\"";
24579
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
   227
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
   228
val scan_string =
27772
b933c997eab3 improved position handling due to SymbolPos.T;
wenzelm
parents: 27732
diff changeset
   229
  $$$ "\"" @@@ !!! "missing quote at end of string"
b933c997eab3 improved position handling due to SymbolPos.T;
wenzelm
parents: 27732
diff changeset
   230
    ((Scan.repeat (scan_gap || scan_str) >> flat) @@@ $$$ "\"");
24596
f1333a841b26 removed obsolete Selector token;
wenzelm
parents: 24579
diff changeset
   231
f1333a841b26 removed obsolete Selector token;
wenzelm
parents: 24579
diff changeset
   232
end;
24579
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
   233
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
   234
30645
e7943202d177 added read_antiq, with improved error reporting;
wenzelm
parents: 30636
diff changeset
   235
(* scan tokens *)
24579
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
   236
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
   237
local
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
   238
30593
495672058d97 added scan_antiq;
wenzelm
parents: 30591
diff changeset
   239
fun token k ss = Token (Symbol_Pos.range ss, (k, Symbol_Pos.content ss));
24579
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
   240
30593
495672058d97 added scan_antiq;
wenzelm
parents: 30591
diff changeset
   241
val scan_ml =
27772
b933c997eab3 improved position handling due to SymbolPos.T;
wenzelm
parents: 27732
diff changeset
   242
 (scan_char >> token Char ||
b933c997eab3 improved position handling due to SymbolPos.T;
wenzelm
parents: 27732
diff changeset
   243
  scan_string >> token String ||
b933c997eab3 improved position handling due to SymbolPos.T;
wenzelm
parents: 27732
diff changeset
   244
  scan_blanks1 >> token Space ||
30573
49899f26fbd1 de-camelized Symbol_Pos;
wenzelm
parents: 29606
diff changeset
   245
  Symbol_Pos.scan_comment !!! >> token Comment ||
27772
b933c997eab3 improved position handling due to SymbolPos.T;
wenzelm
parents: 27732
diff changeset
   246
  Scan.max token_leq
b933c997eab3 improved position handling due to SymbolPos.T;
wenzelm
parents: 27732
diff changeset
   247
   (scan_keyword >> token Keyword)
b933c997eab3 improved position handling due to SymbolPos.T;
wenzelm
parents: 27732
diff changeset
   248
   (scan_word >> token Word ||
b933c997eab3 improved position handling due to SymbolPos.T;
wenzelm
parents: 27732
diff changeset
   249
    scan_real >> token Real ||
b933c997eab3 improved position handling due to SymbolPos.T;
wenzelm
parents: 27732
diff changeset
   250
    scan_int >> token Int ||
b933c997eab3 improved position handling due to SymbolPos.T;
wenzelm
parents: 27732
diff changeset
   251
    scan_longident >> token LongIdent ||
b933c997eab3 improved position handling due to SymbolPos.T;
wenzelm
parents: 27732
diff changeset
   252
    scan_ident >> token Ident ||
b933c997eab3 improved position handling due to SymbolPos.T;
wenzelm
parents: 27732
diff changeset
   253
    scan_typevar >> token TypeVar));
b933c997eab3 improved position handling due to SymbolPos.T;
wenzelm
parents: 27732
diff changeset
   254
30645
e7943202d177 added read_antiq, with improved error reporting;
wenzelm
parents: 30636
diff changeset
   255
val scan_antiq = Antiquote.scan || scan_ml >> Antiquote.Text;
e7943202d177 added read_antiq, with improved error reporting;
wenzelm
parents: 30636
diff changeset
   256
27772
b933c997eab3 improved position handling due to SymbolPos.T;
wenzelm
parents: 27732
diff changeset
   257
fun recover msg =
b933c997eab3 improved position handling due to SymbolPos.T;
wenzelm
parents: 27732
diff changeset
   258
  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
   259
  >> (fn cs => [token (Error msg) cs]);
24579
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
   260
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
   261
in
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
   262
24596
f1333a841b26 removed obsolete Selector token;
wenzelm
parents: 24579
diff changeset
   263
fun source src =
30573
49899f26fbd1 de-camelized Symbol_Pos;
wenzelm
parents: 29606
diff changeset
   264
  Symbol_Pos.source (Position.line 1) src
30593
495672058d97 added scan_antiq;
wenzelm
parents: 30591
diff changeset
   265
  |> Source.source Symbol_Pos.stopper (Scan.bulk (!!! "bad input" scan_ml)) (SOME (false, recover));
30591
6c9c00ea4ae6 added tokenize;
wenzelm
parents: 30573
diff changeset
   266
31543
5bef6c7cc819 allow Isabelle symbols within low-level ML source;
wenzelm
parents: 31474
diff changeset
   267
val tokenize =
5bef6c7cc819 allow Isabelle symbols within low-level ML source;
wenzelm
parents: 31474
diff changeset
   268
  Source.of_string #>
5bef6c7cc819 allow Isabelle symbols within low-level ML source;
wenzelm
parents: 31474
diff changeset
   269
  Symbol.source {do_recover = true} #>
5bef6c7cc819 allow Isabelle symbols within low-level ML source;
wenzelm
parents: 31474
diff changeset
   270
  source #>
5bef6c7cc819 allow Isabelle symbols within low-level ML source;
wenzelm
parents: 31474
diff changeset
   271
  Source.exhaust;
24579
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
   272
37198
3af985b10550 replaced ML_Lex.read_antiq by more concise ML_Lex.read, which includes full read/report with explicit position information;
wenzelm
parents: 37195
diff changeset
   273
fun read pos txt =
3af985b10550 replaced ML_Lex.read_antiq by more concise ML_Lex.read, which includes full read/report with explicit position information;
wenzelm
parents: 37195
diff changeset
   274
  let
39507
839873937ddd tuned signature of (Context_)Position.report variants;
wenzelm
parents: 38474
diff changeset
   275
    val _ = Position.report pos Markup.ML_source;
37198
3af985b10550 replaced ML_Lex.read_antiq by more concise ML_Lex.read, which includes full read/report with explicit position information;
wenzelm
parents: 37195
diff changeset
   276
    val syms = Symbol_Pos.explode (txt, pos);
37209
1c8cf0048934 terminate ML compiler input produced by ML_Lex.read (cf. 85e864045497);
wenzelm
parents: 37198
diff changeset
   277
    val termination =
1c8cf0048934 terminate ML compiler input produced by ML_Lex.read (cf. 85e864045497);
wenzelm
parents: 37198
diff changeset
   278
      if null syms then []
1c8cf0048934 terminate ML compiler input produced by ML_Lex.read (cf. 85e864045497);
wenzelm
parents: 37198
diff changeset
   279
      else
1c8cf0048934 terminate ML compiler input produced by ML_Lex.read (cf. 85e864045497);
wenzelm
parents: 37198
diff changeset
   280
        let
1c8cf0048934 terminate ML compiler input produced by ML_Lex.read (cf. 85e864045497);
wenzelm
parents: 37198
diff changeset
   281
          val pos1 = List.last syms |-> Position.advance;
1c8cf0048934 terminate ML compiler input produced by ML_Lex.read (cf. 85e864045497);
wenzelm
parents: 37198
diff changeset
   282
          val pos2 = Position.advance Symbol.space pos1;
1c8cf0048934 terminate ML compiler input produced by ML_Lex.read (cf. 85e864045497);
wenzelm
parents: 37198
diff changeset
   283
        in [Antiquote.Text (Token (Position.range pos1 pos2, (Space, Symbol.space)))] end;
1c8cf0048934 terminate ML compiler input produced by ML_Lex.read (cf. 85e864045497);
wenzelm
parents: 37198
diff changeset
   284
    val input =
1c8cf0048934 terminate ML compiler input produced by ML_Lex.read (cf. 85e864045497);
wenzelm
parents: 37198
diff changeset
   285
      (Source.of_list syms
1c8cf0048934 terminate ML compiler input produced by ML_Lex.read (cf. 85e864045497);
wenzelm
parents: 37198
diff changeset
   286
        |> Source.source Symbol_Pos.stopper (Scan.bulk (!!! "bad input" scan_antiq))
1c8cf0048934 terminate ML compiler input produced by ML_Lex.read (cf. 85e864045497);
wenzelm
parents: 37198
diff changeset
   287
          (SOME (false, fn msg => recover msg >> map Antiquote.Text))
1c8cf0048934 terminate ML compiler input produced by ML_Lex.read (cf. 85e864045497);
wenzelm
parents: 37198
diff changeset
   288
        |> Source.exhaust
1c8cf0048934 terminate ML compiler input produced by ML_Lex.read (cf. 85e864045497);
wenzelm
parents: 37198
diff changeset
   289
        |> tap (List.app (Antiquote.report report_token))
1c8cf0048934 terminate ML compiler input produced by ML_Lex.read (cf. 85e864045497);
wenzelm
parents: 37198
diff changeset
   290
        |> tap Antiquote.check_nesting
1c8cf0048934 terminate ML compiler input produced by ML_Lex.read (cf. 85e864045497);
wenzelm
parents: 37198
diff changeset
   291
        |> tap (List.app (fn Antiquote.Text tok => ignore (check_content_of tok) | _ => ())))
1c8cf0048934 terminate ML compiler input produced by ML_Lex.read (cf. 85e864045497);
wenzelm
parents: 37198
diff changeset
   292
      handle ERROR msg =>
1c8cf0048934 terminate ML compiler input produced by ML_Lex.read (cf. 85e864045497);
wenzelm
parents: 37198
diff changeset
   293
        cat_error msg ("The error(s) above occurred in ML source" ^ Position.str_of pos);
1c8cf0048934 terminate ML compiler input produced by ML_Lex.read (cf. 85e864045497);
wenzelm
parents: 37198
diff changeset
   294
  in input @ termination end;
30645
e7943202d177 added read_antiq, with improved error reporting;
wenzelm
parents: 30636
diff changeset
   295
24579
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
   296
end;
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
   297
24596
f1333a841b26 removed obsolete Selector token;
wenzelm
parents: 24579
diff changeset
   298
end;
24579
852fc50927b1 Lexical syntax for SML.
wenzelm
parents:
diff changeset
   299