# HG changeset patch
# User wenzelm
# Date 1229779152 -3600
# Node ID bce2f2ea981963ffceed8e513dfb5d93f1363225
# Parent  283a974972b4709ae240bbccef42e77c44faec09
misc tuning and adaption according to original IsabelleParser --
  cf. http://isabelle.in.tum.de/repos/isabelle/file/b1c6f4563df7/lib/jedit/plugin/isabelle_parser.scala;

diff -r 283a974972b4 -r bce2f2ea9819 src/Tools/jEdit/src/prover/IsabelleSKParser.scala
--- a/src/Tools/jEdit/src/prover/IsabelleSKParser.scala	Sat Dec 20 13:27:48 2008 +0100
+++ b/src/Tools/jEdit/src/prover/IsabelleSKParser.scala	Sat Dec 20 14:19:12 2008 +0100
@@ -1,37 +1,60 @@
 /*
- * SideKick parser for proof document
+ * SideKick parser for Isabelle proof documents
  *
  * @author Fabian Immler, TU Munich
+ * @author Makarius
+ *
+ * TODO:
+ *   - locking of buffer and/or document model (!?)
+ *   - check treatment of assets
+ *   - completion support
+ *   - rename to isabelle.jedit.IsabelleSideKickParser
  */
 
 package isabelle.prover
 
-import isabelle.jedit.{Plugin}
-import sidekick.{SideKickParser, SideKickParsedData, IAsset}
-import org.gjt.sp.jedit.{Buffer, ServiceManager}
+
 import javax.swing.tree.DefaultMutableTreeNode
-import errorlist.DefaultErrorSource;
+
+import isabelle.jedit.Plugin
+
+import org.gjt.sp.jedit.{Buffer, EditPane}
+import errorlist.DefaultErrorSource
+import sidekick.{SideKickParser, SideKickParsedData, SideKickCompletion}
+
 
 class IsabelleSKParser extends SideKickParser("isabelle") {
-  
-  override def parse(b : Buffer,
-                     errorSource : DefaultErrorSource)
-    : SideKickParsedData = {
-      Plugin.plugin.prover_setup(b) match {
-        case None =>
-          val data = new SideKickParsedData("WARNING:")
-          data.root.add(new DefaultMutableTreeNode("can only parse buffer which is activated via IsabellePlugin -> activate"))
-          data
-        case Some(prover_setup) =>
-          val prover = prover_setup.prover
-          val document = prover.document
-          val data = new SideKickParsedData(b.getPath)
+
+  /* parsing */
+
+  private var stopped = false
+  override def stop () = { stopped = true }
 
-          for(command <- document.commands){
-            data.root.add(command.root_node.swing_node)
-          }
-          data
+  def parse(buffer : Buffer, error_source : DefaultErrorSource): SideKickParsedData = {
+    stopped = false
+    
+    val data = new SideKickParsedData(buffer.getName)
+    
+    Plugin.plugin.prover_setup(buffer) match {
+      case None =>
+        data.root.add(new DefaultMutableTreeNode("<buffer inactive>"))
+      case Some(prover_setup) =>
+        val document = prover_setup.prover.document
+        val commands = document.commands()
+        while (!stopped && commands.hasNext) {
+          data.root.add(commands.next.root_node.swing_node)
+        }
+        if (stopped) data.root.add(new DefaultMutableTreeNode("<parser stopped>"))
       }
-    }
+
+    data
+  }
+
 
+  /* completion */
+
+  override def supportsCompletion = true
+  override def canCompleteAnywhere = true
+
+  override def complete(pane: EditPane, caret: Int): SideKickCompletion = null
 }