renamed isabelle.prover.IsabelleSKParser to isabelle.jedit.IsabelleSideKickParser;
authorwenzelm
Sat, 20 Dec 2008 18:17:39 +0100
changeset 34426 81f93e0f13b4
parent 34425 1a574ef87254
child 34427 46aff93a5863
renamed isabelle.prover.IsabelleSKParser to isabelle.jedit.IsabelleSideKickParser; tuned;
src/Tools/jEdit/plugin/services.xml
src/Tools/jEdit/src/jedit/IsabelleSideKickParser.scala
src/Tools/jEdit/src/prover/IsabelleSKParser.scala
--- a/src/Tools/jEdit/plugin/services.xml	Sat Dec 20 17:53:00 2008 +0100
+++ b/src/Tools/jEdit/plugin/services.xml	Sat Dec 20 18:17:39 2008 +0100
@@ -2,7 +2,7 @@
 <!DOCTYPE SERVICES SYSTEM "services.dtd">
 <SERVICES>
 	<SERVICE NAME="isabelle" CLASS="sidekick.SideKickParser">
-		new isabelle.prover.IsabelleSKParser();
+		new isabelle.jedit.IsabelleSideKickParser();
 	</SERVICE>
 	<SERVICE NAME="isabelle" CLASS="org.gjt.sp.jedit.io.VFS">
 		new isabelle.jedit.VFS();
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/jedit/IsabelleSideKickParser.scala	Sat Dec 20 18:17:39 2008 +0100
@@ -0,0 +1,52 @@
+/*
+ * SideKick parser for Isabelle proof documents
+ *
+ * @author Fabian Immler, TU Munich
+ * @author Makarius
+ */
+
+package isabelle.jedit
+
+
+import javax.swing.tree.DefaultMutableTreeNode
+
+import org.gjt.sp.jedit.{Buffer, EditPane}
+import errorlist.DefaultErrorSource
+import sidekick.{SideKickParser, SideKickParsedData, SideKickCompletion}
+
+
+class IsabelleSideKickParser extends SideKickParser("isabelle") {
+
+  /* parsing */
+
+  private var stopped = false
+  override def stop () = { stopped = true }
+
+  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  // TODO
+}
--- a/src/Tools/jEdit/src/prover/IsabelleSKParser.scala	Sat Dec 20 17:53:00 2008 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,60 +0,0 @@
-/*
- * 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 javax.swing.tree.DefaultMutableTreeNode
-
-import isabelle.jedit.Plugin
-
-import org.gjt.sp.jedit.{Buffer, EditPane}
-import errorlist.DefaultErrorSource
-import sidekick.{SideKickParser, SideKickParsedData, SideKickCompletion}
-
-
-class IsabelleSKParser extends SideKickParser("isabelle") {
-
-  /* parsing */
-
-  private var stopped = false
-  override def stop () = { stopped = true }
-
-  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
-}