# HG changeset patch
# User wenzelm
# Date 1197145205 -3600
# Node ID 655453e635c443c03cb7effa527cfdf15d36abe6
# Parent  f2b137c3e725c1fd29e7aa834d102affb99af93d
text_of: make double sure that result is well-formed, to avoid recurrent failures;

diff -r f2b137c3e725 -r 655453e635c4 src/Pure/Isar/outer_lex.ML
--- 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, "")