# HG changeset patch
# User wenzelm
# Date 1582036837 -3600
# Node ID 09c850e82258086f26d459b0814eeef8a1a6fc25
# Parent  35b2d407e558199b2e68fe1bc03d280671d7e237
more robust pretty printing of broken YXML, e.g. single "\^E";

diff -r 35b2d407e558 -r 09c850e82258 src/Pure/ML/ml_syntax.ML
--- a/src/Pure/ML/ml_syntax.ML	Mon Feb 17 20:49:47 2020 +0100
+++ b/src/Pure/ML/ml_syntax.ML	Tue Feb 18 15:40:37 2020 +0100
@@ -128,8 +128,9 @@
 fun pretty_string max_len str =
   let
     val body =
-      maps (fn XML.Elem _ => ["<markup>"] | XML.Text s => Symbol.explode s) (YXML.parse_body str)
-        handle Fail _ => Symbol.explode str;
+      if YXML.is_wellformed str then
+        maps (fn XML.Elem _ => ["<markup>"] | XML.Text s => Symbol.explode s) (YXML.parse_body str)
+      else Symbol.explode str;
     val body' =
       if length body <= max_len then body
       else take (Int.max (max_len, 0)) body @ ["..."];
diff -r 35b2d407e558 -r 09c850e82258 src/Pure/PIDE/yxml.ML
--- a/src/Pure/PIDE/yxml.ML	Mon Feb 17 20:49:47 2020 +0100
+++ b/src/Pure/PIDE/yxml.ML	Tue Feb 18 15:40:37 2020 +0100
@@ -29,6 +29,7 @@
   val parse_body: string -> XML.body
   val parse: string -> XML.tree
   val content_of: string -> string
+  val is_wellformed: string -> bool
 end;
 
 structure YXML: YXML =
@@ -158,5 +159,7 @@
 
 val content_of = parse_body #> XML.content_of;
 
+fun is_wellformed s = string_of_body (parse_body s) = s
+  handle Fail _ => false;
+
 end;
-