# HG changeset patch
# User wenzelm
# Date 1232143067 -3600
# Node ID e561d0915f28ae196788392c6ab5abd166547e9c
# Parent  e2b1fb731241cc9cfff4d200e89c2ef086e5708c
IsabelleProcess.parse_message (message markup within Scala layer);

diff -r e2b1fb731241 -r e561d0915f28 src/Tools/jEdit/src/jedit/ScrollerDockable.scala
--- a/src/Tools/jEdit/src/jedit/ScrollerDockable.scala	Fri Jan 16 22:57:24 2009 +0100
+++ b/src/Tools/jEdit/src/jedit/ScrollerDockable.scala	Fri Jan 16 22:57:47 2009 +0100
@@ -228,7 +228,7 @@
         fontResolver.setFontMapping("Isabelle", Isabelle.plugin.font)
       panel.relayout()
     })
-    val tree = YXML.parse_failsafe(Isabelle.symbols.decode(r.result))
+    val tree = IsabelleProcess.parse_message(r.kind, Isabelle.symbols.decode(r.result))
     val document = XML.document(tree)
     panel.setDocument(document, UserAgent.baseURL)
     val sa = new SelectionActions
diff -r e2b1fb731241 -r e561d0915f28 src/Tools/jEdit/src/prover/Prover.scala
--- a/src/Tools/jEdit/src/prover/Prover.scala	Fri Jan 16 22:57:24 2009 +0100
+++ b/src/Tools/jEdit/src/prover/Prover.scala	Fri Jan 16 22:57:47 2009 +0100
@@ -75,7 +75,7 @@
       }
     }
     else {
-      val tree = YXML.parse_failsafe(isabelle_symbols.decode(r.result))
+      val tree = IsabelleProcess.parse_message(r.kind, isabelle_symbols.decode(r.result))
       if (st == null || (st.status != Command.Status.REMOVED && st.status != Command.Status.REMOVE)) {
         r.kind match {