# HG changeset patch
# User wenzelm
# Date 1219525650 -7200
# Node ID 825286a7a3a4e303dce9f4dacf8b213c081cf0b8
# Parent  4557e77d4d3db0d2a65340ae5d6319fa6d3aefee
adapted to new IsabelleProcess from Pure.jar;
IsabellePlugin.result_content decodes symbols;

diff -r 4557e77d4d3d -r 825286a7a3a4 lib/jedit/plugin/isabelle/IsabelleDock.scala
--- a/lib/jedit/plugin/isabelle/IsabelleDock.scala	Sat Aug 23 23:07:28 2008 +0200
+++ b/lib/jedit/plugin/isabelle/IsabelleDock.scala	Sat Aug 23 23:07:30 2008 +0200
@@ -61,7 +61,7 @@
     val errorStyle = makeStyle("error", true, new Color(255, 160, 160))
 
     IsabellePlugin.addPermanentConsumer (result =>
-      if (result != null && !result.isSystem) {
+      if (result != null && !result.is_system) {
         SwingUtilities.invokeLater(new Runnable {
           def run = {
             val logic = IsabellePlugin.isabelle.session
@@ -70,13 +70,13 @@
 
             val doc = pane.getDocument.asInstanceOf[StyledDocument]
             val style = result.kind match {
-              case IsabelleProcess.Result.Kind.WARNING => warningStyle
-              case IsabelleProcess.Result.Kind.ERROR => errorStyle
-              case IsabelleProcess.Result.Kind.TRACING => infoStyle
-              case _ => if (result.isRaw) rawStyle else null
+              case IsabelleProcess.Kind.WARNING => warningStyle
+              case IsabelleProcess.Kind.ERROR => errorStyle
+              case IsabelleProcess.Kind.TRACING => infoStyle
+              case _ => if (result.is_raw) rawStyle else null
             }
-            doc.insertString(doc.getLength, result.result, style)
-            if (!result.isRaw) doc.insertString(doc.getLength, "\n", style)
+            doc.insertString(doc.getLength, IsabellePlugin.result_content(result), style)
+            if (!result.is_raw) doc.insertString(doc.getLength, "\n", style)
             pane.setCaretPosition(doc.getLength)
           }
         })
diff -r 4557e77d4d3d -r 825286a7a3a4 lib/jedit/plugin/isabelle/IsabellePlugin.scala
--- a/lib/jedit/plugin/isabelle/IsabellePlugin.scala	Sat Aug 23 23:07:28 2008 +0200
+++ b/lib/jedit/plugin/isabelle/IsabellePlugin.scala	Sat Aug 23 23:07:30 2008 +0200
@@ -7,18 +7,18 @@
 
 package isabelle
 
-import isabelle.IsabelleProcess
-
 import org.gjt.sp.jedit.EditPlugin
 import org.gjt.sp.util.Log
 
 import errorlist.DefaultErrorSource
 import errorlist.ErrorSource
 
-import scala.collection.mutable.ListBuffer
 import java.util.Properties
 import java.lang.NumberFormatException
 
+import scala.collection.mutable.ListBuffer
+import scala.io.Source
+
 
 /* Global state */
 
@@ -31,7 +31,7 @@
 
   def idProperties(value: String) : Properties = {
      val props = new Properties
-     props.setProperty("id", value)
+     props.setProperty(Markup.ID, value)
      props
   }
 
@@ -47,6 +47,11 @@
   var isabelle: IsabelleProcess = null
 
 
+  // result content
+  def result_content(result: IsabelleProcess.Result) =
+    XML.content(isabelle.result_tree(result)).mkString("")
+
+
   // result consumers
   type consumer = IsabelleProcess.Result => Boolean
   private var consumers = new ListBuffer[consumer]
@@ -84,32 +89,37 @@
 
     IsabellePlugin.addPermanentConsumer (result =>
       if (result != null && result.props != null &&
-          (result.kind == IsabelleProcess.Result.Kind.WARNING ||
-           result.kind == IsabelleProcess.Result.Kind.ERROR)) {
+          (result.kind == IsabelleProcess.Kind.WARNING ||
+           result.kind == IsabelleProcess.Kind.ERROR)) {
         val typ =
-          if (result.kind == IsabelleProcess.Result.Kind.WARNING) ErrorSource.WARNING
+          if (result.kind == IsabelleProcess.Kind.WARNING) ErrorSource.WARNING
           else ErrorSource.ERROR
-        val line = result.props.getProperty(IsabelleProcess.Property.LINE)
-        val file = result.props.getProperty(IsabelleProcess.Property.FILE)
-        if (line != null && file != null && result.result.length > 0) {
-          val msg = result.result.split("\n")
-          val err = new DefaultErrorSource.DefaultError(IsabellePlugin.errors,
-              typ, file, Integer.parseInt(line) - 1, 0, 0, msg(0))
-          for (i <- 1 to msg.length - 1)
-            err.addExtraMessage(msg(i))
-          IsabellePlugin.errors.addError(err)
+        (Position.line_of(result.props), Position.file_of(result.props)) match {
+          case (Some(line), Some(file)) =>
+            val content = IsabellePlugin.result_content(result)
+            if (content.length > 0) {
+              val lines = Source.fromString(content).getLines
+              val err = new DefaultErrorSource.DefaultError(IsabellePlugin.errors,
+                  typ, file, line - 1, 0, 0, lines.next)
+              for (msg <- lines) err.addExtraMessage(msg)
+              IsabellePlugin.errors.addError(err)
+            }
+          case _ =>
         }
       })
 
+
     // Isabelle process
-    IsabellePlugin.isabelle = new IsabelleProcess(Array("-m", "builtin_browser"), null)
+    IsabellePlugin.isabelle =
+      new IsabelleProcess("-mno_brackets", "-mno_type_brackets", "-mxsymbols")
     thread = new Thread (new Runnable {
       def run = {
         var result: IsabelleProcess.Result = null
         do {
           try {
-            result = IsabellePlugin.isabelle.results.take.asInstanceOf[IsabelleProcess.Result]
-          } catch {
+            result = IsabellePlugin.isabelle.results.take
+          }
+          catch {
             case _: NullPointerException => result = null
             case _: InterruptedException => result = null
           }
@@ -117,7 +127,7 @@
             System.err.println(result)   // FIXME
             IsabellePlugin.consume(result)
           }
-          if (result.kind == IsabelleProcess.Result.Kind.EXIT) {
+          if (result.kind == IsabelleProcess.Kind.EXIT) {
             result = null
             IsabellePlugin.consume(null)
           }
@@ -136,4 +146,3 @@
     IsabellePlugin.errors = null
   }
 }
-