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