# HG changeset patch
# User wenzelm
# Date 1087829398 -7200
# Node ID 26fb63c4acb5f6d116ee413a1e770c10ae7c681b
# Parent  582b655da757da0f0314ef102f07689cdc5c00fa
added unparse;

diff -r 582b655da757 -r 26fb63c4acb5 src/Pure/Isar/outer_lex.ML
--- a/src/Pure/Isar/outer_lex.ML	Mon Jun 21 16:41:06 2004 +0200
+++ b/src/Pure/Isar/outer_lex.ML	Mon Jun 21 16:49:58 2004 +0200
@@ -26,6 +26,7 @@
   val is_end_ignore: token -> bool
   val is_newline: token -> bool
   val is_indent: token -> bool
+  val unparse: token -> string
   val val_of: token -> string
   val is_sid: string -> bool
   val !!! : string -> (Position.T * 'a -> 'b) -> Position.T * 'a -> 'b
@@ -132,13 +133,20 @@
   | is_indent _ = false;
 
 
-(* name and value of token *)
+(* token content *)
 
 fun name_of (tok as Token (_, (k, x))) =
   if is_semicolon tok then "terminator"
   else if x = "" then str_of_kind k
   else str_of_kind k ^ " " ^ quote x;
 
+fun unparse (Token (_, (kind, x))) =
+  (case kind of
+    String => x |> translate_string (fn "\"" => "\\\"" | "\\" => "\\\\" | c => c) |> quote
+  | Verbatim => x |> enclose "{*" "*}"
+  | Comment => x |> enclose "(*" "*)"
+  | _ => x);
+
 fun val_of (Token (_, (_, x))) = x;
 
 fun token_leq (Token (_, (_, x)), Token (_, (_, x'))) = x <= x';