# HG changeset patch
# User wenzelm
# Date 1184102986 -7200
# Node ID aa088ef9237cd911f67c2aa9991ebf3f0741cebb
# Parent  d0d583c7a41f54bf2b79e1f3bc0fa9470463dbc6
added kind_of;
unparse: extra care for Malformed;

diff -r d0d583c7a41f -r aa088ef9237c src/Pure/Isar/outer_lex.ML
--- a/src/Pure/Isar/outer_lex.ML	Tue Jul 10 23:29:44 2007 +0200
+++ b/src/Pure/Isar/outer_lex.ML	Tue Jul 10 23:29:46 2007 +0200
@@ -17,6 +17,7 @@
   val not_eof: token -> bool
   val position_of: token -> Position.T
   val pos_of: token -> string
+  val kind_of: token -> token_kind
   val is_kind: token_kind -> token -> bool
   val keyword_with: (string -> bool) -> token -> bool
   val ident_with: (string -> bool) -> token -> bool
@@ -39,7 +40,7 @@
   val scan_string: Position.T * Symbol.symbol list -> string * (Position.T * Symbol.symbol list)
   val scan: (Scan.lexicon * Scan.lexicon) ->
     Position.T * Symbol.symbol list -> token * (Position.T * Symbol.symbol list)
-  val source: bool option -> (unit -> (Scan.lexicon * Scan.lexicon)) ->
+  val source: bool option -> (unit -> Scan.lexicon * Scan.lexicon) ->
     Position.T -> (Symbol.symbol, 'a) Source.source ->
     (token, Position.T * (Symbol.symbol, 'a) Source.source) Source.source
   val source_proper: (token, 'a) Source.source ->
@@ -104,6 +105,8 @@
 
 (* kind of token *)
 
+fun kind_of (Token (_, (k, _))) = k;
+
 fun is_kind k (Token (_, (k', _))) = k = k';
 
 fun keyword_with pred (Token (_, (Keyword, x))) = pred x
@@ -154,6 +157,7 @@
   | AltString => x |> enclose "`" "`" o escape "`"
   | Verbatim => x |> enclose "{*" "*}"
   | Comment => x |> enclose "(*" "*)"
+  | Malformed _ => Output.escape (implode (map Output.output (explode x)))
   | _ => x);
 
 fun val_of (Token (_, (_, x))) = x;