rearranged source files;
authorwenzelm
Sun, 24 Aug 2008 19:02:22 +0200
changeset 27987 c3f7fa72af2a
parent 27986 26e1a7a6695d
child 27988 efc6d38d16d2
rearranged source files;
lib/jedit/plugin/isabelle/IsabelleDock.scala
lib/jedit/plugin/isabelle/IsabelleParser.scala
lib/jedit/plugin/isabelle/IsabellePlugin.scala
lib/jedit/plugin/isabelle_dock.scala
lib/jedit/plugin/isabelle_parser.scala
lib/jedit/plugin/isabelle_plugin.scala
lib/jedit/plugin/mk
--- a/lib/jedit/plugin/isabelle/IsabelleDock.scala	Sun Aug 24 18:57:43 2008 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,152 +0,0 @@
-/*  Title:      jedit/plugin/IsabelleDock.scala
-    ID:         $Id$
-    Author:     Makarius
-
-Dockable window for Isabelle process control.
-*/
-
-package isabelle.jedit
-
-import org.gjt.sp.jedit.View
-import org.gjt.sp.jedit.gui.DefaultFocusComponent
-import org.gjt.sp.jedit.gui.DockableWindowManager
-import org.gjt.sp.jedit.gui.RolloverButton
-import org.gjt.sp.jedit.gui.HistoryTextField
-import org.gjt.sp.jedit.GUIUtilities
-
-import java.awt.Color
-import java.awt.Insets
-import java.awt.BorderLayout
-import java.awt.Dimension
-import java.awt.event.ActionListener
-import java.awt.event.ActionEvent
-import javax.swing.BoxLayout
-import javax.swing.JPanel
-import javax.swing.JScrollPane
-import javax.swing.JTextPane
-import javax.swing.text.{StyledDocument, StyleConstants}
-import javax.swing.SwingUtilities
-import javax.swing.Icon
-import javax.swing.Box
-import javax.swing.JTextField
-import javax.swing.JComboBox
-import javax.swing.DefaultComboBoxModel
-
-
-class IsabelleDock(view: View, position: String)
-    extends JPanel(new BorderLayout) with DefaultFocusComponent
-{
-  private val text = new HistoryTextField("isabelle", false, true)
-  private val logicCombo = new JComboBox
-
-  {
-    // output pane
-    val pane = new JTextPane
-    pane.setEditable(false)
-    add(BorderLayout.CENTER, new JScrollPane(pane))
-    if (position == DockableWindowManager.FLOATING)
-      setPreferredSize(new Dimension(1000, 500))
-
-    val doc = pane.getDocument.asInstanceOf[StyledDocument]
-
-    def makeStyle(name: String, bg: Boolean, color: Color) = {
-      val style = doc.addStyle(name, null)
-      if (bg) StyleConstants.setBackground(style, color)
-      else StyleConstants.setForeground(style, color)
-      style
-    }
-    val rawStyle = makeStyle("raw", false, Color.GRAY)
-    val infoStyle = makeStyle("info", true, new Color(160, 255, 160))
-    val warningStyle = makeStyle("warning", true, new Color(255, 255, 160))
-    val errorStyle = makeStyle("error", true, new Color(255, 160, 160))
-
-    IsabellePlugin.addPermanentConsumer (result =>
-      if (result != null && !result.is_system) {
-        SwingUtilities.invokeLater(new Runnable {
-          def run = {
-            val logic = IsabellePlugin.isabelle.session
-            logicCombo.setModel(new DefaultComboBoxModel(Array(logic).asInstanceOf[Array[AnyRef]]))
-            logicCombo.setPrototypeDisplayValue("AAAA")  // FIXME ??
-
-            val doc = pane.getDocument.asInstanceOf[StyledDocument]
-            val style = result.kind match {
-              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, IsabellePlugin.result_content(result), style)
-            if (!result.is_raw) doc.insertString(doc.getLength, "\n", style)
-            pane.setCaretPosition(doc.getLength)
-          }
-        })
-      })
-
-
-    // control box
-    val box = new Box(BoxLayout.X_AXIS)
-    add(BorderLayout.SOUTH, box)
-
-
-    // logic combo
-    logicCombo.setToolTipText("Isabelle logics")
-    logicCombo.setRequestFocusEnabled(false)
-    logicCombo.setModel(new DefaultComboBoxModel(Array("default").asInstanceOf[Array[AnyRef]]))
-    box.add(logicCombo)
-
-
-    // mode combo
-    val modeIsar = "Isar"
-    val modeML = "ML"
-    val modes = Array(modeIsar, modeML)
-    var mode = modeIsar
-
-    val modeCombo = new JComboBox
-    modeCombo.setToolTipText("Toplevel mode")
-    modeCombo.setRequestFocusEnabled(false)
-    modeCombo.setModel(new DefaultComboBoxModel(modes.asInstanceOf[Array[AnyRef]]))
-    modeCombo.setPrototypeDisplayValue("AAAA")
-    modeCombo.addActionListener(new ActionListener {
-      def actionPerformed(evt: ActionEvent): Unit = {
-        mode = modeCombo.getSelectedItem.asInstanceOf[String]
-      }
-    })
-    box.add(modeCombo)
-
-
-    // input field
-    text.setToolTipText("Command line")
-    text.addActionListener(new ActionListener {
-      def actionPerformed(evt: ActionEvent): Unit = {
-        val command = text.getText
-        if (command.length > 0) {
-          if (mode == modeIsar)
-            IsabellePlugin.isabelle.command(command)
-          else if (mode == modeML)
-            IsabellePlugin.isabelle.ML(command)
-          text.setText("")
-        }
-      }
-    })
-    box.add(text)
-
-
-    // buttons
-    def iconButton(icon: String, tip: String, action: => Unit) = {
-      val button = new RolloverButton(GUIUtilities.loadIcon(icon))
-      button.setToolTipText(tip)
-      button.setMargin(new Insets(0,0,0,0))
-      button.setRequestFocusEnabled(false)
-      button.addActionListener(new ActionListener {
-        def actionPerformed(evt: ActionEvent): Unit = action
-      })
-      box.add(button)
-    }
-
-    iconButton("Cancel.png", "Stop", IsabellePlugin.isabelle.interrupt)
-    iconButton("Clear.png", "Clear", pane.setText(""))
-  }
-
-  def focusOnDefaultComponent: Unit = text.requestFocus
-}
-
--- a/lib/jedit/plugin/isabelle/IsabelleParser.scala	Sun Aug 24 18:57:43 2008 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,61 +0,0 @@
-/*  Title:      jedit/plugin/IsabelleParser.scala
-    ID:         $Id$
-    Author:     Makarius
-
-Isabelle parser setup for Sidekick plugin.
-*/
-
-package isabelle.jedit
-
-import javax.swing.text.Position
-import javax.swing.tree.DefaultMutableTreeNode
-import javax.swing.tree.DefaultTreeModel
-
-import org.gjt.sp.jedit.Buffer
-import org.gjt.sp.util.Log
-
-import sidekick.Asset
-import sidekick.SideKickParsedData
-import sidekick.SideKickParser
-import errorlist.DefaultErrorSource
-
-
-private class IsabelleAsset(name: String, content: String) extends Asset(name)
-{
-  override def getShortString() = { name }
-  override def getLongString() = { content }
-  override def getIcon() = { null }
-}
-
-
-class IsabelleParser extends SideKickParser("isabelle") {
-  private var stopped = false
-
-  override def stop () { stopped = true }
-
-  def parse(buffer: Buffer, e: DefaultErrorSource): SideKickParsedData = {
-    stopped = false
-
-    var text: String = null
-    var data: SideKickParsedData = null
-
-    try {
-      buffer.readLock()
-      text = buffer.getText(0, buffer.getLength())
-      data = new SideKickParsedData(buffer.getName())
-
-      val asset = new IsabelleAsset("theory", null)
-      asset.setStart(buffer.createPosition(0))
-      asset.setEnd(buffer.createPosition(buffer.getLength()))
-
-      val node = new DefaultMutableTreeNode(asset)
-      data.root.insert(node, node.getChildCount())
-
-    } finally {
-      buffer.readUnlock()
-    }
-
-    data
-  }
-}
-
--- a/lib/jedit/plugin/isabelle/IsabellePlugin.scala	Sun Aug 24 18:57:43 2008 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,148 +0,0 @@
-/*  Title:      jedit/plugin/IsabellePlugin.scala
-    ID:         $Id$
-    Author:     Makarius
-
-Isabelle/jEdit plugin -- main setup.
-*/
-
-package isabelle.jedit
-
-import org.gjt.sp.jedit.EditPlugin
-import org.gjt.sp.util.Log
-
-import errorlist.DefaultErrorSource
-import errorlist.ErrorSource
-
-import java.util.Properties
-import java.lang.NumberFormatException
-
-import scala.collection.mutable.ListBuffer
-import scala.io.Source
-
-
-/* Global state */
-
-object IsabellePlugin {
-  // unique ids
-  @volatile
-  private var idCount = 0
-
-  def id() : String = synchronized { idCount += 1; "jedit:" + idCount }
-
-  def idProperties(value: String) : Properties = {
-     val props = new Properties
-     props.setProperty(Markup.ID, value)
-     props
-  }
-
-  def idProperties() : Properties = { idProperties(id()) }
-
-
-  // the error source
-  @volatile
-  var errors: DefaultErrorSource = null
-
-  // the Isabelle process
-  @volatile
-  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]
-
-  def addConsumer(consumer: consumer) = synchronized { consumers += consumer }
-
-  def addPermanentConsumer(consumer: IsabelleProcess.Result => Unit) = {
-    addConsumer(result => { consumer(result); false })
-  }
-
-  def delConsumer(consumer: consumer) = synchronized { consumers -= consumer }
-
-  def consume(result: IsabelleProcess.Result) : Unit = {
-    synchronized { consumers.elements.toList } foreach (consumer =>
-      {
-        val finished =
-          try { consumer(result) }
-          catch { case e: Throwable => Log.log(Log.ERROR, this, e); true }
-        if (finished || result == null)
-          delConsumer(consumer)
-      })
-  }
-}
-
-
-/* Main plugin setup */
-
-class IsabellePlugin extends EditPlugin {
-  private var thread: Thread = null
-
-  override def start = {
-    // error source
-    IsabellePlugin.errors = new DefaultErrorSource("isabelle")
-    ErrorSource.registerErrorSource(IsabellePlugin.errors)
-
-    IsabellePlugin.addPermanentConsumer (result =>
-      if (result != null && result.props != null &&
-          (result.kind == IsabelleProcess.Kind.WARNING ||
-           result.kind == IsabelleProcess.Kind.ERROR)) {
-        val typ =
-          if (result.kind == IsabelleProcess.Kind.WARNING) ErrorSource.WARNING
-          else ErrorSource.ERROR
-        (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("-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
-          }
-          catch {
-            case _: NullPointerException => result = null
-            case _: InterruptedException => result = null
-          }
-          if (result != null) {
-            System.err.println(result)   // FIXME
-            IsabellePlugin.consume(result)
-          }
-          if (result.kind == IsabelleProcess.Kind.EXIT) {
-            result = null
-            IsabellePlugin.consume(null)
-          }
-        } while (result != null)
-      }
-    })
-    thread.start
-  }
-
-  override def stop = {
-    IsabellePlugin.isabelle.kill
-    thread.interrupt; thread.join; thread = null
-    IsabellePlugin.isabelle = null
-
-    ErrorSource.unregisterErrorSource(IsabellePlugin.errors)
-    IsabellePlugin.errors = null
-  }
-}
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/lib/jedit/plugin/isabelle_dock.scala	Sun Aug 24 19:02:22 2008 +0200
@@ -0,0 +1,152 @@
+/*  Title:      lib/jedit/plugin/isabelle_dock.scala
+    ID:         $Id$
+    Author:     Makarius
+
+Dockable window for Isabelle process control.
+*/
+
+package isabelle.jedit
+
+import org.gjt.sp.jedit.View
+import org.gjt.sp.jedit.gui.DefaultFocusComponent
+import org.gjt.sp.jedit.gui.DockableWindowManager
+import org.gjt.sp.jedit.gui.RolloverButton
+import org.gjt.sp.jedit.gui.HistoryTextField
+import org.gjt.sp.jedit.GUIUtilities
+
+import java.awt.Color
+import java.awt.Insets
+import java.awt.BorderLayout
+import java.awt.Dimension
+import java.awt.event.ActionListener
+import java.awt.event.ActionEvent
+import javax.swing.BoxLayout
+import javax.swing.JPanel
+import javax.swing.JScrollPane
+import javax.swing.JTextPane
+import javax.swing.text.{StyledDocument, StyleConstants}
+import javax.swing.SwingUtilities
+import javax.swing.Icon
+import javax.swing.Box
+import javax.swing.JTextField
+import javax.swing.JComboBox
+import javax.swing.DefaultComboBoxModel
+
+
+class IsabelleDock(view: View, position: String)
+    extends JPanel(new BorderLayout) with DefaultFocusComponent
+{
+  private val text = new HistoryTextField("isabelle", false, true)
+  private val logicCombo = new JComboBox
+
+  {
+    // output pane
+    val pane = new JTextPane
+    pane.setEditable(false)
+    add(BorderLayout.CENTER, new JScrollPane(pane))
+    if (position == DockableWindowManager.FLOATING)
+      setPreferredSize(new Dimension(1000, 500))
+
+    val doc = pane.getDocument.asInstanceOf[StyledDocument]
+
+    def makeStyle(name: String, bg: Boolean, color: Color) = {
+      val style = doc.addStyle(name, null)
+      if (bg) StyleConstants.setBackground(style, color)
+      else StyleConstants.setForeground(style, color)
+      style
+    }
+    val rawStyle = makeStyle("raw", false, Color.GRAY)
+    val infoStyle = makeStyle("info", true, new Color(160, 255, 160))
+    val warningStyle = makeStyle("warning", true, new Color(255, 255, 160))
+    val errorStyle = makeStyle("error", true, new Color(255, 160, 160))
+
+    IsabellePlugin.addPermanentConsumer (result =>
+      if (result != null && !result.is_system) {
+        SwingUtilities.invokeLater(new Runnable {
+          def run = {
+            val logic = IsabellePlugin.isabelle.session
+            logicCombo.setModel(new DefaultComboBoxModel(Array(logic).asInstanceOf[Array[AnyRef]]))
+            logicCombo.setPrototypeDisplayValue("AAAA")  // FIXME ??
+
+            val doc = pane.getDocument.asInstanceOf[StyledDocument]
+            val style = result.kind match {
+              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, IsabellePlugin.result_content(result), style)
+            if (!result.is_raw) doc.insertString(doc.getLength, "\n", style)
+            pane.setCaretPosition(doc.getLength)
+          }
+        })
+      })
+
+
+    // control box
+    val box = new Box(BoxLayout.X_AXIS)
+    add(BorderLayout.SOUTH, box)
+
+
+    // logic combo
+    logicCombo.setToolTipText("Isabelle logics")
+    logicCombo.setRequestFocusEnabled(false)
+    logicCombo.setModel(new DefaultComboBoxModel(Array("default").asInstanceOf[Array[AnyRef]]))
+    box.add(logicCombo)
+
+
+    // mode combo
+    val modeIsar = "Isar"
+    val modeML = "ML"
+    val modes = Array(modeIsar, modeML)
+    var mode = modeIsar
+
+    val modeCombo = new JComboBox
+    modeCombo.setToolTipText("Toplevel mode")
+    modeCombo.setRequestFocusEnabled(false)
+    modeCombo.setModel(new DefaultComboBoxModel(modes.asInstanceOf[Array[AnyRef]]))
+    modeCombo.setPrototypeDisplayValue("AAAA")
+    modeCombo.addActionListener(new ActionListener {
+      def actionPerformed(evt: ActionEvent): Unit = {
+        mode = modeCombo.getSelectedItem.asInstanceOf[String]
+      }
+    })
+    box.add(modeCombo)
+
+
+    // input field
+    text.setToolTipText("Command line")
+    text.addActionListener(new ActionListener {
+      def actionPerformed(evt: ActionEvent): Unit = {
+        val command = text.getText
+        if (command.length > 0) {
+          if (mode == modeIsar)
+            IsabellePlugin.isabelle.command(command)
+          else if (mode == modeML)
+            IsabellePlugin.isabelle.ML(command)
+          text.setText("")
+        }
+      }
+    })
+    box.add(text)
+
+
+    // buttons
+    def iconButton(icon: String, tip: String, action: => Unit) = {
+      val button = new RolloverButton(GUIUtilities.loadIcon(icon))
+      button.setToolTipText(tip)
+      button.setMargin(new Insets(0,0,0,0))
+      button.setRequestFocusEnabled(false)
+      button.addActionListener(new ActionListener {
+        def actionPerformed(evt: ActionEvent): Unit = action
+      })
+      box.add(button)
+    }
+
+    iconButton("Cancel.png", "Stop", IsabellePlugin.isabelle.interrupt)
+    iconButton("Clear.png", "Clear", pane.setText(""))
+  }
+
+  def focusOnDefaultComponent: Unit = text.requestFocus
+}
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/lib/jedit/plugin/isabelle_parser.scala	Sun Aug 24 19:02:22 2008 +0200
@@ -0,0 +1,61 @@
+/*  Title:      lib/jedit/plugin/isabelle_parser.scala
+    ID:         $Id$
+    Author:     Makarius
+
+Isabelle parser setup for Sidekick plugin.
+*/
+
+package isabelle.jedit
+
+import javax.swing.text.Position
+import javax.swing.tree.DefaultMutableTreeNode
+import javax.swing.tree.DefaultTreeModel
+
+import org.gjt.sp.jedit.Buffer
+import org.gjt.sp.util.Log
+
+import sidekick.Asset
+import sidekick.SideKickParsedData
+import sidekick.SideKickParser
+import errorlist.DefaultErrorSource
+
+
+private class IsabelleAsset(name: String, content: String) extends Asset(name)
+{
+  override def getShortString() = { name }
+  override def getLongString() = { content }
+  override def getIcon() = { null }
+}
+
+
+class IsabelleParser extends SideKickParser("isabelle") {
+  private var stopped = false
+
+  override def stop () { stopped = true }
+
+  def parse(buffer: Buffer, e: DefaultErrorSource): SideKickParsedData = {
+    stopped = false
+
+    var text: String = null
+    var data: SideKickParsedData = null
+
+    try {
+      buffer.readLock()
+      text = buffer.getText(0, buffer.getLength())
+      data = new SideKickParsedData(buffer.getName())
+
+      val asset = new IsabelleAsset("theory", null)
+      asset.setStart(buffer.createPosition(0))
+      asset.setEnd(buffer.createPosition(buffer.getLength()))
+
+      val node = new DefaultMutableTreeNode(asset)
+      data.root.insert(node, node.getChildCount())
+
+    } finally {
+      buffer.readUnlock()
+    }
+
+    data
+  }
+}
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/lib/jedit/plugin/isabelle_plugin.scala	Sun Aug 24 19:02:22 2008 +0200
@@ -0,0 +1,148 @@
+/*  Title:      lib/jedit/plugin/isabelle_plugin.scala
+    ID:         $Id$
+    Author:     Makarius
+
+Isabelle/jEdit plugin -- main setup.
+*/
+
+package isabelle.jedit
+
+import org.gjt.sp.jedit.EditPlugin
+import org.gjt.sp.util.Log
+
+import errorlist.DefaultErrorSource
+import errorlist.ErrorSource
+
+import java.util.Properties
+import java.lang.NumberFormatException
+
+import scala.collection.mutable.ListBuffer
+import scala.io.Source
+
+
+/* Global state */
+
+object IsabellePlugin {
+  // unique ids
+  @volatile
+  private var idCount = 0
+
+  def id() : String = synchronized { idCount += 1; "jedit:" + idCount }
+
+  def idProperties(value: String) : Properties = {
+     val props = new Properties
+     props.setProperty(Markup.ID, value)
+     props
+  }
+
+  def idProperties() : Properties = { idProperties(id()) }
+
+
+  // the error source
+  @volatile
+  var errors: DefaultErrorSource = null
+
+  // the Isabelle process
+  @volatile
+  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]
+
+  def addConsumer(consumer: consumer) = synchronized { consumers += consumer }
+
+  def addPermanentConsumer(consumer: IsabelleProcess.Result => Unit) = {
+    addConsumer(result => { consumer(result); false })
+  }
+
+  def delConsumer(consumer: consumer) = synchronized { consumers -= consumer }
+
+  def consume(result: IsabelleProcess.Result) : Unit = {
+    synchronized { consumers.elements.toList } foreach (consumer =>
+      {
+        val finished =
+          try { consumer(result) }
+          catch { case e: Throwable => Log.log(Log.ERROR, this, e); true }
+        if (finished || result == null)
+          delConsumer(consumer)
+      })
+  }
+}
+
+
+/* Main plugin setup */
+
+class IsabellePlugin extends EditPlugin {
+  private var thread: Thread = null
+
+  override def start = {
+    // error source
+    IsabellePlugin.errors = new DefaultErrorSource("isabelle")
+    ErrorSource.registerErrorSource(IsabellePlugin.errors)
+
+    IsabellePlugin.addPermanentConsumer (result =>
+      if (result != null && result.props != null &&
+          (result.kind == IsabelleProcess.Kind.WARNING ||
+           result.kind == IsabelleProcess.Kind.ERROR)) {
+        val typ =
+          if (result.kind == IsabelleProcess.Kind.WARNING) ErrorSource.WARNING
+          else ErrorSource.ERROR
+        (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("-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
+          }
+          catch {
+            case _: NullPointerException => result = null
+            case _: InterruptedException => result = null
+          }
+          if (result != null) {
+            System.err.println(result)   // FIXME
+            IsabellePlugin.consume(result)
+          }
+          if (result.kind == IsabelleProcess.Kind.EXIT) {
+            result = null
+            IsabellePlugin.consume(null)
+          }
+        } while (result != null)
+      }
+    })
+    thread.start
+  }
+
+  override def stop = {
+    IsabellePlugin.isabelle.kill
+    thread.interrupt; thread.join; thread = null
+    IsabellePlugin.isabelle = null
+
+    ErrorSource.unregisterErrorSource(IsabellePlugin.errors)
+    IsabellePlugin.errors = null
+  }
+}
--- a/lib/jedit/plugin/mk	Sun Aug 24 18:57:43 2008 +0200
+++ b/lib/jedit/plugin/mk	Sun Aug 24 19:02:22 2008 +0200
@@ -10,9 +10,9 @@
 
 scalac -d build \
   -cp $JEDIT_HOME/jedit.jar:$PLUGINS/SideKick.jar:$PLUGINS/ErrorList.jar:$PLUGINS/Console.jar:../../classes/Pure.jar \
-  isabelle/IsabellePlugin.scala \
-  isabelle/IsabelleDock.scala \
-  isabelle/IsabelleParser.scala \
+  isabelle_plugin.scala \
+  isabelle_dock.scala \
+  isabelle_parser.scala \
 && (
   cp *.xml *.props build/
   cd build