--- a/src/Tools/jEdit/build.xml Fri Dec 19 11:25:06 2008 +0100
+++ b/src/Tools/jEdit/build.xml Sat Jan 10 17:59:23 2009 +0100
@@ -70,6 +70,6 @@
<copy file="plugin/services.xml" todir="${build.classes.dir}" />
<copy file="plugin/dockables.xml" todir="${build.classes.dir}" />
<copy file="plugin/actions.xml" todir="${build.classes.dir}" />
- <copy file="plugin/IsabellePlugin.props" todir="${build.classes.dir}" />
+ <copy file="plugin/Isabelle.props" todir="${build.classes.dir}" />
</target>
</project>
--- a/src/Tools/jEdit/dist-template/interface Fri Dec 19 11:25:06 2008 +0100
+++ b/src/Tools/jEdit/dist-template/interface Sat Jan 10 17:59:23 2009 +0100
@@ -11,7 +11,7 @@
echo
echo " Options are:"
echo " -J OPTION add JVM runtime option"
- echo " (default JEDIT_JAVE_OPTIONS=$JEDIT_JAVE_OPTIONS)"
+ echo " (default JEDIT_JAVA_OPTIONS=$JEDIT_JAVA_OPTIONS)"
echo " -j OPTION add jEdit runtime option"
echo " (default JEDIT_OPTIONS=$JEDIT_OPTIONS)"
echo " -l NAME logic image name (default ISABELLE_LOGIC=$ISABELLE_LOGIC)"
@@ -67,12 +67,13 @@
# args
-FILES=""
+unset FILES; declare -a FILES
+
if [ "$#" -eq 0 ]; then
- FILES="isabelle:$HOME/Scratch.thy"
+ FILES[0]="isabelle:$HOME/Scratch.thy"
else
while [ "$#" -gt 0 ]; do
- FILES="$FILES 'isabelle:$1'"
+ FILES[${#FILES[@]}]="isabelle:$1"
shift
done
fi
@@ -92,4 +93,4 @@
exec "$ISABELLE_TOOL" java $JEDIT_JAVA_OPTIONS \
-jar "$(jvmpath "$JEDIT_HOME/jedit.jar")" \
- "-settings=$(jvmpath "$ISABELLE_HOME_USER/jedit")" $JEDIT_OPTIONS $FILES
+ "-settings=$(jvmpath "$ISABELLE_HOME_USER/jedit")" $JEDIT_OPTIONS "${FILES[@]}"
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/dist-template/modes/isabelle.xml Sat Jan 10 17:59:23 2009 +0100
@@ -0,0 +1,43 @@
+<?xml version="1.0"?>
+<!DOCTYPE MODE SYSTEM "xmode.dtd">
+
+<!-- Isabelle theory mode -->
+<MODE>
+ <PROPS>
+ <PROPERTY NAME="commentStart" VALUE="(*"/>
+ <PROPERTY NAME="commentEnd" VALUE="*)"/>
+ <PROPERTY NAME="noWordSep" VALUE="_'.?"/>
+ <PROPERTY NAME="indentOpenBrackets" VALUE="{"/>
+ <PROPERTY NAME="indentCloseBrackets" VALUE="}"/>
+ <PROPERTY NAME="unalignedOpenBrackets" VALUE="(" />
+ <PROPERTY NAME="unalignedCloseBrackets" VALUE=")" />
+ <PROPERTY NAME="tabSize" VALUE="2" />
+ <PROPERTY NAME="indentSize" VALUE="2" />
+ </PROPS>
+ <RULES IGNORE_CASE="FALSE" HIGHLIGHT_DIGITS="FALSE" ESCAPE="\">
+ <SPAN TYPE="COMMENT1">
+ <BEGIN>(*</BEGIN>
+ <END>*)</END>
+ </SPAN>
+ <SPAN TYPE="COMMENT3">
+ <BEGIN>{*</BEGIN>
+ <END>*}</END>
+ </SPAN>
+ <SPAN TYPE="LITERAL1">
+ <BEGIN>`</BEGIN>
+ <END>`</END>
+ </SPAN>
+ <SPAN TYPE="LITERAL3">
+ <BEGIN>"</BEGIN>
+ <END>"</END>
+ </SPAN>
+ <KEYWORDS>
+ <LABEL>header</LABEL>
+ <KEYWORD3>theory</KEYWORD3>
+ <KEYWORD4>imports</KEYWORD4>
+ <KEYWORD4>uses</KEYWORD4>
+ <KEYWORD4>begin</KEYWORD4>
+ <KEYWORD4>end</KEYWORD4>
+ </KEYWORDS>
+ </RULES>
+</MODE>
--- a/src/Tools/jEdit/dist-template/properties/jedit.props Fri Dec 19 11:25:06 2008 +0100
+++ b/src/Tools/jEdit/dist-template/properties/jedit.props Sat Jan 10 17:59:23 2009 +0100
@@ -21,3 +21,7 @@
view.gutter.fontsize=12
view.middleMousePaste=true
view.showToolbar=false
+buffer.sidekick.keystroke-parse=true
+sidekick.buffer-save-parse=true
+sidekick-tree.dock-position=right
+isabelle-state.dock-position=bottom
--- a/src/Tools/jEdit/makedist Fri Dec 19 11:25:06 2008 +0100
+++ b/src/Tools/jEdit/makedist Sat Jan 10 17:59:23 2009 +0100
@@ -11,7 +11,7 @@
## diagnostics
-JEDIT_HOME="/home/isajedit/jedit-orig/4.3pre15"
+JEDIT_HOME="/home/isajedit/jedit-orig/4.3pre16"
SCALA_HOME="/home/scala/current"
function usage()
@@ -84,12 +84,19 @@
[ "$JEDIT_HOME/jedit.jar" ] || fail "Bad original jEdit directory: $JEDIT_HOME"
cp -R "$JEDIT_HOME/." "$JEDIT/."
+rm -rf "$JEDIT/jEdit"
+
+mkdir "$JEDIT/jars"
[ "$SCALA_HOME/lib/scala-library.jar" ] || fail "Bad Scala directory: $SCALA_HOME"
cp "$SCALA_HOME/lib/scala-library.jar" "$JEDIT/jars/"
cp -R "$THIS/dist-template/." "$JEDIT/."
+perl -i -e 'while (<>) { if (m/NAME="javacc"/) {
+ print qq,<MODE NAME="isabelle" FILE="isabelle.xml" FILE_NAME_GLOB="*.thy"/>\n\n,; }
+ print; }' "$JEDIT/modes/catalog"
+
cp jars/Isabelle-jEdit.jar "$JEDIT/jars/isabelle.jar"
cp jars/lib/Pure.jar "$JEDIT/jars/isabelle-Pure.jar"
cp jars/lib/core-renderer.jar "$JEDIT/jars/"
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/plugin/Isabelle.props Sat Jan 10 17:59:23 2009 +0100
@@ -0,0 +1,44 @@
+## Isabelle plugin properties
+
+#identification
+plugin.isabelle.jedit.Plugin.name=Isabelle
+plugin.isabelle.jedit.Plugin.author=Johannes Hölzl, Fabian Immler, Makarius Wenzel
+plugin.isabelle.jedit.Plugin.version=0.0.1
+plugin.isabelle.jedit.Plugin.description=Isabelle/Isar live document editing
+
+#system parameters
+plugin.isabelle.jedit.Plugin.activate=defer
+plugin.isabelle.jedit.Plugin.usePluginHome=false
+plugin.isabelle.jedit.Plugin.jars=isabelle-Pure.jar core-renderer.jar scala-library.jar
+
+#dependencies
+plugin.isabelle.jedit.Plugin.depend.0=jdk 1.5
+plugin.isabelle.jedit.Plugin.depend.1=jedit 04.03.14.00
+plugin.isabelle.jedit.Plugin.depend.2=plugin errorlist.ErrorListPlugin 1.7
+plugin.isabelle.jedit.Plugin.depend.3=plugin sidekick.SideKickPlugin 0.7.6
+
+#options
+plugin.isabelle.jedit.Plugin.option-pane=isabelle
+options.isabelle.label=Isabelle
+options.isabelle.code=new isabelle.jedit.OptionPane();
+options.isabelle.font-path.title=Font Path
+options.isabelle.font-size.title=Font Size
+options.isabelle.font-size=14
+
+#menu actions
+plugin.isabelle.jedit.Plugin.menu.label=Isabelle
+plugin.isabelle.jedit.Plugin.menu=isabelle.activate isabelle.show-state isabelle.show-output isabelle.show-scroller
+isabelle.activate.label=Activate current buffer
+isabelle.show-state.label=Show State
+isabelle.show-output.label=Show Output
+isabelle.show-scroller.label=Show Scroller
+
+#dockables
+isabelle-output.title=Isabelle Output
+isabelle-state.title=Isabelle State
+isabelle-scroller.title=Isabelle Scroller
+
+#SideKick
+sidekick.parser.isabelle.label=Isabelle
+mode.isabelle.sidekick.parser=isabelle
+mode.ml.sidekick.parser=isabelle
--- a/src/Tools/jEdit/plugin/IsabellePlugin.ant Fri Dec 19 11:25:06 2008 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,10 +0,0 @@
-<?xml version="1.0"?>
-<project name="IsabellePlugin installer" default="install" basedir=".">
- <target name="install">
- <copy file="services.xml" todir="bin" />
- <copy file="dockables.xml" todir="bin" />
- <copy file="actions.xml" todir="bin" />
- <copy file="IsabellePlugin.props" todir="bin" />
- <jar destfile="IsabellePlugin.jar" basedir="bin" />
- </target>
-</project>
\ No newline at end of file
--- a/src/Tools/jEdit/plugin/IsabellePlugin.props Fri Dec 19 11:25:06 2008 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,29 +0,0 @@
-# jEdit Properties
-
-plugin.isabelle.jedit.Plugin.activate=startup
-plugin.isabelle.jedit.Plugin.name=IsabellePlugin
-plugin.isabelle.jedit.Plugin.version=0.1
-plugin.isabelle.jedit.Plugin.description=Isabelle/Isar integration into jEdit
-plugin.isabelle.jedit.Plugin.option-pane=isabelle
-
-plugin.isabelle.jedit.Plugin.menu.label=Isabelle
-plugin.isabelle.jedit.Plugin.menu=Isabelle.show-output Isabelle.show-state Isabelle.activate Isabelle.show-scroller
-
-Isabelle.show-output.label=Show Output
-Isabelle.show-state.label=Show State
-Isabelle.show-scroller.label=Show Scroller
-Isabelle.activate.label=Activate current buffer
-
-Isabelle_output.title=Isabelle Output
-Isabelle_state.title=Isabelle State
-Isabelle_scroller.title=Isabelle Scroller
-
-options.isabelle.label=Isabelle
-options.isabelle.code=new isabelle.jedit.OptionPane();
-options.isabelle.font-path.title=Font Path
-options.isabelle.font-size.title=Font Size
-options.isabelle.font-size=14
-
-plugin.isabelle.jedit.Plugin.depend.1=plugin sidekick.SideKickPlugin 0.7.6
-sidekick.parser.isabelle.label=Isabelle
-mode.text.sidekick.parser=isabelle
\ No newline at end of file
--- a/src/Tools/jEdit/plugin/actions.xml Fri Dec 19 11:25:06 2008 +0100
+++ b/src/Tools/jEdit/plugin/actions.xml Sat Jan 10 17:59:23 2009 +0100
@@ -1,25 +1,25 @@
<ACTIONS>
- <ACTION NAME="Isabelle.show-output">
+ <ACTION NAME="isabelle.show-output">
<CODE>
- wm.addDockableWindow("Isabelle_output");
+ wm.addDockableWindow("isabelle-output");
</CODE>
</ACTION>
- <ACTION NAME="Isabelle.show-state">
+ <ACTION NAME="isabelle.show-state">
<CODE>
- wm.addDockableWindow("Isabelle_state");
+ wm.addDockableWindow("isabelle-state");
</CODE>
</ACTION>
- <ACTION NAME="Isabelle.show-scroller">
+ <ACTION NAME="isabelle.show-scroller">
<CODE>
- wm.addDockableWindow("Isabelle_scroller");
+ wm.addDockableWindow("isabelle-scroller");
</CODE>
</ACTION>
- <ACTION NAME="Isabelle.activate">
+ <ACTION NAME="isabelle.activate">
<CODE>
- isabelle.jedit.Plugin$.MODULE$.plugin().switch_active(view);
+ isabelle.jedit.Isabelle.plugin().switch_active(view);
</CODE>
<IS_SELECTED>
- return isabelle.jedit.Plugin$.MODULE$.plugin().is_active(view.getBuffer());
+ return isabelle.jedit.Isabelle.plugin().is_active(view.getBuffer());
</IS_SELECTED>
</ACTION>
</ACTIONS>
\ No newline at end of file
--- a/src/Tools/jEdit/plugin/dockables.xml Fri Dec 19 11:25:06 2008 +0100
+++ b/src/Tools/jEdit/plugin/dockables.xml Sat Jan 10 17:59:23 2009 +0100
@@ -3,13 +3,13 @@
<!DOCTYPE DOCKABLES SYSTEM "dockables.dtd">
<DOCKABLES>
- <DOCKABLE NAME="Isabelle_output">
+ <DOCKABLE NAME="isabelle-output" MOVABLE="TRUE">
new isabelle.jedit.OutputDockable(view, position);
</DOCKABLE>
- <DOCKABLE NAME="Isabelle_state">
+ <DOCKABLE NAME="isabelle-state" MOVABLE="TRUE">
new isabelle.jedit.StateViewDockable(view, position);
</DOCKABLE>
- <DOCKABLE NAME="Isabelle_scroller">
+ <DOCKABLE NAME="isabelle-scroller" MOVABLE="TRUE">
new isabelle.jedit.ScrollerDockable(view, position);
</DOCKABLE>
</DOCKABLES>
\ No newline at end of file
--- a/src/Tools/jEdit/plugin/services.xml Fri Dec 19 11:25:06 2008 +0100
+++ b/src/Tools/jEdit/plugin/services.xml Sat Jan 10 17:59:23 2009 +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/Dummy.java Sat Jan 10 17:59:23 2009 +0100
@@ -0,0 +1,3 @@
+/* dummy class to make ant javadoc work */
+package isabelle;
+public class Dummy { }
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/jedit/IsabelleSideKickParser.scala Sat Jan 10 17:59:23 2009 +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)
+
+ Isabelle.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/jedit/OptionPane.scala Fri Dec 19 11:25:06 2008 +0100
+++ b/src/Tools/jEdit/src/jedit/OptionPane.scala Sat Jan 10 17:59:23 2009 +0100
@@ -1,3 +1,9 @@
+/*
+ * Editor pane for plugin options
+ *
+ * @author Johannes Hölzl, TU Munich
+ */
+
package isabelle.jedit
import java.lang.Integer
@@ -9,12 +15,10 @@
import javax.swing.{ JTextField, JButton, JPanel, JLabel, JFileChooser,
JSpinner, SwingUtilities, JComboBox }
-import isabelle.IsabelleSystem
-
import org.gjt.sp.jedit.AbstractOptionPane
class OptionPane extends AbstractOptionPane("isabelle") {
- import Plugin.property
+ import Isabelle.property
var pathName = new JTextField()
var fontSize = new JSpinner()
@@ -53,14 +57,12 @@
})
addComponent(property("logic.title"), {
- val logics : Array[Object] =
- (IsabelleSystem.isabelle_tool("findlogics") _1).split("\\s").asInstanceOf[Array[Object]]
- for (name <- logics) {
+ for (name <- Isabelle.system.find_logics()) {
logicName.addItem(name)
if (name == property("logic"))
logicName.setSelectedItem(name)
}
-
+
logicName
})
}
@@ -73,7 +75,7 @@
property("font-size", size.toString)
SwingUtilities invokeLater new Runnable() {
override def run() =
- Plugin.plugin.setFont(name, size.asInstanceOf[Integer].intValue)
+ Isabelle.plugin.set_font(name, size.asInstanceOf[Integer].intValue)
}
}
--- a/src/Tools/jEdit/src/jedit/OutputDockable.scala Fri Dec 19 11:25:06 2008 +0100
+++ b/src/Tools/jEdit/src/jedit/OutputDockable.scala Sat Jan 10 17:59:23 2009 +0100
@@ -1,13 +1,25 @@
+/*
+ * Dockable window for raw process output
+ *
+ * @author Fabian Immler, TU Munich
+ * @author Johannes Hölzl, TU Munich
+ */
+
package isabelle.jedit
-import java.awt.GridLayout
-import javax.swing.{ JPanel, JTextArea, JScrollPane }
+import java.awt.{Dimension, GridLayout}
+import javax.swing.{JPanel, JTextArea, JScrollPane}
import org.gjt.sp.jedit.View
+import org.gjt.sp.jedit.gui.DockableWindowManager
+
class OutputDockable(view : View, position : String) extends JPanel {
+ if (position == DockableWindowManager.FLOATING)
+ setPreferredSize(new Dimension(500, 250))
+
setLayout(new GridLayout(1, 1))
- add(new JScrollPane(new JTextArea("No Prover running")))
+ add(new JScrollPane(new JTextArea))
}
--- a/src/Tools/jEdit/src/jedit/PhaseOverviewPanel.scala Fri Dec 19 11:25:06 2008 +0100
+++ b/src/Tools/jEdit/src/jedit/PhaseOverviewPanel.scala Sat Jan 10 17:59:23 2009 +0100
@@ -1,3 +1,9 @@
+/*
+ * Information on command status left of scrollbar (with panel)
+ *
+ * @author Fabian Immler, TU Munich
+ */
+
package isabelle.jedit
import isabelle.prover.Command
@@ -18,7 +24,7 @@
var textarea : JEditTextArea = null
val repaint_delay = new isabelle.utils.Delay(100, () => repaint())
- prover.commandInfo.add(cc => repaint_delay.delay_or_ignore())
+ prover.command_info += (_ => repaint_delay.delay_or_ignore())
setRequestFocusEnabled(false);
@@ -57,10 +63,10 @@
val line2 = buffer.getLineOfOffset(command.stop - 1) + 1
val y = lineToY(line1)
val height = lineToY(line2) - y - 1
- val (light, dark) = command.phase match {
- case Command.Phase.UNPROCESSED => (Color.yellow, new Color(128,128,0))
- case Command.Phase.FINISHED => (Color.green, new Color(0, 128, 0))
- case Command.Phase.FAILED => (Color.red, new Color(128,0,0))
+ val (light, dark) = command.status match {
+ case Command.Status.UNPROCESSED => (Color.yellow, new Color(128,128,0))
+ case Command.Status.FINISHED => (Color.green, new Color(0, 128, 0))
+ case Command.Status.FAILED => (Color.red, new Color(128,0,0))
}
gfx.setColor(light)
--- a/src/Tools/jEdit/src/jedit/Plugin.scala Fri Dec 19 11:25:06 2008 +0100
+++ b/src/Tools/jEdit/src/jedit/Plugin.scala Sat Jan 10 17:59:23 2009 +0100
@@ -1,46 +1,79 @@
+/*
+ * Main Isabelle/jEdit plugin setup
+ *
+ * @author Johannes Hölzl, TU Munich
+ * @author Fabian Immler, TU Munich
+ */
+
package isabelle.jedit
+
+import java.io.{FileInputStream, IOException}
import java.awt.Font
-import java.io.{ FileInputStream, IOException }
import javax.swing.JScrollPane
-import isabelle.utils.EventSource
-
-import isabelle.prover.{ Prover, Command }
-
-import isabelle.IsabelleSystem
-
import scala.collection.mutable.HashMap
-import org.gjt.sp.jedit.{ jEdit, EBMessage, EBPlugin, Buffer, EditPane, ServiceManager, View }
+import isabelle.prover.{Prover, Command}
+import isabelle.{IsabelleSystem, Symbol}
+
+import org.gjt.sp.jedit.{jEdit, EBMessage, EBPlugin, Buffer, EditPane, ServiceManager, View}
import org.gjt.sp.jedit.buffer.JEditBuffer
import org.gjt.sp.jedit.textarea.JEditTextArea
-import org.gjt.sp.jedit.msg.{ EditPaneUpdate, PropertiesChanged }
+import org.gjt.sp.jedit.msg.{EditPaneUpdate, PropertiesChanged}
+
-object Plugin {
+object Isabelle {
+ // name
val NAME = "Isabelle"
val OPTION_PREFIX = "options.isabelle."
val VFS_PREFIX = "isabelle:"
-
- def property(name : String) = jEdit.getProperty(OPTION_PREFIX + name)
- def property(name : String, value : String) =
+
+ // properties
+ def property(name: String) = jEdit.getProperty(OPTION_PREFIX + name)
+ def property(name: String, value: String) =
jEdit.setProperty(OPTION_PREFIX + name, value)
-
- var plugin : Plugin = null
- def prover(buffer : JEditBuffer) = plugin.prover_setup(buffer).get.prover
- def prover_setup(buffer : JEditBuffer) = plugin.prover_setup(buffer).get
+
+
+ // Isabelle system
+ var system: IsabelleSystem = null
+ var symbols: Symbol.Interpretation = null
+
+ // plugin instance
+ var plugin: Plugin = null
+
+ // provers
+ def prover(buffer: JEditBuffer) = plugin.prover_setup(buffer).get.prover
+ def prover_setup(buffer: JEditBuffer) = plugin.prover_setup(buffer).get
}
+
class Plugin extends EBPlugin {
- import Plugin._
+
+ // Isabelle font
+
+ var font: Font = null
+ val font_changed = new EventBus[Font]
+
+ def set_font(path: String, size: Float) {
+ font = Font.createFont(Font.TRUETYPE_FONT, new FileInputStream(path)).
+ deriveFont(Font.PLAIN, size)
+ font_changed.event(font)
+ }
+
+
+ /* unique ids */ // FIXME specific to "session" (!??)
+
+ private var id_count: BigInt = 0
+ def id() : String = synchronized { id_count += 1; "editor:" + id_count }
+
+
+ // mapping buffer <-> prover
private val mapping = new HashMap[JEditBuffer, ProverSetup]
- var viewFont : Font = null
- val viewFontChanged = new EventSource[Font]
-
- def install(view : View) {
+ def install(view: View) {
val buffer = view.getBuffer
mapping.get(buffer) match{
case None =>{
@@ -52,7 +85,7 @@
}
}
- def uninstall(view : View) {
+ def uninstall(view: View) {
val buffer = view.getBuffer
mapping.removeKey(buffer) match{
case None => System.err.println("No Plugin installed on this Buffer")
@@ -62,20 +95,23 @@
}
def prover_setup (buffer : JEditBuffer) : Option[ProverSetup] = mapping.get(buffer)
- def is_active (buffer : JEditBuffer) = mapping.get(buffer) match { case None => false case _ => true}
+ def is_active (buffer : JEditBuffer) = mapping.isDefinedAt(buffer)
def switch_active (view : View) = mapping.get(view.getBuffer) match {
case None => install(view)
case _ => uninstall(view)}
+
- override def handleMessage(msg : EBMessage) = msg match {
- case epu : EditPaneUpdate => epu.getWhat() match {
+ // main plugin plumbing
+
+ override def handleMessage(msg: EBMessage) = msg match {
+ case epu: EditPaneUpdate => epu.getWhat match {
case EditPaneUpdate.BUFFER_CHANGED =>
mapping get epu.getEditPane.getBuffer match {
//only activate 'isabelle'-buffers!
case None =>
case Some(prover_setup) =>
prover_setup.theory_view.activate
- val dockable = epu.getEditPane.getView.getDockableWindowManager.getDockable("Isabelle_output")
+ val dockable = epu.getEditPane.getView.getDockableWindowManager.getDockable("isabelle-output")
if(dockable != null) {
val output_dockable = dockable.asInstanceOf[OutputDockable]
if(output_dockable.getComponent(0) != prover_setup.output_text_view ) {
@@ -94,36 +130,27 @@
}
case _ =>
}
-
case _ =>
}
- def setFont(path : String, size : Float) {
- try {
- val fontStream = new FileInputStream(path)
- val font = Font.createFont(Font.TRUETYPE_FONT, fontStream)
- viewFont = font.deriveFont(Font.PLAIN, size)
-
- viewFontChanged.fire(viewFont)
- }
- catch {
- case e : IOException =>
- }
- }
-
override def start() {
- plugin = this
+ Isabelle.system = new IsabelleSystem
+ Isabelle.symbols = new Symbol.Interpretation(Isabelle.system)
+ Isabelle.plugin = this
- if (property("font-path") != null && property("font-size") != null)
+ if (Isabelle.property("font-path") != null && Isabelle.property("font-size") != null)
try {
- setFont(property("font-path"), property("font-size").toFloat)
+ set_font(Isabelle.property("font-path"), Isabelle.property("font-size").toFloat)
}
catch {
- case e : NumberFormatException =>
+ case e: NumberFormatException =>
}
}
override def stop() {
- // TODO: implement cleanup
+ // TODO: proper cleanup
+ Isabelle.symbols = null
+ Isabelle.system = null
+ Isabelle.plugin = null
}
}
--- a/src/Tools/jEdit/src/jedit/ProverSetup.scala Fri Dec 19 11:25:06 2008 +0100
+++ b/src/Tools/jEdit/src/jedit/ProverSetup.scala Sat Jan 10 17:59:23 2009 +0100
@@ -1,55 +1,51 @@
/*
- * BufferExtension.scala
+ * Independent prover sessions
*
- * To change this template, choose Tools | Template Manager
- * and open the template in the editor.
+ * @author Fabian Immler, TU Munich
*/
package isabelle.jedit
-import isabelle.utils.EventSource
-import isabelle.prover.{ Prover, Command }
+import isabelle.prover.{Prover, Command}
+import isabelle.renderer.UserAgent
+
+
import org.w3c.dom.Document
-import isabelle.IsabelleSystem
-
-import org.gjt.sp.jedit.{ jEdit, EBMessage, EBPlugin, Buffer, EditPane, View }
+import org.gjt.sp.jedit.{jEdit, EBMessage, EBPlugin, Buffer, EditPane, View}
import org.gjt.sp.jedit.buffer.JEditBuffer
-import org.gjt.sp.jedit.msg.{ EditPaneUpdate, PropertiesChanged }
+import org.gjt.sp.jedit.msg.{EditPaneUpdate, PropertiesChanged}
import javax.swing.{JTextArea, JScrollPane}
-class ProverSetup(buffer : JEditBuffer) {
- val prover = new Prover()
- var theory_view : TheoryView = null
-
- private var _selectedState : Command = null
+class ProverSetup(buffer: JEditBuffer)
+{
+ val prover = new Prover(Isabelle.system, Isabelle.symbols)
+ var theory_view: TheoryView = null
- val stateUpdate = new EventSource[Command]
+ val state_update = new EventBus[Command]
- def selectedState = _selectedState
- def selectedState_=(newState : Command) {
- _selectedState = newState
- stateUpdate fire newState
- }
+ private var _selected_state: Command = null
+ def selected_state = _selected_state
+ def selected_state_=(state: Command) { _selected_state = state; state_update.event(state) }
- val output_text_view = new JTextArea("== Isabelle output ==\n")
-
- def activate(view : View) {
- val logic = Plugin.property("logic")
- prover.start(if (logic == null) logic else "HOL")
+ val output_text_view = new JTextArea
+
+ def activate(view: View) {
+ prover.start(Isabelle.property("logic"))
val buffer = view.getBuffer
- val dir = buffer.getDirectory()
+ val dir = buffer.getDirectory
theory_view = new TheoryView(view.getTextArea)
- prover.setDocument(theory_view ,
- if (dir.startsWith(Plugin.VFS_PREFIX)) dir.substring(Plugin.VFS_PREFIX.length) else dir)
+ prover.set_document(theory_view,
+ if (dir.startsWith(Isabelle.VFS_PREFIX)) dir.substring(Isabelle.VFS_PREFIX.length) else dir)
theory_view.activate
- prover.outputInfo.add( text => {
+ prover.output_info += (text =>
+ {
output_text_view.append(text)
- val dockable = view.getDockableWindowManager.getDockable("Isabelle_output")
+ val dockable = view.getDockableWindowManager.getDockable("isabelle-output")
//link process output if dockable is active
if(dockable != null) {
val output_dockable = dockable.asInstanceOf[OutputDockable]
@@ -60,23 +56,25 @@
}
}
})
-
+
//register for state-view
- stateUpdate.add(state => {
- val state_view = view.getDockableWindowManager.getDockable("Isabelle_state")
- val state_panel = if(state_view != null) state_view.asInstanceOf[StateViewDockable].panel else null
- if(state_panel != null){
+ state_update += (state => {
+ val state_view = view.getDockableWindowManager.getDockable("isabelle-state")
+ val state_panel =
+ if (state_view != null) state_view.asInstanceOf[StateViewDockable].panel
+ else null
+ if (state_panel != null){
if (state == null)
- state_panel.setDocument(null : Document)
+ state_panel.setDocument(null: Document)
else
state_panel.setDocument(state.results_xml, UserAgent.baseURL)
}
})
-
+
//register for theory-view
// could also use this:
- // prover.commandInfo.add(c => Plugin.theory_view.repaint(c.command))
+ // prover.commandInfo.add(c => Isabelle.theory_view.repaint(c.command))
}
--- a/src/Tools/jEdit/src/jedit/ScrollerDockable.scala Fri Dec 19 11:25:06 2008 +0100
+++ b/src/Tools/jEdit/src/jedit/ScrollerDockable.scala Sat Jan 10 17:59:23 2009 +0100
@@ -1,19 +1,21 @@
/*
- * ScrollerDockable.scala
+ * Dockable window with scrollable messages
*
+ * @author Fabian Immler, TU Munich
*/
package isabelle.jedit
-import isabelle.utils.EventSource
+
import isabelle.IsabelleProcess.Result
-import isabelle.YXML.parse_failsafe
+import isabelle.renderer.UserAgent
+
import scala.collection.mutable.{ArrayBuffer, HashMap}
-import java.awt.{ BorderLayout, Adjustable }
-import java.awt.event.{ ActionListener, ActionEvent, AdjustmentListener, AdjustmentEvent, ComponentListener, ComponentEvent }
-import javax.swing.{ JFrame, JPanel, JRadioButton, JScrollBar, JTextArea, Timer }
+import java.awt.{BorderLayout, Adjustable, Dimension}
+import java.awt.event.{ActionListener, ActionEvent, AdjustmentListener, AdjustmentEvent, ComponentListener, ComponentEvent}
+import javax.swing.{JFrame, JPanel, JRadioButton, JScrollBar, JTextArea, Timer}
import org.w3c.dom.Document
@@ -21,6 +23,8 @@
import org.xhtmlrenderer.context.AWTFontResolver
import org.gjt.sp.jedit.View
+import org.gjt.sp.jedit.gui.DockableWindowManager
+
trait Renderer[U, R] {
def render (u: U): R
@@ -99,9 +103,9 @@
def setText(s: String) {
message_ind.setText(s)
}
-
}
+
class ScrollerDockable(view : View, position : String) extends JPanel with AdjustmentListener {
val renderer:Renderer[Result, XHTMLPanel] = new ResultToPanelRenderer
@@ -116,7 +120,10 @@
vscroll.setUnitIncrement(subunits / 3)
vscroll.setBlockIncrement(subunits)
vscroll.addAdjustmentListener(this)
-
+
+ if (position == DockableWindowManager.FLOATING)
+ setPreferredSize(new Dimension(500, 250))
+
setLayout(new BorderLayout())
add (vscroll, BorderLayout.EAST)
add (message_panel, BorderLayout.CENTER)
@@ -166,7 +173,7 @@
// TODO: register
- //Plugin.plugin.prover.allInfo.add(add_result(_))
+ //Isabelle.plugin.prover.allInfo.add(add_result(_))
}
//Concrete Implementations
@@ -213,15 +220,15 @@
val panel = new XHTMLPanel(new UserAgent())
val fontResolver =
panel.getSharedContext.getFontResolver.asInstanceOf[AWTFontResolver]
- if (Plugin.plugin.viewFont != null)
- fontResolver.setFontMapping("Isabelle", Plugin.plugin.viewFont)
+ if (Isabelle.plugin.font != null)
+ fontResolver.setFontMapping("Isabelle", Isabelle.plugin.font)
- Plugin.plugin.viewFontChanged.add(font => {
- if (Plugin.plugin.viewFont != null)
- fontResolver.setFontMapping("Isabelle", Plugin.plugin.viewFont)
+ Isabelle.plugin.font_changed += (font => {
+ if (Isabelle.plugin.font != null)
+ fontResolver.setFontMapping("Isabelle", Isabelle.plugin.font)
panel.relayout()
})
- val tree = parse_failsafe(VFS.converter.decode(r.result))
+ val tree = YXML.parse_failsafe(Isabelle.symbols.decode(r.result))
val document = XML.document(tree)
panel.setDocument(document, UserAgent.baseURL)
val sa = new SelectionActions
@@ -237,7 +244,7 @@
panel.doDocumentLayout (panel.getGraphics) //lay out, preferred size is set then
// if there are thousands of empty panels, all have to be rendered -
// but this takes time (even for empty panels); therefore minimum size
- panel.setPreferredSize(new java.awt.Dimension(width,Math.max(25, panel.getPreferredSize.getHeight.toInt)))
+ panel.setPreferredSize(new java.awt.Dimension(width, Math.max(25, panel.getPreferredSize.getHeight.toInt)))
}
}
\ No newline at end of file
--- a/src/Tools/jEdit/src/jedit/SelectionActions.scala Fri Dec 19 11:25:06 2008 +0100
+++ b/src/Tools/jEdit/src/jedit/SelectionActions.scala Sat Jan 10 17:59:23 2009 +0100
@@ -1,8 +1,7 @@
/*
- * SelectionActions.scala
+ * Text selection for XHTML renderer
*
- * To change this template, choose Tools | Template Manager
- * and open the template in the editor.
+ * @author Fabian Immler, TU Munich
*/
package isabelle.jedit
@@ -26,24 +25,22 @@
def copyaction {
val selected_string = getSelectionRange.toString
- val encoded = VFS.converter.encode (selected_string)
+ val encoded = Isabelle.symbols.encode(selected_string)
val clipboard = java.awt.Toolkit.getDefaultToolkit().getSystemClipboard;
val transferable = new java.awt.datatransfer.StringSelection(selected_string)
clipboard.setContents(transferable, null)
}
- override def keyPressed (e: KeyEvent) {
+ override def keyPressed(e: KeyEvent) {
if(e.getKeyCode == KeyEvent.VK_ENTER) {
copyaction
e.consume
}
}
- override def keyReleased (e: KeyEvent) {
-
- }
- override def keyTyped (e: KeyEvent) {
-
+
+ override def keyReleased(e: KeyEvent) {
}
-
+ override def keyTyped(e: KeyEvent) {
+ }
}
--- a/src/Tools/jEdit/src/jedit/StateViewDockable.scala Fri Dec 19 11:25:06 2008 +0100
+++ b/src/Tools/jEdit/src/jedit/StateViewDockable.scala Sat Jan 10 17:59:23 2009 +0100
@@ -1,34 +1,74 @@
+/*
+ * Dockable window with rendered state output
+ *
+ * @author Fabian Immler, TU Munich
+ * @author Johannes Hölzl, TU Munich
+ */
+
package isabelle.jedit
-import java.awt.BorderLayout
-import javax.swing.{ JButton, JPanel, JScrollPane }
+import java.awt.{BorderLayout, Dimension}
+import javax.swing.{JButton, JPanel, JScrollPane}
-import isabelle.IsabelleSystem.getenv
+import isabelle.renderer.UserAgent
-import org.xhtmlrenderer.simple.XHTMLPanel
+import org.xhtmlrenderer.simple.{XHTMLPanel, FSScrollPane}
import org.xhtmlrenderer.context.AWTFontResolver
+import org.xhtmlrenderer.layout.SharedContext;
+import org.xhtmlrenderer.extend.TextRenderer;
+import org.xhtmlrenderer.swing.Java2DTextRenderer;
+import org.gjt.sp.jedit.jEdit
import org.gjt.sp.jedit.View
+import org.gjt.sp.jedit.gui.DockableWindowManager
+import org.gjt.sp.jedit.textarea.AntiAlias
+
class StateViewDockable(view : View, position : String) extends JPanel {
- val panel = new XHTMLPanel(new UserAgent())
+
+ // outer panel
+ if (position == DockableWindowManager.FLOATING)
+ setPreferredSize(new Dimension(500, 250))
setLayout(new BorderLayout)
- //Copy-paste-support
- private val cp = new SelectionActions
- cp.install(panel)
+
+ // XHTML panel
+ val panel = new XHTMLPanel(new UserAgent)
+
- add(new JScrollPane(panel), BorderLayout.CENTER)
+ // anti-aliasing
+ // TODO: proper EditBus event handling
+ {
+ val aa = jEdit.getProperty("view.antiAlias")
+ if (aa != null && aa != AntiAlias.NONE) {
+ panel.getSharedContext.setTextRenderer(
+ {
+ val renderer = new Java2DTextRenderer
+ renderer.setSmoothingThreshold(0)
+ renderer.setSmoothingLevel(TextRenderer.HIGH)
+ renderer
+ })
+ }
+ }
+
+
+ // copy & paste
+ (new SelectionActions).install(panel)
+
+
+ // scrolling
+ add(new FSScrollPane(panel), BorderLayout.CENTER)
+
private val fontResolver =
panel.getSharedContext.getFontResolver.asInstanceOf[AWTFontResolver]
- if (Plugin.plugin.viewFont != null)
- fontResolver.setFontMapping("Isabelle", Plugin.plugin.viewFont)
+ if (Isabelle.plugin.font != null)
+ fontResolver.setFontMapping("Isabelle", Isabelle.plugin.font)
- Plugin.plugin.viewFontChanged.add(font => {
- if (Plugin.plugin.viewFont != null)
- fontResolver.setFontMapping("Isabelle", Plugin.plugin.viewFont)
+ Isabelle.plugin.font_changed += (font => {
+ if (Isabelle.plugin.font != null)
+ fontResolver.setFontMapping("Isabelle", Isabelle.plugin.font)
panel.relayout()
})
--- a/src/Tools/jEdit/src/jedit/TheoryView.scala Fri Dec 19 11:25:06 2008 +0100
+++ b/src/Tools/jEdit/src/jedit/TheoryView.scala Sat Jan 10 17:59:23 2009 +0100
@@ -1,262 +1,290 @@
+/*
+ * jEdit text area as document text source
+ *
+ * @author Fabian Immler, TU Munich
+ * @author Johannes Hölzl, TU Munich
+ * @author Makarius
+ */
+
package isabelle.jedit
-import isabelle.utils.EventSource
import isabelle.proofdocument.Text
+import isabelle.prover.{Prover, Command}
-import isabelle.prover.{ Prover, Command, CommandChangeInfo }
-import isabelle.prover.Command.Phase
-
-import javax.swing.Timer
-import javax.swing.event.{ CaretListener, CaretEvent }
import java.awt.Graphics2D
-import java.awt.event.{ ActionEvent, ActionListener }
-import java.awt.Color;
+import java.awt.event.{ActionEvent, ActionListener}
+import java.awt.Color
+import javax.swing.Timer
+import javax.swing.event.{CaretListener, CaretEvent}
-import org.gjt.sp.jedit.buffer.{ BufferListener, JEditBuffer }
-import org.gjt.sp.jedit.textarea.{ JEditTextArea, TextAreaExtension, TextAreaPainter }
+import org.gjt.sp.jedit.buffer.{BufferListener, JEditBuffer}
+import org.gjt.sp.jedit.textarea.{JEditTextArea, TextAreaExtension, TextAreaPainter}
import org.gjt.sp.jedit.syntax.SyntaxStyle
+
object TheoryView {
- def chooseColor(state : Command) : Color = {
- if (state == null)
- Color.red
+ def choose_color(state: Command): Color = {
+ if (state == null) Color.red
else
- state.phase match {
- case Phase.UNPROCESSED => new Color(255, 255, 192)
- case Phase.FINISHED => new Color(192, 255, 192)
- case Phase.FAILED => new Color(255, 192, 192)
+ state.status match {
+ case Command.Status.UNPROCESSED => new Color(255, 228, 225)
+ case Command.Status.FINISHED => new Color(234, 248, 255)
+ case Command.Status.FAILED => new Color(255, 192, 192)
case _ => Color.red
}
}
- def chooseColor(status : String) : Color = {
- //TODO: as properties!
- status match {
- //outer
- case "ident" | "command" | "keyword" => Color.blue
- case "verbatim"=> Color.green
- case "comment" => Color.gray
- case "control" => Color.white
- case "malformed" => Color.red
- case "string" | "altstring" => Color.orange
- //logical
- case "tclass" | "tycon" | "fixed_decl" | "fixed"
- | "const_decl" | "const" | "fact_decl" | "fact"
- |"dynamic_fact" |"local_fact_decl" | "local_fact"
- => new Color(255, 0, 255)
- //inner syntax
- case "tfree" | "free" => Color.blue
- case "tvar" | "skolem" | "bound" | "var" => Color.green
- case "num" | "xnum" | "xstr" | "literal" | "inner_comment" => new Color(255, 128, 128)
- case "sort" | "typ" | "term" | "prop" | "attribute" | "method" => Color.yellow
- // embedded source
- case "doc_source" | "ML_source" | "ML_antic" | "doc_antiq" | "antiq"
- => new Color(0, 192, 0)
+ def choose_color(markup: String): Color = {
+ // TODO: as properties
+ markup match {
+ // logical entities
+ case Markup.TCLASS | Markup.TYCON | Markup.FIXED_DECL | Markup.FIXED | Markup.CONST_DECL
+ | Markup.CONST | Markup.FACT_DECL | Markup.FACT | Markup.DYNAMIC_FACT
+ | Markup.LOCAL_FACT_DECL | Markup.LOCAL_FACT => new Color(255, 0, 255)
+ // inner syntax
+ case Markup.TFREE | Markup.FREE => Color.blue
+ case Markup.TVAR | Markup.SKOLEM | Markup.BOUND | Markup.VAR => Color.green
+ case Markup.NUM | Markup.FLOAT | Markup.XNUM | Markup.XSTR | Markup.LITERAL
+ | Markup.INNER_COMMENT => new Color(255, 128, 128)
+ case Markup.SORT | Markup.TYP | Markup.TERM | Markup.PROP
+ | Markup.ATTRIBUTE | Markup.METHOD => Color.yellow
+ // embedded source text
+ case Markup.ML_SOURCE | Markup.DOC_SOURCE | Markup.ANTIQ | Markup.ML_ANTIQ
+ | Markup.DOC_ANTIQ => new Color(0, 192, 0)
+ // outer syntax
+ case Markup.IDENT | Markup.COMMAND | Markup.KEYWORD => Color.blue
+ case Markup.VERBATIM => Color.green
+ case Markup.COMMENT => Color.gray
+ case Markup.CONTROL => Color.white
+ case Markup.MALFORMED => Color.red
+ case Markup.STRING | Markup.ALTSTRING => Color.orange
+ // other
case _ => Color.white
}
}
}
-class TheoryView (text_area : JEditTextArea)
+
+class TheoryView (text_area: JEditTextArea)
extends TextAreaExtension with Text with BufferListener {
- import TheoryView._
- import Text.Changed
- var col : Changed = null
-
- val buffer = text_area.getBuffer
+ private val buffer = text_area.getBuffer
buffer.addBufferListener(this)
-
- val colTimer = new Timer(300, new ActionListener() {
- override def actionPerformed(e : ActionEvent) { commit() }
+
+
+ private var col: Text.Changed = null
+
+ private val col_timer = new Timer(300, new ActionListener() {
+ override def actionPerformed(e: ActionEvent) = commit()
})
-
- val changesSource = new EventSource[Changed]
- val phase_overview = new PhaseOverviewPanel(Plugin.prover(buffer))
- val repaint_delay = new isabelle.utils.Delay(100, () => repaintAll())
- Plugin.prover(buffer).commandInfo.add(_ => repaint_delay.delay_or_ignore())
- Plugin.plugin.viewFontChanged.add(font => updateFont())
+ col_timer.stop
+ col_timer.setRepeats(true)
- colTimer.stop
- colTimer.setRepeats(true)
+
+ private val phase_overview = new PhaseOverviewPanel(Isabelle.prover(buffer))
+
+
+ /* activation */
+
+ Isabelle.plugin.font_changed += (_ => update_font())
- def activate() {
- text_area.addCaretListener(selectedStateController)
- phase_overview.textarea = text_area
- text_area.addLeftOfScrollBar(phase_overview)
- val painter = text_area.getPainter()
- painter.addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, this)
- updateFont()
- }
-
- private def updateFont() {
+ private def update_font() = {
if (text_area != null) {
- val painter = text_area.getPainter()
- if (Plugin.plugin.viewFont != null) {
- painter.setStyles(painter.getStyles().map(style =>
- new SyntaxStyle(style.getForegroundColor,
- style.getBackgroundColor,
- Plugin.plugin.viewFont)
+ if (Isabelle.plugin.font != null) {
+ val painter = text_area.getPainter
+ painter.setStyles(painter.getStyles.map(style =>
+ new SyntaxStyle(style.getForegroundColor, style.getBackgroundColor, Isabelle.plugin.font)
))
- painter.setFont(Plugin.plugin.viewFont)
- repaintAll()
+ painter.setFont(Isabelle.plugin.font)
+ repaint_all()
}
}
}
-
- def deactivate() {
- text_area.getPainter().removeExtension(this)
- text_area.removeCaretListener(selectedStateController)
- text_area.removeLeftOfScrollBar(phase_overview)
- }
-
- val selectedStateController = new CaretListener() {
- override def caretUpdate(e : CaretEvent) {
- val cmd = Plugin.prover(buffer).document.getNextCommandContaining(e.getDot())
- if (cmd != null && cmd.start <= e.getDot() &&
- Plugin.prover_setup(buffer).selectedState != cmd)
- Plugin.prover_setup(buffer).selectedState = cmd
+
+ private val selected_state_controller = new CaretListener {
+ override def caretUpdate(e: CaretEvent) = {
+ val cmd = Isabelle.prover(buffer).document.getNextCommandContaining(e.getDot)
+ if (cmd != null && cmd.start <= e.getDot &&
+ Isabelle.prover_setup(buffer).selected_state != cmd)
+ Isabelle.prover_setup(buffer).selected_state = cmd
}
}
- private def fromCurrent(pos : Int) =
+ def activate() = {
+ text_area.addCaretListener(selected_state_controller)
+ phase_overview.textarea = text_area
+ text_area.addLeftOfScrollBar(phase_overview)
+ text_area.getPainter.addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, this)
+ update_font()
+ }
+
+ def deactivate() = {
+ text_area.getPainter.removeExtension(this)
+ text_area.removeLeftOfScrollBar(phase_overview)
+ text_area.removeCaretListener(selected_state_controller)
+ }
+
+
+ /* painting */
+
+ val repaint_delay = new isabelle.utils.Delay(100, () => repaint_all())
+ Isabelle.prover(buffer).command_info += (_ => repaint_delay.delay_or_ignore())
+
+ private def from_current(pos: Int) =
if (col != null && col.start <= pos)
if (pos < col.start + col.added) col.start
else pos - col.added + col.removed
else pos
-
- private def toCurrent(pos : Int) =
+
+ private def to_current(pos : Int) =
if (col != null && col.start <= pos)
if (pos < col.start + col.removed) col.start
else pos + col.added - col.removed
else pos
-
- def repaint(cmd : Command)
+
+ def repaint(cmd: Command) =
{
- val ph = cmd.phase
- if (text_area != null && ph != Phase.REMOVE && ph != Phase.REMOVED) {
- var start = text_area.getLineOfOffset(toCurrent(cmd.start))
- var stop = text_area.getLineOfOffset(toCurrent(cmd.stop) - 1)
+ val status = cmd.status
+ if (text_area != null && status != Command.Status.REMOVE && status != Command.Status.REMOVED) {
+ val start = text_area.getLineOfOffset(to_current(cmd.start))
+ val stop = text_area.getLineOfOffset(to_current(cmd.stop) - 1)
text_area.invalidateLineRange(start, stop)
-
- if (Plugin.prover_setup(buffer).selectedState == cmd)
- Plugin.prover_setup(buffer).selectedState = cmd // update State view
+
+ if (Isabelle.prover_setup(buffer).selected_state == cmd)
+ Isabelle.prover_setup(buffer).selected_state = cmd // update State view
}
}
-
- def repaintAll()
+
+ def repaint_all() =
{
if (text_area != null)
- text_area.invalidateLineRange(text_area.getFirstPhysicalLine,
- text_area.getLastPhysicalLine)
+ text_area.invalidateLineRange(text_area.getFirstPhysicalLine, text_area.getLastPhysicalLine)
}
- def encolor(gfx : Graphics2D, y : Int, height : Int, begin : Int, finish : Int, color : Color, fill : Boolean){
- val fm = text_area.getPainter.getFontMetrics
- val startP = text_area.offsetToXY(begin)
- val stopP = if (finish < buffer.getLength()) text_area.offsetToXY(finish)
- else { var p = text_area.offsetToXY(finish - 1)
- p.x = p.x + fm.charWidth(' ')
- p }
-
- if (startP != null && stopP != null) {
- gfx.setColor(color)
- if(fill){gfx.fillRect(startP.x, y, stopP.x - startP.x, height)}
- else {gfx.drawRect(startP.x, y, stopP.x - startP.x, height)}
+ def encolor(gfx: Graphics2D,
+ y: Int, height: Int, begin: Int, finish: Int, color: Color, fill: Boolean) =
+ {
+ val start = text_area.offsetToXY(begin)
+ val stop =
+ if (finish < buffer.getLength) text_area.offsetToXY(finish)
+ else {
+ val p = text_area.offsetToXY(finish - 1)
+ p.x = p.x + text_area.getPainter.getFontMetrics.charWidth(' ')
+ p
}
+
+ if (start != null && stop != null) {
+ gfx.setColor(color)
+ if (fill) gfx.fillRect(start.x, y, stop.x - start.x, height)
+ else gfx.drawRect(start.x, y, stop.x - start.x, height)
+ }
}
- override def paintValidLine(gfx : Graphics2D, screenLine : Int,
- pl : Int, start : Int, end : Int, y : Int)
- {
- val fm = text_area.getPainter.getFontMetrics
- var savedColor = gfx.getColor
- var e = Plugin.prover(buffer).document.getNextCommandContaining(fromCurrent(start))
+
+ /* TextAreaExtension methods */
+
+ override def paintValidLine(gfx: Graphics2D,
+ screen_line: Int, physical_line: Int, start: Int, end: Int, y: Int) =
+ {
+ val saved_color = gfx.getColor
+
+ val metrics = text_area.getPainter.getFontMetrics
+ var e = Isabelle.prover(buffer).document.getNextCommandContaining(from_current(start))
- //Encolor Phase
- while (e != null && toCurrent(e.start) < end) {
- val begin = start max toCurrent(e.start)
- val finish = end - 1 min toCurrent(e.stop)
- encolor(gfx, y, fm.getHeight, begin, finish, chooseColor(e), true)
+ // encolor phase
+ while (e != null && to_current(e.start) < end) {
+ val begin = start max to_current(e.start)
+ val finish = end - 1 min to_current(e.stop)
+ encolor(gfx, y, metrics.getHeight, begin, finish, TheoryView.choose_color(e), true)
+
// paint details of command
- for(node <- e.root_node.dfs){
- val begin = toCurrent(node.start + e.start)
- val finish = toCurrent(node.end + e.start)
- if(finish > start && begin < end)
- encolor(gfx, y + fm.getHeight - 4, 2, begin max start, finish min end, chooseColor(node.short), true)
+ for (node <- e.root_node.dfs) {
+ val begin = to_current(node.start + e.start)
+ val finish = to_current(node.end + e.start)
+ if (finish > start && begin < end) {
+ encolor(gfx, y + metrics.getHeight - 4, 2, begin max start, finish min end,
+ TheoryView.choose_color(node.short), true)
+ }
}
e = e.next
}
- gfx.setColor(savedColor)
+ gfx.setColor(saved_color)
}
-
- def content(start : Int, stop : Int) = buffer.getText(start, stop - start)
- override def length = buffer.getLength
+
+
+ /* Text methods */
- def changes = changesSource
+ def content(start: Int, stop: Int) = buffer.getText(start, stop - start)
+ def length = buffer.getLength
+ val changes = new EventBus[Text.Changed]
+
+
+ /* BufferListener methods */
private def commit() {
if (col != null)
- changes.fire(col)
+ changes.event(col)
col = null
- if (colTimer.isRunning())
- colTimer.stop()
- }
-
- private def delayCommit() {
- if (colTimer.isRunning())
- colTimer.restart()
+ if (col_timer.isRunning())
+ col_timer.stop()
+ }
+
+ private def delay_commit() {
+ if (col_timer.isRunning())
+ col_timer.restart()
else
- colTimer.start()
+ col_timer.start()
}
-
- override def contentInserted(buffer : JEditBuffer, startLine : Int,
- offset : Int, numLines : Int, length : Int) { }
- override def contentRemoved(buffer : JEditBuffer, startLine : Int,
- offset : Int, numLines : Int, length : Int) { }
+
+
+ override def contentInserted(buffer: JEditBuffer,
+ start_line: Int, offset: Int, num_lines: Int, length: Int) { }
+
+ override def contentRemoved(buffer: JEditBuffer,
+ start_line: Int, offset: Int, num_lines: Int, length: Int) { }
- override def preContentInserted(buffer : JEditBuffer, startLine : Int,
- offset : Int, numLines : Int, length : Int) {
+ override def preContentInserted(buffer: JEditBuffer,
+ start_line: Int, offset: Int, num_lines: Int, length: Int) =
+ {
if (col == null)
- col = new Changed(offset, length, 0)
- else if (col.start <= offset && offset <= col.start + col.added)
- col = new Changed(col.start, col.added + length, col.removed)
- else {
+ col = new Text.Changed(offset, length, 0)
+ else if (col.start <= offset && offset <= col.start + col.added)
+ col = new Text.Changed(col.start, col.added + length, col.removed)
+ else {
commit()
- col = new Changed(offset, length, 0)
+ col = new Text.Changed(offset, length, 0)
}
- delayCommit()
- }
-
- override def preContentRemoved(buffer : JEditBuffer, startLine : Int,
- start : Int, numLines : Int, removed : Int) {
+ delay_commit()
+ }
+
+ override def preContentRemoved(buffer: JEditBuffer,
+ start_line: Int, start: Int, num_lines: Int, removed: Int) =
+ {
if (col == null)
- col = new Changed(start, 0, removed)
- else if (col.start > start + removed || start > col.start + col.added) {
+ col = new Text.Changed(start, 0, removed)
+ else if (col.start > start + removed || start > col.start + col.added) {
commit()
- col = new Changed(start, 0, removed)
+ col = new Text.Changed(start, 0, removed)
}
else {
val offset = start - col.start
val diff = col.added - removed
- val (added, addRemoved) =
- if (diff < offset)
+ val (added, add_removed) =
+ if (diff < offset)
(offset max 0, diff - (offset max 0))
- else
+ else
(diff - (offset min 0), offset min 0)
-
- col = new Changed(start min col.start, added, col.removed - addRemoved)
+ col = new Text.Changed(start min col.start, added, col.removed - add_removed)
}
- delayCommit()
+ delay_commit()
}
- override def bufferLoaded(buffer : JEditBuffer) { }
- override def foldHandlerChanged(buffer : JEditBuffer) { }
- override def foldLevelChanged(buffer : JEditBuffer, startLine : Int,
- endLine : Int) = { }
- override def transactionComplete(buffer : JEditBuffer) = { }
-}
\ No newline at end of file
+ override def bufferLoaded(buffer: JEditBuffer) { }
+ override def foldHandlerChanged(buffer: JEditBuffer) { }
+ override def foldLevelChanged(buffer: JEditBuffer, start_line: Int, end_line: Int) { }
+ override def transactionComplete(buffer: JEditBuffer) { }
+}
--- a/src/Tools/jEdit/src/jedit/UserAgent.scala Fri Dec 19 11:25:06 2008 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,39 +0,0 @@
-package isabelle.jedit
-
-import java.io.ByteArrayInputStream
-import org.xhtmlrenderer.swing.NaiveUserAgent
-import org.xhtmlrenderer.resource.CSSResource
-import isabelle.IsabelleSystem.getenv
-
-object UserAgent {
- val baseURL = "file://localhost" + getenv("ISABELLE_HOME") + "/lib/html/"
- val userStylesheet = "file://localhost" + getenv("ISABELLE_HOME_USER") + "/etc/user.css";
- val stylesheet = """
-
-@import "isabelle.css";
-
-@import '""" + userStylesheet + """';
-
-messages, message {
- display: block;
- white-space: pre-wrap;
- font-family: Isabelle;
-}
-"""
-}
-
-class UserAgent extends NaiveUserAgent {
- override def getCSSResource(uri : String) : CSSResource = {
- if (uri == UserAgent.baseURL + "style")
- new CSSResource(
- new ByteArrayInputStream(UserAgent.stylesheet.getBytes()))
- else {
- val stream = resolveAndOpenStream(uri)
- val resource = new CSSResource(stream)
- if (stream == null)
- resource.getResourceInputSource().setByteStream(
- new ByteArrayInputStream(new Array[Byte](0)))
- resource
- }
- }
-}
\ No newline at end of file
--- a/src/Tools/jEdit/src/jedit/VFS.scala Fri Dec 19 11:25:06 2008 +0100
+++ b/src/Tools/jEdit/src/jedit/VFS.scala Sat Jan 10 17:59:23 2009 +0100
@@ -1,33 +1,36 @@
+/*
+ * Isabelle virtual file system for jEdit.
+ *
+ * This filesystem passes every operation on to FileVFS. Just the read and write
+ * operations are overwritten to convert Isabelle symbols to unicode on read and
+ * unicode to Isabelle symbols on write.
+ *
+ * @author Johannes Hölzl, TU Munich
+ */
+
package isabelle.jedit
-import java.io.InputStream
-import java.io.OutputStream
-import java.io.ByteArrayInputStream
-import java.io.ByteArrayOutputStream
-import java.io.InputStreamReader
+import java.io.{InputStream, OutputStream, ByteArrayInputStream, ByteArrayOutputStream, InputStreamReader}
import java.awt.Component
-import isabelle.Symbol.Interpretation
-
import org.gjt.sp.jedit.Buffer
import org.gjt.sp.jedit.View
import org.gjt.sp.jedit.io
import org.gjt.sp.jedit.io.VFSFile
import org.gjt.sp.jedit.io.VFSManager
-object VFS {
- val converter = new Interpretation()
-
+
+object VFS {
val BUFFER_SIZE = 1024
- def inputConverter(in : InputStream) = {
- val reader = new InputStreamReader(in, "UTF-8")
- val buffer = new StringBuffer()
+ def input_converter(isabelle_system: IsabelleSystem, in: InputStream) = {
+ val reader = new InputStreamReader(in, Isabelle.system.charset)
+ val buffer = new StringBuilder
val array = new Array[Char](BUFFER_SIZE)
var finished = false
- while (! finished) {
+ while (!finished) {
val length = reader.read(array, 0, array.length)
if (length == -1)
finished = true
@@ -35,31 +38,33 @@
buffer.append(array, 0, length)
}
- val str = converter.decode(buffer.toString())
- new ByteArrayInputStream(str.getBytes("UTF-8"))
+ val str = Isabelle.symbols.decode(buffer.toString)
+ new ByteArrayInputStream(str.getBytes(isabelle_system.charset))
}
- class OutputConverter(out : OutputStream) extends ByteArrayOutputStream {
+ class OutputConverter(out: OutputStream) extends ByteArrayOutputStream {
override def close() {
- out.write(converter.encode(new String(buf, 0, count)).getBytes())
+ out.write(Isabelle.symbols.encode(new String(buf, 0, count)).getBytes)
out.close()
}
}
- def mapFile(vfs : VFS, base : VFSFile) =
+ def map_file(vfs: VFS, base: VFSFile) =
if (base == null) null else new File(vfs, base)
- class File(vfs : VFS, base : VFSFile) extends VFSFile {
+ class File(vfs: VFS, base: VFSFile) extends VFSFile {
+ // FIXME redundant overriding (!??)
+
override def getColor() =
base.getColor()
override def getDeletePath() =
base.getDeletePath()
- override def getExtendedAttribute(name : String) =
+ override def getExtendedAttribute(name: String) =
base.getExtendedAttribute(name)
- override def getIcon(expanded : Boolean, openBuffer : Boolean) =
+ override def getIcon(expanded: Boolean, openBuffer: Boolean) =
base.getIcon(expanded, openBuffer)
override def getLength() =
@@ -69,7 +74,7 @@
base.getName()
override def getPath() =
- Plugin.VFS_PREFIX + base.getPath()
+ Isabelle.VFS_PREFIX + base.getPath()
override def getSymlinkPath() =
base.getSymlinkPath()
@@ -80,7 +85,7 @@
override def getVFS() =
vfs
- override def isBinary(session : Object) =
+ override def isBinary(session: Object) =
base.isBinary(session)
override def isHidden() =
@@ -92,52 +97,44 @@
override def isWriteable() =
base.isWriteable()
- override def setDeletePath(path : String) =
+ override def setDeletePath(path: String) =
base.setDeletePath(path)
- override def setHidden(hidden : Boolean) =
+ override def setHidden(hidden: Boolean) =
base.setHidden(hidden)
- override def setLength(length : Long) =
+ override def setLength(length: Long) =
base.setLength(length)
- override def setName(name : String) =
+ override def setName(name: String) =
base.setName(name)
- override def setPath(path : String) =
+ override def setPath(path: String) =
base.setPath(path)
- override def setReadable(readable : Boolean) =
+ override def setReadable(readable: Boolean) =
base.setReadable(readable)
- override def setWriteable(writeable : Boolean) =
+ override def setWriteable(writeable: Boolean) =
base.setWriteable(writeable)
- override def setSymlinkPath(symlinkPath : String) =
+ override def setSymlinkPath(symlinkPath: String) =
base.setSymlinkPath(symlinkPath)
- override def setType(fType : Int) =
+ override def setType(fType: Int) =
base.setType(fType)
- }
-
+ }
}
-/**
- * The Isabelle virtual file system for jEdit.
- *
- * This filesystem passes every operation on to FileVFS. Just the read and write
- * operations are overwritten to convert the xsymbols to unicode on read and
- * unicode to xsymbols on write.
- *
- * @author Johannes Hölzl <hoelzl@in.tum.de>
- */
-class VFS extends io.VFS("isabelle", VFSManager.getVFSForProtocol("file").getCapabilities()) {
- private var baseVFS = VFSManager.getVFSForProtocol("file")
+
+class VFS extends io.VFS("isabelle", VFSManager.getVFSForProtocol("file").getCapabilities) {
+ private var baseVFS = VFSManager.getVFSForProtocol("file")
- private def cutPath(path : String) =
- if (path.startsWith(Plugin.VFS_PREFIX)) path.substring(Plugin.VFS_PREFIX.length) else path
+ private def cutPath(path: String) =
+ if (path.startsWith(Isabelle.VFS_PREFIX)) path.substring(Isabelle.VFS_PREFIX.length)
+ else path
- override def createVFSSession(path : String, comp : Component) =
+ override def createVFSSession(path: String, comp: Component) =
baseVFS.createVFSSession(cutPath(path), comp)
override def getCapabilities() =
@@ -146,54 +143,49 @@
override def getExtendedAttributes() =
baseVFS.getExtendedAttributes()
- override def getParentOfPath(path : String) =
- Plugin.VFS_PREFIX + baseVFS.getParentOfPath(cutPath(path))
+ override def getParentOfPath(path: String) =
+ Isabelle.VFS_PREFIX + baseVFS.getParentOfPath(cutPath(path))
- override def constructPath(parent : String, path : String) =
- Plugin.VFS_PREFIX + baseVFS.constructPath(cutPath(parent), path)
+ override def constructPath(parent: String, path: String) =
+ Isabelle.VFS_PREFIX + baseVFS.constructPath(cutPath(parent), path)
- override def getFileName(path : String) =
+ override def getFileName(path: String) =
baseVFS.getFileName(path)
override def getFileSeparator() =
baseVFS.getFileSeparator()
- override def getTwoStageSaveName(path : String) =
- Plugin.VFS_PREFIX + baseVFS.getTwoStageSaveName(cutPath(path))
+ override def getTwoStageSaveName(path: String) =
+ Isabelle.VFS_PREFIX + baseVFS.getTwoStageSaveName(cutPath(path))
- override def _canonPath(session : Object, path : String, comp : Component) =
- Plugin.VFS_PREFIX + baseVFS._canonPath(session, cutPath(path), comp)
+ override def _canonPath(session: Object, path: String, comp: Component) =
+ Isabelle.VFS_PREFIX + baseVFS._canonPath(session, cutPath(path), comp)
- override def _createInputStream(session : Object, path : String,
- ignoreErrors : Boolean, comp : Component) =
- VFS.inputConverter(baseVFS._createInputStream(session, cutPath(path),
- ignoreErrors, comp))
+ override def _createInputStream(session: Object, path: String,
+ ignoreErrors: Boolean, comp: Component) =
+ VFS.input_converter(Isabelle.system, baseVFS._createInputStream(session, cutPath(path), ignoreErrors, comp))
- override def _createOutputStream(session : Object, path : String,
- comp : Component) =
+ override def _createOutputStream(session: Object, path: String, comp: Component) =
new VFS.OutputConverter(baseVFS._createOutputStream(session, cutPath(path), comp))
- override def _delete(session : Object, path : String, comp : Component) =
+ override def _delete(session: Object, path: String, comp: Component) =
baseVFS._delete(session, cutPath(path), comp)
- override def _getFile(session : Object, path : String, comp : Component) =
- VFS.mapFile(this, baseVFS._getFile(session, cutPath(path), comp))
+ override def _getFile(session: Object, path: String, comp: Component) =
+ VFS.map_file(this, baseVFS._getFile(session, cutPath(path), comp))
- override def _listFiles(session : Object, path : String, comp : Component): Array[VFSFile] =
- (baseVFS._listFiles(session, cutPath(path), comp)
- .map(file => VFS.mapFile(this, file)))
+ override def _listFiles(session: Object, path: String, comp: Component): Array[VFSFile] =
+ (baseVFS._listFiles(session, cutPath(path), comp).map(file => VFS.map_file(this, file)))
- override def _mkdir(session : Object, path : String, comp : Component) =
+ override def _mkdir(session: Object, path: String, comp: Component) =
baseVFS._mkdir(session, cutPath(path), comp)
- override def _rename(session : Object, from : String, to : String,
- comp : Component) =
+ override def _rename(session: Object, from: String, to: String, comp: Component) =
baseVFS._rename(session, cutPath(from), cutPath(to), comp)
- override def _backup(session : Object, path : String, comp : Component) =
- baseVFS._backup(session, cutPath(path), comp);
+ override def _backup(session: Object, path: String, comp: Component) =
+ baseVFS._backup(session, cutPath(path), comp)
- override def _saveComplete(session : Object, buffer : Buffer, path : String,
- comp : Component) =
+ override def _saveComplete(session: Object, buffer: Buffer, path: String, comp: Component) =
baseVFS._saveComplete(session, buffer, cutPath(path), comp)
}
--- a/src/Tools/jEdit/src/proofdocument/ProofDocument.scala Fri Dec 19 11:25:06 2008 +0100
+++ b/src/Tools/jEdit/src/proofdocument/ProofDocument.scala Sat Jan 10 17:59:23 2009 +0100
@@ -1,8 +1,13 @@
+/*
+ * Document as list of tokens
+ *
+ * @author Johannes Hölzl, TU Munich
+ */
+
package isabelle.proofdocument
import java.util.regex.Pattern
-import isabelle.utils.EventSource
object ProofDocument {
// Be carefully when changeing this regex. Not only must it handle the
@@ -30,15 +35,14 @@
protected var lastToken : Token[C] = null
private var active = false
- {
- text.changes.add(e => textChanged(e.start, e.added, e.removed))
- }
+ text.changes += (e => textChanged(e.start, e.added, e.removed))
- def activate() : Unit =
- if (! active) {
+ def activate() {
+ if (!active) {
active = true
textChanged(0, text.length, 0)
}
+ }
protected def tokens(start : Token[C], stop : Token[C]) =
new Iterator[Token[C]]() {
@@ -218,7 +222,7 @@
tokenChanged(beforeChange, afterChange, firstRemoved)
}
- protected def isStartKeyword(str : String) : Boolean;
+ protected def isStartKeyword(str: String): Boolean
protected def tokenChanged(start : Token[C], stop : Token[C],
removed : Token[C])
--- a/src/Tools/jEdit/src/proofdocument/Text.scala Fri Dec 19 11:25:06 2008 +0100
+++ b/src/Tools/jEdit/src/proofdocument/Text.scala Sat Jan 10 17:59:23 2009 +0100
@@ -1,14 +1,18 @@
+/*
+ * Text as event source
+ *
+ * @author Johannes Hölzl, TU Munich
+ */
+
package isabelle.proofdocument
-import isabelle.utils.EventSource
object Text {
- class Changed(val start : Int, val added : Int, val removed : Int) { }
+ class Changed(val start: Int, val added: Int, val removed: Int)
}
trait Text {
- def content(start : Int, stop : Int) : String
- def length : Int
-
- def changes : EventSource[Text.Changed]
+ def content(start: Int, stop: Int): String
+ def length: Int
+ def changes: EventBus[Text.Changed]
}
--- a/src/Tools/jEdit/src/proofdocument/Token.scala Fri Dec 19 11:25:06 2008 +0100
+++ b/src/Tools/jEdit/src/proofdocument/Token.scala Sat Jan 10 17:59:23 2009 +0100
@@ -1,3 +1,10 @@
+/*
+ * Document tokens as text ranges
+ *
+ * @author Johannes Hölzl, TU Munich
+ * @author Fabian Immler, TU Munich
+ */
+
package isabelle.proofdocument
object Token {
--- a/src/Tools/jEdit/src/prover/Command.scala Fri Dec 19 11:25:06 2008 +0100
+++ b/src/Tools/jEdit/src/prover/Command.scala Sat Jan 10 17:59:23 2009 +0100
@@ -1,90 +1,103 @@
+/*
+ * Prover commands with semantic state
+ *
+ * @author Johannes Hölzl, TU Munich
+ * @author Fabian Immler, TU Munich
+ */
+
package isabelle.prover
-import isabelle.proofdocument.Token
-import isabelle.jedit.Plugin
-import isabelle.{ YXML, XML }
-import sidekick.{SideKickParsedData, IAsset}
+
import javax.swing.text.Position
import javax.swing.tree.DefaultMutableTreeNode
+import isabelle.proofdocument.Token
+import isabelle.jedit.{Isabelle, Plugin}
+import isabelle.{YXML, XML}
+
+import sidekick.{SideKickParsedData, IAsset}
+
+
object Command {
- object Phase extends Enumeration {
+ object Status extends Enumeration {
val UNPROCESSED = Value("UNPROCESSED")
val FINISHED = Value("FINISHED")
val REMOVE = Value("REMOVE")
val REMOVED = Value("REMOVED")
val FAILED = Value("FAILED")
}
-
- private var nextId : Long = 0
- def generateId : Long = {
- nextId = nextId + 1
- return nextId
- }
-
- def idFromString(id : String) = Long.unbox(java.lang.Long.valueOf(id, 36))
}
-class Command(val document : Document, val first : Token[Command], val last : Token[Command]) {
- import Command._
+
+class Command(val document: Document, val first: Token[Command], val last: Token[Command])
+{
+ val id = Isabelle.plugin.id()
{
var t = first
- while(t != null) {
+ while (t != null) {
t.command = this
t = if (t == last) null else t.next
}
}
-
- val id : Long = generateId
+
+
+ /* command status */
- private var p = Phase.UNPROCESSED
- def phase = p
- def phase_=(p_new : Phase.Value) = {
- if(p_new == Phase.UNPROCESSED){
- //delete inner syntax
- for(child <- root_node.children){
+ private var _status = Command.Status.UNPROCESSED
+ def status = _status
+ def status_=(st: Command.Status.Value) = {
+ if (st == Command.Status.UNPROCESSED) {
+ // delete markup
+ for (child <- root_node.children) {
child.children = Nil
}
}
- p = p_new
- }
-
- var results = Nil : List[XML.Tree]
-
- def idString = java.lang.Long.toString(id, 36)
- def results_xml = XML.document(results match {
- case Nil => XML.Elem("message", List(), List())
- case List(elem) => elem
- case _ =>
- XML.Elem("messages", List(), List(results.first,
- results.last))
- }, "style")
- def addResult(tree : XML.Tree) {
- results = results ::: List(tree)
- }
-
- val root_node =
- new MarkupNode(this, 0, stop - start, idString, "Command", document.getContent(this))
-
- def node_from(kind : String, begin : Int, end : Int) : MarkupNode = {
- val markup_content = /*content.substring(begin, end)*/ ""
- new MarkupNode(this, begin, end, idString, kind, markup_content)
+ _status = st
}
- def content = document.getContent(this)
+
+ /* accumulated results */
+
+ var results: List[XML.Tree] = Nil
+
+ def results_xml = XML.document(
+ results match {
+ case Nil => XML.Elem("message", Nil, Nil)
+ case List(elem) => elem
+ case _ => XML.Elem("messages", Nil, List(results.first, results.last))
+ }, "style")
+ def add_result(tree: XML.Tree) {
+ results = results ::: List(tree) // FIXME canonical reverse order
+ }
+
+
+ /* content */
+
+ def content(): String = document.getContent(this)
def next = if (last.next != null) last.next.command else null
def previous = if (first.previous != null) first.previous.command else null
- def start = first start
- def stop = last stop
-
- def properStart = start
- def properStop = {
+ def start = first.start
+ def stop = last.stop
+
+ def proper_start = start
+ def proper_stop = {
var i = last
while (i != first && i.kind.equals(Token.Kind.COMMENT))
i = i.previous
i.stop
- }
-}
\ No newline at end of file
+ }
+
+
+ /* markup tree */
+
+ val root_node =
+ new MarkupNode(this, 0, stop - start, id, Markup.COMMAND_SPAN, content())
+
+ def node_from(kind: String, begin: Int, end: Int) = {
+ val markup_content = /*content.substring(begin, end)*/ ""
+ new MarkupNode(this, begin, end, id, kind, markup_content)
+ }
+}
--- a/src/Tools/jEdit/src/prover/CommandChangeInfo.scala Fri Dec 19 11:25:06 2008 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,3 +0,0 @@
-package isabelle.prover
-
-class CommandChangeInfo(val command : Command)
--- a/src/Tools/jEdit/src/prover/Document.scala Fri Dec 19 11:25:06 2008 +0100
+++ b/src/Tools/jEdit/src/prover/Document.scala Sat Jan 10 17:59:23 2009 +0100
@@ -1,8 +1,13 @@
+/*
+ * Document as list of commands
+ *
+ * @author Johannes Hölzl, TU Munich
+ */
+
package isabelle.prover
-import isabelle.proofdocument.{ ProofDocument, Token, Text }
+import isabelle.proofdocument.{ProofDocument, Token, Text}
-import isabelle.utils.EventSource
object Document {
class StructureChange(val beforeChange : Command,
@@ -10,36 +15,37 @@
val removedCommands : List[Command])
}
+
class Document(text : Text, val prover : Prover) extends ProofDocument[Command](text)
-{
- val structuralChanges = new EventSource[Document.StructureChange]()
-
+{
+ val structural_changes = new EventBus[Document.StructureChange]
+
def isStartKeyword(s : String) = prover.command_decls.contains(s)
-
+
def commands() = new Iterator[Command] {
var current = firstToken
def hasNext() = current != null
def next() = { try {val s = current.command ; current = s.last.next ; s}
- catch { case error : NullPointerException =>
+ catch { case error : NullPointerException =>
System.err.println("NPE!")
throw error
- }
+ }
}
}
- def getContent(cmd : Command) = text.content(cmd.properStart, cmd.properStop)
+ def getContent(cmd : Command) = text.content(cmd.proper_start, cmd.proper_stop)
def getNextCommandContaining(pos : Int) : Command = {
for( cmd <- commands()) { if (pos < cmd.stop) return cmd }
return null
}
-
- override def tokenChanged(start : Token[Command], stop : Token[Command],
+
+ override def tokenChanged(start : Token[Command], stop : Token[Command],
removed : Token[Command]) {
var removedCommands : List[Command] = Nil
var first : Command = null
var last : Command = null
-
+
for(t <- tokens(removed)) {
if (first == null)
first = t.command
@@ -59,7 +65,7 @@
else
before = first.previous
}
-
+
var addedCommands : List[Command] = Nil
var scan : Token[Command] = null
if (start != null) {
@@ -90,7 +96,7 @@
}
else
scan = firstToken
-
+
var stopScan : Token[Command] = null
if (stop != null) {
if (stop == stop.command.first)
@@ -102,19 +108,19 @@
stopScan = last.last.next
else
stopScan = null
-
+
var cmdStart : Token[Command] = null
var cmdStop : Token[Command] = null
var overrun = false
var finished = false
while (scan != null && !finished) {
- if (scan == stopScan) {
+ if (scan == stopScan) {
if (scan.kind.equals(Token.Kind.COMMAND_START))
finished = true
else
overrun = true
}
-
+
if (scan.kind.equals(Token.Kind.COMMAND_START) && cmdStart != null && !finished) {
if (! overrun) {
addedCommands = new Command(this, cmdStart, cmdStop) :: addedCommands
@@ -134,19 +140,19 @@
removedCommands = scan.command :: removedCommands
last = scan.command
}
-
+
if (!finished)
scan = scan.next
}
-
+
if (cmdStart != null)
addedCommands = new Command(this, cmdStart, cmdStop) :: addedCommands
-
+
// relink commands
addedCommands = addedCommands.reverse
removedCommands = removedCommands.reverse
-
- structuralChanges.fire(new Document.StructureChange(before, addedCommands,
- removedCommands))
+
+ structural_changes.event(
+ new Document.StructureChange(before, addedCommands, removedCommands))
}
}
--- a/src/Tools/jEdit/src/prover/IsabelleSKParser.scala Fri Dec 19 11:25:06 2008 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,38 +0,0 @@
-/*
- * IsabelleSKParser.scala
- *
- * To change this template, choose Tools | Template Manager
- * and open the template in the editor.
- */
-
-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;
-
-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)
-
- for(command <- document.commands){
- data.root.add(command.root_node.swing_node)
- }
- data
- }
- }
-
-}
--- a/src/Tools/jEdit/src/prover/MarkupNode.scala Fri Dec 19 11:25:06 2008 +0100
+++ b/src/Tools/jEdit/src/prover/MarkupNode.scala Sat Jan 10 17:59:23 2009 +0100
@@ -1,8 +1,7 @@
/*
- * RelativeAsset.scala
+ * Document markup nodes, with connection to Swing tree model
*
- * To change this template, choose Tools | Template Manager
- * and open the template in the editor.
+ * @author Fabian Immler, TU Munich
*/
package isabelle.prover
--- a/src/Tools/jEdit/src/prover/Prover.scala Fri Dec 19 11:25:06 2008 +0100
+++ b/src/Tools/jEdit/src/prover/Prover.scala Sat Jan 10 17:59:23 2009 +0100
@@ -1,204 +1,168 @@
+/*
+ * Higher-level prover communication
+ *
+ * @author Johannes Hölzl, TU Munich
+ * @author Fabian Immler, TU Munich
+ * @author Makarius
+ */
+
package isabelle.prover
-import scala.collection.mutable.{ HashMap, HashSet }
import java.util.Properties
-import javax.swing.SwingUtilities
+import scala.collection.mutable.{HashMap, HashSet}
-import isabelle.proofdocument.{ ProofDocument, Text, Token }
-import isabelle.IsabelleProcess.Result
-import isabelle.YXML.parse_failsafe
-import isabelle.XML.{ Elem, Tree }
-import isabelle.Symbol.Interpretation
-import isabelle.IsabelleSyntax.{ encode_properties, encode_string }
+import org.gjt.sp.util.Log
+
+import isabelle.proofdocument.{ProofDocument, Text, Token}
+
-import isabelle.utils.EventSource
-
-import Command.Phase
+class Prover(isabelle_system: IsabelleSystem, isabelle_symbols: Symbol.Interpretation)
+{
+ private var _logic = isabelle_system.getenv_strict("ISABELLE_LOGIC")
+ private var process: Isar = null
+ private var commands = new HashMap[String, Command]
-class Prover() {
- val converter = new Interpretation()
-
- private var _logic = "HOL"
- private var process = null : IsabelleProcess
- private var commands = new HashMap[String, Command]
-
val command_decls = new HashSet[String]
val keyword_decls = new HashSet[String]
private var initialized = false
-
- val activated = new EventSource[Unit]
- val commandInfo = new EventSource[CommandChangeInfo]
- val outputInfo = new EventSource[String]
- val allInfo = new EventSource[Result]
- var document = null : Document
+
+ val activated = new EventBus[Unit]
+ val command_info = new EventBus[Command]
+ val output_info = new EventBus[String]
+ var document: Document = null
- def fireChange(c : Command) =
- inUIThread(() => commandInfo.fire(new CommandChangeInfo(c)))
+
+ def command_change(c: Command) = Swing.now { command_info.event(c) }
+
+ private def handle_result(r: IsabelleProcess.Result) = {
+ val id = if (r.props != null) r.props.getProperty(Markup.ID) else null
+ val st = if (id != null) commands.getOrElse(id, null) else null
- val worker_thread = new Thread("isabelle.Prover: worker") {
- override def run() : Unit = {
- while (true) {
- val r = process.get_result
-
- val id = if (r.props != null) r.props.getProperty("id") else null
- val st = if (id != null) commands.getOrElse(id, null) else null
-
- if (r.kind == IsabelleProcess.Kind.EXIT)
- return
- else if (r.kind == IsabelleProcess.Kind.STDOUT
- || r.kind == IsabelleProcess.Kind.STDIN)
- inUIThread(() => outputInfo.fire(r.result))
- else if (r.kind == IsabelleProcess.Kind.WRITELN && !initialized) {
- initialized = true
- inUIThread(() =>
- if (document != null) {
- document.activate()
- activated.fire(())
- }
- )
+ if (r.kind == IsabelleProcess.Kind.STDOUT || r.kind == IsabelleProcess.Kind.STDIN)
+ Swing.now { output_info.event(r.result) }
+ else if (r.kind == IsabelleProcess.Kind.WRITELN && !initialized) {
+ initialized = true
+ Swing.now {
+ if (document != null) {
+ document.activate()
+ activated.event(())
}
- else {
- val tree = parse_failsafe(converter.decode(r.result))
- if (st == null || (st.phase != Phase.REMOVED && st.phase != Phase.REMOVE))
- tree match {
- //handle all kinds of status messages here
- case Elem("message", List(("class","status")), elems) =>
- elems map (elem => elem match{
+ }
+ }
+ else {
+ val tree = YXML.parse_failsafe(isabelle_symbols.decode(r.result))
+ if (st == null || (st.status != Command.Status.REMOVED && st.status != Command.Status.REMOVE)) {
+ r.kind match {
- // catch command_start and keyword declarations
- case Elem("command_decl", List(("name", name), ("kind", _)), _) =>
- command_decls.addEntry(name)
- case Elem("keyword_decl", List(("name", name)), _) =>
- keyword_decls.addEntry(name)
+ case IsabelleProcess.Kind.STATUS =>
+ //{{{ handle all kinds of status messages here
+ tree match {
+ case XML.Elem(Markup.MESSAGE, _, elems) =>
+ for (elem <- elems) {
+ elem match {
+ //{{{
+ // command status
+ case XML.Elem(Markup.FINISHED, _, _) =>
+ st.status = Command.Status.FINISHED
+ command_change(st)
+ case XML.Elem(Markup.UNPROCESSED, _, _) =>
+ st.status = Command.Status.UNPROCESSED
+ command_change(st)
+ case XML.Elem(Markup.FAILED, _, _) =>
+ st.status = Command.Status.FAILED
+ command_change(st)
+ case XML.Elem(Markup.DISPOSED, _, _) =>
+ document.prover.commands.removeKey(st.id)
+ st.status = Command.Status.REMOVED
+ command_change(st)
- // expecting markups here
- case Elem(kind, List(("offset", offset),
- ("end_offset", end_offset),
- ("id", id)), List()) =>
- val begin = Int.unbox(java.lang.Integer.valueOf(offset)) - 1
- val end = Int.unbox(java.lang.Integer.valueOf(end_offset)) - 1
-
- val command =
- // outer syntax: no id in props
- if(st == null) commands.getOrElse(id, null)
- // inner syntax: id from props
- else st
- command.root_node.insert(command.node_from(kind, begin, end))
+ // command and keyword declarations
+ case XML.Elem(Markup.COMMAND_DECL, (Markup.NAME, name) :: _, _) =>
+ command_decls += name
+ case XML.Elem(Markup.KEYWORD_DECL, (Markup.NAME, name) :: _, _) =>
+ keyword_decls += name
- // Phase changed
- case Elem("finished", _, _) =>
- st.phase = Phase.FINISHED
- fireChange(st)
- case Elem("unprocessed", _, _) =>
- st.phase = Phase.UNPROCESSED
- fireChange(st)
- case Elem("failed", _, _) =>
- st.phase = Phase.FAILED
- fireChange(st)
- case Elem("removed", _, _) =>
- document.prover.commands.removeKey(st.idString)
- st.phase = Phase.REMOVED
- fireChange(st)
- case _ =>
- })
- case _ =>
- if (st != null)
- handleResult(st, r, tree)
- }
+ // other markup
+ case XML.Elem(kind,
+ (Markup.OFFSET, offset) :: (Markup.END_OFFSET, end_offset) ::
+ (Markup.ID, markup_id) :: _, _) =>
+ val begin = Int.unbox(java.lang.Integer.valueOf(offset)) - 1
+ val end = Int.unbox(java.lang.Integer.valueOf(end_offset)) - 1
+
+ val command =
+ // outer syntax: no id in props
+ if (st == null) commands.getOrElse(markup_id, null)
+ // inner syntax: id from props
+ else st
+ command.root_node.insert(command.node_from(kind, begin, end))
+
+ case _ =>
+ //}}}
+ }
+ }
+ case _ =>
+ }
+ //}}}
+
+ case IsabelleProcess.Kind.ERROR if st != null =>
+ if (st.status != Command.Status.REMOVED && st.status != Command.Status.REMOVE)
+ st.status = Command.Status.FAILED
+ st.add_result(tree)
+ command_change(st)
+
+ case IsabelleProcess.Kind.WRITELN | IsabelleProcess.Kind.PRIORITY
+ | IsabelleProcess.Kind.WARNING if st != null =>
+ st.add_result(tree)
+ command_change(st)
+
+ case _ =>
}
-
}
}
}
-
- def handleResult(st : Command, r : Result, tree : XML.Tree) {
+
- r.kind match {
- case IsabelleProcess.Kind.ERROR =>
- if (st.phase != Phase.REMOVED && st.phase != Phase.REMOVE)
- st.phase = Phase.FAILED
- st.addResult(tree)
- fireChange(st)
-
- case IsabelleProcess.Kind.WRITELN =>
- st.addResult(tree)
- fireChange(st)
-
- case IsabelleProcess.Kind.PRIORITY =>
- st.addResult(tree)
- fireChange(st)
+ def start(logic: String) {
+ if (logic != null) _logic = logic
- case IsabelleProcess.Kind.WARNING =>
- st.addResult(tree)
- fireChange(st)
-
- case IsabelleProcess.Kind.STATUS =>
- System.err.println("handleResult - Ignored: " + tree)
+ val results = new EventBus[IsabelleProcess.Result]
+ results += handle_result
+ results.logger = Log.log(Log.ERROR, null, _)
- case _ =>
- }
- }
-
- def logic = _logic
-
- def start(logic : String) {
- if (logic != null)
- _logic = logic
- process = new IsabelleProcess("-m", "xsymbols", _logic)
- worker_thread.start
+ process = new Isar(isabelle_system, results, "-m", "xsymbols", _logic)
}
def stop() {
process.kill
}
-
- private def inUIThread(runnable : () => Unit) {
- SwingUtilities invokeAndWait new Runnable() {
- override def run() { runnable () }
- }
- }
-
- def setDocument(text : Text, path : String) {
+
+ def set_document(text: Text, path: String) {
this.document = new Document(text, this)
- process.ML("ThyLoad.add_path " + encode_string(path))
+ process.ML("ThyLoad.add_path " + IsabelleSyntax.encode_string(path))
- document.structuralChanges.add(changes => {
+ document.structural_changes += (changes => {
for (cmd <- changes.removedCommands) remove(cmd)
for (cmd <- changes.addedCommands) send(cmd)
})
if (initialized) {
document.activate()
- activated.fire(())
+ activated.event(())
}
}
-
- private def send(cmd : Command) {
- commands.put(cmd.idString, cmd)
-
- val props = new Properties()
- props.setProperty("id", cmd.idString)
- props.setProperty("offset", Integer.toString(1))
+
+ private def send(cmd: Command) {
+ cmd.status = Command.Status.UNPROCESSED
+ commands.put(cmd.id, cmd)
- val content = converter.encode(document.getContent(cmd))
- process.output_sync("Isar.command "
- + encode_properties(props)
- + " "
- + encode_string(content))
-
- process.output_sync("Isar.insert "
- + encode_string(if (cmd.previous == null) ""
- else cmd.previous.idString)
- + " "
- + encode_string(cmd.idString))
-
- cmd.phase = Phase.UNPROCESSED
+ val content = isabelle_symbols.encode(document.getContent(cmd))
+ process.create_command(cmd.id, content)
+ process.insert_command(if (cmd.previous == null) "" else cmd.previous.id, cmd.id)
}
-
- def remove(cmd : Command) {
- cmd.phase = Phase.REMOVE
- process.output_sync("Isar.remove " + encode_string(cmd.idString))
+ def remove(cmd: Command) {
+ cmd.status = Command.Status.REMOVE
+ process.remove_command(cmd.id)
}
-}
\ No newline at end of file
+}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/renderer/UserAgent.scala Sat Jan 10 17:59:23 2009 +0100
@@ -0,0 +1,48 @@
+/*
+ * XML/CSS rendering -- user agent
+ *
+ * @author Fabian Immler, TU Munich
+ * @author Johannes Hölzl, TU Munich
+ */
+
+package isabelle.renderer
+
+
+import java.io.ByteArrayInputStream
+import org.xhtmlrenderer.swing.NaiveUserAgent
+import org.xhtmlrenderer.resource.CSSResource
+
+
+object UserAgent {
+ // FIXME avoid static getenv
+ val baseURL = "file://localhost" + System.getenv("ISABELLE_HOME") + "/lib/html/"
+ val userStylesheet = "file://localhost" + System.getenv("ISABELLE_HOME_USER") + "/etc/user.css"
+ val stylesheet = """
+
+@import "isabelle.css";
+
+@import '""" + userStylesheet + """';
+
+messages, message {
+ display: block;
+ white-space: pre-wrap;
+ font-family: Isabelle;
+}
+"""
+}
+
+class UserAgent extends NaiveUserAgent {
+ override def getCSSResource(uri : String) : CSSResource = {
+ if (uri == UserAgent.baseURL + "style")
+ new CSSResource(
+ new ByteArrayInputStream(UserAgent.stylesheet.getBytes()))
+ else {
+ val stream = resolveAndOpenStream(uri)
+ val resource = new CSSResource(stream)
+ if (stream == null)
+ resource.getResourceInputSource().setByteStream(
+ new ByteArrayInputStream(new Array[Byte](0)))
+ resource
+ }
+ }
+}
\ No newline at end of file
--- a/src/Tools/jEdit/src/utils/Delay.scala Fri Dec 19 11:25:06 2008 +0100
+++ b/src/Tools/jEdit/src/utils/Delay.scala Sat Jan 10 17:59:23 2009 +0100
@@ -1,3 +1,9 @@
+/*
+ * Delayed actions
+ *
+ * @author Fabian Immler, TU Munich
+ */
+
package isabelle.utils
import javax.swing.Timer
--- a/src/Tools/jEdit/src/utils/EventSource.scala Fri Dec 19 11:25:06 2008 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,12 +0,0 @@
-package isabelle.utils
-
-import scala.collection.mutable.HashSet
-
-class EventSource[Event] {
- private val handlers = new HashSet[(Event) => Unit]()
-
- def add(handler : (Event) => Unit) { handlers += handler }
- def remove(handler : (Event) => Unit) { handlers -= handler }
-
- def fire(event : Event) { for(h <- handlers) h(event) }
-}
\ No newline at end of file