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