# HG changeset patch # User wenzelm # Date 1229793459 -3600 # Node ID 81f93e0f13b40c01ae134c5bc7119af9f128f600 # Parent 1a574ef872547ff8e9ce4808c3357d870d51d0cc renamed isabelle.prover.IsabelleSKParser to isabelle.jedit.IsabelleSideKickParser; tuned; diff -r 1a574ef87254 -r 81f93e0f13b4 src/Tools/jEdit/plugin/services.xml --- 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 @@ - new isabelle.prover.IsabelleSKParser(); + new isabelle.jedit.IsabelleSideKickParser(); new isabelle.jedit.VFS(); diff -r 1a574ef87254 -r 81f93e0f13b4 src/Tools/jEdit/src/jedit/IsabelleSideKickParser.scala --- /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("")) + 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("")) + } + + data + } + + + /* completion */ + + override def supportsCompletion = true + override def canCompleteAnywhere = true + + override def complete(pane: EditPane, caret: Int): SideKickCompletion = null // TODO +} diff -r 1a574ef87254 -r 81f93e0f13b4 src/Tools/jEdit/src/prover/IsabelleSKParser.scala --- 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("")) - 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("")) - } - - data - } - - - /* completion */ - - override def supportsCompletion = true - override def canCompleteAnywhere = true - - override def complete(pane: EditPane, caret: Int): SideKickCompletion = null -}