IsabelleProcess.parse_message (message markup within Scala layer);
authorwenzelm
Fri, 16 Jan 2009 22:57:47 +0100
changeset 34477 e561d0915f28
parent 34476 e2b1fb731241
child 34479 c787cbe6cdce
IsabelleProcess.parse_message (message markup within Scala layer);
src/Tools/jEdit/src/jedit/ScrollerDockable.scala
src/Tools/jEdit/src/prover/Prover.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
--- 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 {