src/Pure/Thy/thy_scan.ML
author wenzelm
Wed Oct 17 18:52:30 2001 +0200 (2001-10-17)
changeset 11819 9283b3c11234
parent 6667 58b9785f8534
child 14729 0e987111a17e
permissions -rw-r--r--
tuned comments;
wenzelm@4705
     1
(*  Title:	Pure/Thy/thy_scan.ML
wenzelm@4705
     2
    ID:		$Id$
wenzelm@4705
     3
    Author:	Markus Wenzel, TU Muenchen
wenzelm@11819
     4
    License:    GPL (GNU GENERAL PUBLIC LICENSE)
wenzelm@388
     5
wenzelm@11819
     6
Lexer for *old-style* outer syntax.
wenzelm@388
     7
*)
wenzelm@388
     8
wenzelm@388
     9
signature THY_SCAN =
wenzelm@4705
    10
sig
wenzelm@388
    11
  datatype token_kind =
wenzelm@4705
    12
    Keyword | Ident | LongIdent | Var | TypeVar | Nat | String | Verbatim | Ignore | EOF
wenzelm@388
    13
  val name_of_kind: token_kind -> string
wenzelm@6207
    14
  val tokenize: Scan.lexicon -> string list -> (token_kind * string * int) list
wenzelm@4705
    15
end;
wenzelm@388
    16
wenzelm@4705
    17
structure ThyScan: THY_SCAN =
wenzelm@388
    18
struct
wenzelm@388
    19
wenzelm@388
    20
wenzelm@388
    21
(** token kinds **)
wenzelm@388
    22
wenzelm@388
    23
datatype token_kind =
wenzelm@4705
    24
  Keyword | Ident | LongIdent | Var | TypeVar | Nat | String | Verbatim | Ignore | EOF;
wenzelm@388
    25
wenzelm@388
    26
fun name_of_kind Keyword = "keyword"
wenzelm@388
    27
  | name_of_kind Ident = "identifier"
wenzelm@388
    28
  | name_of_kind LongIdent = "long identifier"
wenzelm@4705
    29
  | name_of_kind Var = "schematic variable"
wenzelm@388
    30
  | name_of_kind TypeVar = "type variable"
wenzelm@388
    31
  | name_of_kind Nat = "natural number"
wenzelm@388
    32
  | name_of_kind String = "string"
wenzelm@388
    33
  | name_of_kind Verbatim = "verbatim text"
wenzelm@4705
    34
  | name_of_kind Ignore = "ignore"
wenzelm@388
    35
  | name_of_kind EOF = "end-of-file";
wenzelm@388
    36
wenzelm@388
    37
wenzelm@388
    38
wenzelm@388
    39
(** scanners **)
wenzelm@388
    40
wenzelm@4705
    41
(* diagnostics *)
wenzelm@4705
    42
wenzelm@4705
    43
fun lex_err None msg = "Outer lexical error: " ^ msg
wenzelm@4705
    44
  | lex_err (Some n) msg = "Outer lexical error on line " ^ string_of_int n ^ ": " ^ msg;
wenzelm@388
    45
wenzelm@388
    46
wenzelm@4705
    47
(* line numbering *)
wenzelm@4705
    48
wenzelm@4705
    49
val incr = apsome (fn n:int => n + 1);
wenzelm@388
    50
wenzelm@4705
    51
fun incr_line scan = Scan.depend (fn n => scan >> pair (incr n));
wenzelm@4705
    52
val keep_line = Scan.lift;
wenzelm@388
    53
wenzelm@4705
    54
val scan_blank =
wenzelm@4705
    55
  incr_line ($$ "\n") ||
wenzelm@4705
    56
  keep_line (Scan.one Symbol.is_blank);
wenzelm@388
    57
wenzelm@388
    58
wenzelm@4705
    59
(* scan ML-style strings *)
wenzelm@388
    60
wenzelm@4705
    61
val scan_ctrl =
wenzelm@4705
    62
  $$ "^" ^^ Scan.one (fn c => Symbol.is_ascii c andalso ord c >= 64 andalso ord c <= 95);
wenzelm@388
    63
wenzelm@4705
    64
val scan_dig = Scan.one Symbol.is_digit;
wenzelm@388
    65
wenzelm@388
    66
val scan_esc =
wenzelm@4921
    67
  keep_line ($$ "\\") ^^ !! (fn ((n, _), _) => lex_err n "bad escape sequence in string")
wenzelm@4705
    68
    (keep_line ($$ "n" || $$ "t" || $$ "\"" || $$ "\\" ||
wenzelm@4705
    69
      scan_ctrl || scan_dig ^^ scan_dig ^^ scan_dig) ||
wenzelm@4705
    70
      (Scan.repeat1 scan_blank >> implode) ^^ keep_line ($$ "\\"));
wenzelm@388
    71
wenzelm@4705
    72
val scan_str =
wenzelm@4705
    73
  scan_esc ||
wenzelm@5910
    74
  scan_blank >> K Symbol.space ||
wenzelm@4705
    75
  keep_line (Scan.one (not_equal "\"" andf Symbol.not_eof));
wenzelm@4705
    76
wenzelm@4705
    77
val scan_string =
wenzelm@4705
    78
  keep_line ($$ "\"") ^^
wenzelm@4921
    79
  !! (fn ((n, _), _) => lex_err n "missing quote at end of string")
wenzelm@4705
    80
    ((Scan.repeat scan_str >> implode) ^^ keep_line ($$ "\""));
wenzelm@388
    81
wenzelm@388
    82
wenzelm@388
    83
(* scan verbatim text *)
wenzelm@388
    84
wenzelm@4705
    85
val scan_verb =
wenzelm@4705
    86
  scan_blank ||
wenzelm@4705
    87
  keep_line ($$ "|" --| Scan.ahead (Scan.one (not_equal "}"))) ||
wenzelm@4705
    88
  keep_line (Scan.one (not_equal "|" andf Symbol.not_eof));
wenzelm@4705
    89
wenzelm@4705
    90
val scan_verbatim =
wenzelm@4705
    91
  keep_line ($$ "{" -- $$ "|") |--
wenzelm@4921
    92
  !! (fn ((n, _), _) => lex_err n "missing end of verbatim text")
wenzelm@4705
    93
    ((Scan.repeat scan_verb >> implode) --| keep_line ($$ "|" -- $$ "}"));
wenzelm@388
    94
wenzelm@388
    95
wenzelm@388
    96
(* scan nested comments *)
wenzelm@388
    97
wenzelm@4705
    98
val scan_cmt =
wenzelm@4705
    99
  Scan.lift scan_blank ||
wenzelm@4705
   100
  Scan.depend (fn d => keep_line ($$ "(" ^^ $$ "*") >> pair (d + 1)) ||
wenzelm@4705
   101
  Scan.depend (fn 0 => Scan.fail | d => keep_line ($$ "*" ^^ $$ ")") >> pair (d - 1)) ||
wenzelm@4705
   102
  Scan.lift (keep_line ($$ "*" --| Scan.ahead (Scan.one (not_equal ")")))) ||
wenzelm@4705
   103
  Scan.lift (keep_line (Scan.one (not_equal "*" andf Symbol.not_eof)));
wenzelm@388
   104
wenzelm@4705
   105
val scan_comment =
wenzelm@4705
   106
  keep_line ($$ "(" -- $$ "*") |--
wenzelm@4921
   107
  !! (fn ((n, _), _) => lex_err n "missing end of comment")
wenzelm@4705
   108
    (Scan.pass 0 (Scan.repeat scan_cmt) |-- keep_line ($$ "*" -- $$ ")") >> K "");
wenzelm@388
   109
wenzelm@388
   110
wenzelm@4705
   111
(* scan token *)
wenzelm@4705
   112
wenzelm@4705
   113
fun token k None x = (k, x, 0)
wenzelm@4705
   114
  | token k (Some n) x = (k, x, n);
wenzelm@388
   115
wenzelm@4705
   116
fun scan_tok lex (n, cs) =
wenzelm@4705
   117
 (scan_string >> token String n ||
wenzelm@4705
   118
  scan_verbatim >> token Verbatim n ||
wenzelm@4705
   119
  Scan.repeat1 scan_blank >> (token Ignore n o implode) ||
wenzelm@4705
   120
  scan_comment >> token Ignore n ||
wenzelm@4705
   121
  keep_line (Scan.max (fn ((_, x, _), (_, x', _)) => x <= x')
wenzelm@4705
   122
    (Scan.literal lex >> (token Keyword n o implode))
wenzelm@4705
   123
    (Syntax.scan_longid >> token LongIdent n ||
wenzelm@4705
   124
      Syntax.scan_id >> token Ident n ||
wenzelm@4705
   125
      Syntax.scan_var >> token Var n ||
wenzelm@4705
   126
      Syntax.scan_tid >> token TypeVar n ||
wenzelm@4705
   127
      Syntax.scan_nat >> token Nat n))) (n, cs);
wenzelm@388
   128
wenzelm@4705
   129
val scan_rest = Scan.any Symbol.not_eof >> implode;
wenzelm@388
   130
wenzelm@4705
   131
fun scan_token lex x =
wenzelm@4705
   132
  (case scan_tok lex x of
wenzelm@4705
   133
    ((Keyword, "ML", n), x') => (keep_line scan_rest >> token Verbatim (Some n)) x'
wenzelm@4705
   134
  | tok_x' => tok_x');
wenzelm@388
   135
wenzelm@388
   136
wenzelm@4705
   137
(* tokenize *)
wenzelm@4705
   138
wenzelm@6207
   139
fun tokenize lex chs =
wenzelm@388
   140
  let
wenzelm@4705
   141
    val scan_toks = Scan.repeat (scan_token lex);
wenzelm@4705
   142
    val ignore = fn (Ignore, _, _) => true | _ => false;
wenzelm@388
   143
  in
wenzelm@4938
   144
    (case Scan.error (Scan.finite' Symbol.stopper scan_toks) (Some 1, chs) of
wenzelm@4705
   145
      (toks, (n, [])) => filter_out ignore toks @ [token EOF n "end-of-file"]
wenzelm@5112
   146
    | (_, (n, cs)) => error (lex_err n ("Bad input " ^ quote (Symbol.beginning cs))))
wenzelm@388
   147
  end;
wenzelm@388
   148
wenzelm@388
   149
wenzelm@388
   150
end;