text_of: make double sure that result is well-formed, to avoid recurrent failures;

--- a/src/Pure/Isar/outer_lex.ML	Sat Dec 08 21:14:51 2007 +0100
+++ b/src/Pure/Isar/outer_lex.ML	Sat Dec 08 21:20:05 2007 +0100
@@ -162,7 +162,10 @@
   else
     let
       val k = str_of_kind (kind_of tok);
-      val s = unparse tok;
+      val txt = unparse tok;
+      val s =
+        if can Symbol.explode txt
+        then txt else Output.escape_malformed txt;
     in
       if s = "" then (k, "")
       else if size s < 40 andalso not (exists_string (fn c => c = "\n") s) then (k ^ " " ^ s, "")