original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/plugin/IsabellePlugin.ant Sun Oct 19 16:51:55 2008 +0200
@@ -0,0 +1,10 @@
+<?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
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/plugin/IsabellePlugin.props Sun Oct 19 16:51:55 2008 +0200
@@ -0,0 +1,24 @@
+# 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-output.label=Show Output
+Isabelle.show-state.label=Show State
+Isabelle.activate.label=Activate current buffer
+
+Isabelle_output.title=Isabelle Output
+Isabelle_state.title=Isabelle State
+
+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
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/plugin/actions.xml Sun Oct 19 16:51:55 2008 +0200
@@ -0,0 +1,20 @@
+<ACTIONS>
+ <ACTION NAME="Isabelle.show-output">
+ <CODE>
+ wm.addDockableWindow("Isabelle_output");
+ </CODE>
+ </ACTION>
+ <ACTION NAME="Isabelle.show-state">
+ <CODE>
+ wm.addDockableWindow("Isabelle_state");
+ </CODE>
+ </ACTION>
+ <ACTION NAME="Isabelle.activate">
+ <CODE>
+ isabelle.jedit.Plugin$.MODULE$.plugin().activate(view);
+ </CODE>
+ <IS_SELECTED>
+ return view.getBuffer().getMode().getName() == "isabelle";
+ </IS_SELECTED>
+ </ACTION>
+</ACTIONS>
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/plugin/dockables.xml Sun Oct 19 16:51:55 2008 +0200
@@ -0,0 +1,12 @@
+<?xml version="1.0"?>
+
+<!DOCTYPE DOCKABLES SYSTEM "dockables.dtd">
+
+<DOCKABLES>
+ <DOCKABLE NAME="Isabelle_output">
+ new isabelle.jedit.OutputDockable(view, position);
+ </DOCKABLE>
+ <DOCKABLE NAME="Isabelle_state">
+ new isabelle.jedit.StateViewDockable(view, position);
+ </DOCKABLE>
+</DOCKABLES>
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/plugin/services.xml Sun Oct 19 16:51:55 2008 +0200
@@ -0,0 +1,7 @@
+<?xml version="1.0"?>
+<!DOCTYPE SERVICES SYSTEM "services.dtd">
+<SERVICES>
+ <SERVICE NAME="isa" CLASS="org.gjt.sp.jedit.io.VFS">
+ new isabelle.jedit.VFS();
+ </SERVICE>
+</SERVICES>
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/jedit/OptionPane.scala Sun Oct 19 16:51:55 2008 +0200
@@ -0,0 +1,83 @@
+package isabelle.jedit
+
+import java.lang.Integer
+
+import java.awt.BorderLayout
+import java.awt.GridBagConstraints.HORIZONTAL
+import java.awt.BorderLayout.{ WEST, CENTER, EAST }
+import java.awt.event.{ ActionListener, ActionEvent }
+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
+
+ var pathName = new JTextField()
+ var fontSize = new JSpinner()
+ var logicName = new JComboBox()
+
+ override def _init() {
+ addComponent(property("font-path.title"), {
+ val pickPath = new JButton("...")
+ pickPath.addActionListener(new ActionListener() {
+ override def actionPerformed(e : ActionEvent) {
+ val chooser = new JFileChooser(pathName.getText())
+ if (chooser.showOpenDialog(OptionPane.this) == JFileChooser.APPROVE_OPTION)
+ pathName.setText(chooser.getSelectedFile().getAbsolutePath())
+ }
+ })
+
+ pathName.setText(property("font-path"))
+
+ val pathPanel = new JPanel(new BorderLayout())
+ pathPanel.add(pathName, CENTER)
+ pathPanel.add(pickPath, EAST)
+ pathPanel
+ }, HORIZONTAL)
+
+ addComponent(property("font-size.title"), {
+ try {
+ if (property("font-size") != null)
+ fontSize.setValue(Integer.valueOf(property("font-size")))
+ }
+ catch {
+ case e : NumberFormatException =>
+ fontSize.setValue(14)
+ }
+
+ fontSize
+ })
+
+ addComponent(property("logic.title"), {
+ val logics : Array[Object] =
+ (IsabelleSystem.isabelle_tool("findlogics") _1).split("\\s").asInstanceOf[Array[Object]]
+ for (name <- logics) {
+ logicName.addItem(name)
+ if (name == property("logic"))
+ logicName.setSelectedItem(name)
+ }
+
+ logicName
+ })
+ }
+
+ override def _save() {
+ val size = fontSize.getValue()
+ val name = pathName.getText()
+ if (property("font-path") != name || property("font-size") != size.toString) {
+ property("font-path", name)
+ property("font-size", size.toString)
+ SwingUtilities invokeLater new Runnable() {
+ override def run() =
+ Plugin.plugin.setFont(name, size.asInstanceOf[Integer].intValue)
+ }
+ }
+
+ val logic = logicName.getSelectedItem.asInstanceOf[String]
+ property("logic", logic)
+ }
+}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/jedit/OutputDockable.scala Sun Oct 19 16:51:55 2008 +0200
@@ -0,0 +1,20 @@
+package isabelle.jedit
+
+import java.awt.GridLayout
+
+import javax.swing.{ JPanel, JTextArea, JScrollPane }
+
+import org.gjt.sp.jedit.View
+
+class OutputDockable(view : View, position : String) extends JPanel {
+ {
+ val textView = new JTextArea()
+
+ setLayout(new GridLayout(1, 1))
+ add(new JScrollPane(textView))
+
+ textView.append("== Isabelle output ==\n")
+
+ Plugin.plugin.prover.outputInfo.add( text => textView.append(text) )
+ }
+}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/jedit/Plugin.scala Sun Oct 19 16:51:55 2008 +0200
@@ -0,0 +1,98 @@
+package isabelle.jedit
+
+import java.awt.Font
+import java.io.{ FileInputStream, IOException }
+
+
+import isabelle.utils.EventSource
+
+import isabelle.prover.{ Prover, Command }
+
+import isabelle.IsabelleSystem
+
+import org.gjt.sp.jedit.{ jEdit, EBMessage, EBPlugin, Buffer, EditPane, View }
+import org.gjt.sp.jedit.msg.{ EditPaneUpdate, PropertiesChanged }
+
+object Plugin {
+ val NAME = "Isabelle"
+ val OPTION_PREFIX = "options.isabelle."
+
+ 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
+}
+
+class Plugin extends EBPlugin {
+ import Plugin._
+
+ val prover = new Prover()
+ var theoryView : TheoryView = null
+
+ var viewFont : Font = null
+ val viewFontChanged = new EventSource[Font]
+
+ private var _selectedState : Command = null
+
+ val stateUpdate = new EventSource[Command]
+
+ def selectedState = _selectedState
+ def selectedState_=(newState : Command) {
+ _selectedState = newState
+ stateUpdate fire newState
+ }
+
+ def activate(view : View) {
+ val logic = property("logic")
+ theoryView = new TheoryView(prover, view.getBuffer())
+ prover.start(if (logic == null) logic else "HOL")
+ val dir = view.getBuffer().getDirectory()
+ prover.setDocument(theoryView,
+ if (dir.startsWith("isa:")) dir.substring(4) else dir)
+ TheoryView.activateTextArea(view.getTextArea())
+ }
+
+ override def handleMessage(msg : EBMessage) = msg match {
+ case epu : EditPaneUpdate => epu.getWhat() match {
+ case EditPaneUpdate.BUFFER_CHANGED =>
+ TheoryView.activateTextArea(epu.getEditPane().getTextArea())
+
+ case EditPaneUpdate.BUFFER_CHANGING =>
+ TheoryView.deactivateTextArea(epu.getEditPane().getTextArea())
+
+ 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
+
+ if (property("font-path") != null && property("font-size") != null)
+ try {
+ setFont(property("font-path"), property("font-size").toFloat)
+ }
+ catch {
+ case e : NumberFormatException =>
+ }
+ }
+
+ override def stop() {
+ // TODO: implement cleanup
+ }
+}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/jedit/StateViewDockable.scala Sun Oct 19 16:51:55 2008 +0200
@@ -0,0 +1,80 @@
+package isabelle.jedit
+
+import java.io.{ ByteArrayInputStream, FileInputStream, InputStream }
+
+import java.awt.GridLayout
+import javax.swing.{ JPanel, JTextArea, JScrollPane }
+
+import isabelle.IsabelleSystem.getenv
+
+import org.xml.sax.InputSource;
+
+import org.w3c.dom.Document
+
+import org.xhtmlrenderer.simple.XHTMLPanel
+import org.xhtmlrenderer.context.AWTFontResolver
+import org.xhtmlrenderer.swing.NaiveUserAgent
+import org.xhtmlrenderer.resource.CSSResource
+
+import org.gjt.sp.jedit.View
+
+object StateViewDockable {
+ 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 == StateViewDockable.baseURL + "style")
+ new CSSResource(
+ new ByteArrayInputStream(StateViewDockable.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
+ }
+ }
+}
+
+class StateViewDockable(view : View, position : String) extends JPanel {
+ {
+ val panel = new XHTMLPanel(new UserAgent())
+ setLayout(new GridLayout(1, 1))
+ add(new JScrollPane(panel))
+
+ val fontResolver =
+ panel.getSharedContext.getFontResolver.asInstanceOf[AWTFontResolver]
+ if (Plugin.plugin.viewFont != null)
+ fontResolver.setFontMapping("Isabelle", Plugin.plugin.viewFont)
+
+ Plugin.plugin.viewFontChanged.add(font => {
+ if (Plugin.plugin.viewFont != null)
+ fontResolver.setFontMapping("Isabelle", Plugin.plugin.viewFont)
+
+ panel.relayout()
+ })
+
+ Plugin.plugin.stateUpdate.add(state => {
+ if (state == null)
+ panel.setDocument(null : Document)
+ else
+ panel.setDocument(state.document, StateViewDockable.baseURL)
+ })
+ }
+}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/jedit/TheoryView.scala Sun Oct 19 16:51:55 2008 +0200
@@ -0,0 +1,244 @@
+package isabelle.jedit
+
+import isabelle.utils.EventSource
+
+import isabelle.proofdocument.Text
+
+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 org.gjt.sp.jedit.buffer.{ BufferListener, JEditBuffer }
+import org.gjt.sp.jedit.textarea.{ TextArea, TextAreaExtension, TextAreaPainter }
+import org.gjt.sp.jedit.syntax.SyntaxStyle
+
+object TheoryView {
+ val ISABELLE_THEORY_PROPERTY = "de.tum.in.isabelle.jedit.Theory";
+
+ def chooseColor(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)
+ case _ => Color.red
+ }
+ }
+
+ def withView(view : TextArea, f : (TheoryView) => Unit) {
+ if (view != null && view.getBuffer() != null)
+ view.getBuffer().getProperty(ISABELLE_THEORY_PROPERTY) match {
+ case null => null
+ case view: TheoryView => f(view)
+ case _ => null
+ }
+ }
+
+ def activateTextArea(textArea : TextArea) {
+ withView(textArea, _.activate(textArea))
+ }
+
+ def deactivateTextArea(textArea : TextArea) {
+ withView(textArea, _.deactivate(textArea))
+ }
+}
+
+class TheoryView(prover : Prover, buffer : JEditBuffer)
+ extends TextAreaExtension with Text with BufferListener {
+ import TheoryView._
+ import Text.Changed
+
+ var textArea : TextArea = null;
+ var col : Changed = null;
+
+ val colTimer = new Timer(300, new ActionListener() {
+ override def actionPerformed(e : ActionEvent) { commit() }
+ })
+
+ val changesSource = new EventSource[Changed]
+
+ {
+ buffer.addBufferListener(this)
+ buffer.setProperty(ISABELLE_THEORY_PROPERTY, this)
+
+ prover.commandInfo.add(e => repaint(e.command))
+ prover.commandInfo.add(e => repaintAll())
+
+ Plugin.plugin.viewFontChanged.add(font => updateFont())
+
+ colTimer.stop
+ colTimer.setRepeats(true)
+ }
+
+ def activate(area : TextArea) {
+ textArea = area
+ textArea.addCaretListener(selectedStateController)
+
+ val painter = textArea.getPainter()
+ painter.addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, this)
+ updateFont()
+ }
+
+ private def updateFont() {
+ if (textArea != null) {
+ val painter = textArea.getPainter()
+ if (Plugin.plugin.viewFont != null) {
+ painter.setStyles(painter.getStyles().map(style =>
+ new SyntaxStyle(style.getForegroundColor,
+ style.getBackgroundColor,
+ Plugin.plugin.viewFont)
+ ))
+ painter.setFont(Plugin.plugin.viewFont)
+ repaintAll()
+ }
+ }
+ }
+
+ def deactivate(area : TextArea) {
+ textArea.getPainter().removeExtension(this)
+ textArea.removeCaretListener(selectedStateController)
+ textArea = null
+ }
+
+ val selectedStateController = new CaretListener() {
+ override def caretUpdate(e : CaretEvent) {
+ val cmd = prover.document.getNextCommandContaining(e.getDot())
+ if (cmd != null && cmd.start <= e.getDot() &&
+ Plugin.plugin.selectedState != cmd)
+ Plugin.plugin.selectedState = cmd
+ }
+ }
+
+ private def fromCurrent(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) =
+ 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)
+ {
+ var ph = cmd.phase
+ if (textArea != null && ph != Phase.REMOVE && ph != Phase.REMOVED) {
+ var start = textArea.getLineOfOffset(toCurrent(cmd.start))
+ var stop = textArea.getLineOfOffset(toCurrent(cmd.stop) - 1)
+ textArea.invalidateLineRange(start, stop)
+
+ if (Plugin.plugin.selectedState == cmd)
+ Plugin.plugin.selectedState = cmd // update State view
+ }
+ }
+
+ def repaintAll()
+ {
+ if (textArea != null)
+ textArea.invalidateLineRange(textArea.getFirstPhysicalLine,
+ textArea.getLastPhysicalLine)
+ }
+
+ override def paintValidLine(gfx : Graphics2D, screenLine : Int,
+ pl : Int, start : Int, end : Int, y : Int)
+ {
+ var fm = textArea.getPainter().getFontMetrics()
+ var savedColor = gfx.getColor()
+ var e = prover.document.getNextCommandContaining(fromCurrent(start))
+
+ while (e != null && toCurrent(e.start) < end) {
+ val begin = Math.max(start, toCurrent(e.start))
+ val startP = textArea.offsetToXY(begin)
+
+ val finish = Math.min(end - 1, toCurrent(e.stop))
+ val stopP = if (finish < buffer.getLength()) textArea.offsetToXY(finish)
+ else { var p = textArea.offsetToXY(finish - 1)
+ p.x = p.x + fm.charWidth(' ')
+ p }
+
+ if (startP != null && stopP != null) {
+ gfx.setColor(chooseColor(e))
+ gfx.fillRect(startP.x, y, stopP.x - startP.x, fm.getHeight())
+ }
+
+ e = e.next
+ }
+
+ gfx.setColor(savedColor)
+ }
+
+ def content(start : Int, stop : Int) = buffer.getText(start, stop - start)
+ def length = buffer.getLength()
+
+ def changes = changesSource
+
+ private def commit() {
+ if (col != null)
+ changes.fire(col)
+ col = null
+ if (colTimer.isRunning())
+ colTimer.stop()
+ }
+
+ private def delayCommit() {
+ if (colTimer.isRunning())
+ colTimer.restart()
+ else
+ colTimer.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 preContentInserted(buffer : JEditBuffer, startLine : Int,
+ offset : Int, numLines : 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 {
+ commit()
+ col = new Changed(offset, length, 0)
+ }
+ delayCommit()
+ }
+
+ override def preContentRemoved(buffer : JEditBuffer, startLine : Int,
+ start : Int, numLines : Int, removed : Int) {
+ if (col == null)
+ col = new Changed(start, 0, removed)
+ else if (col.start > start + removed || start > col.start + col.added) {
+ commit()
+ col = new Changed(start, 0, removed)
+ }
+ else {
+ val offset = start - col.start
+ val diff = col.added - removed
+ val (added, addRemoved) =
+ if (diff < offset)
+ (offset max 0, diff - (offset max 0))
+ else
+ (diff - (offset min 0), offset min 0)
+
+ col = new Changed(start min col.start, added, col.removed - addRemoved)
+ }
+ delayCommit()
+ }
+
+ 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
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/jedit/VFS.scala Sun Oct 19 16:51:55 2008 +0200
@@ -0,0 +1,199 @@
+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.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()
+
+ val BUFFER_SIZE = 1024
+
+ def inputConverter(in : InputStream) = {
+ val reader = new InputStreamReader(in, "UTF-8")
+ val buffer = new StringBuffer()
+ val array = new Array[Char](BUFFER_SIZE)
+
+ var finished = false
+ while (! finished) {
+ val length = reader.read(array, 0, array.length)
+ if (length == -1)
+ finished = true
+ else
+ buffer.append(array, 0, length)
+ }
+
+ val str = converter.decode(buffer.toString())
+ new ByteArrayInputStream(str.getBytes())
+ }
+
+ class OutputConverter(out : OutputStream) extends ByteArrayOutputStream {
+ override def close() {
+ out.write(converter.encode(new String(buf, 0, count)).getBytes())
+ out.close()
+ }
+ }
+
+ def mapFile(vfs : VFS, base : VFSFile) =
+ if (base == null) null else new File(vfs, base)
+
+ class File(vfs : VFS, base : VFSFile) extends VFSFile {
+ override def getColor() =
+ base.getColor()
+
+ override def getDeletePath() =
+ base.getDeletePath()
+
+ override def getExtendedAttribute(name : String) =
+ base.getExtendedAttribute(name)
+
+ override def getIcon(expanded : Boolean, openBuffer : Boolean) =
+ base.getIcon(expanded, openBuffer)
+
+ override def getLength() =
+ base.getLength()
+
+ override def getName() =
+ base.getName()
+
+ override def getPath() =
+ "isa:" + base.getPath()
+
+ override def getSymlinkPath() =
+ base.getSymlinkPath()
+
+ override def getType() =
+ base.getType()
+
+ override def getVFS() =
+ vfs
+
+ override def isBinary(session : Object) =
+ base.isBinary(session)
+
+ override def isHidden() =
+ base.isHidden()
+
+ override def isReadable() =
+ base.isReadable()
+
+ override def isWriteable() =
+ base.isWriteable()
+
+ override def setDeletePath(path : String) =
+ base.setDeletePath(path)
+
+ override def setHidden(hidden : Boolean) =
+ base.setHidden(hidden)
+
+ override def setLength(length : Long) =
+ base.setLength(length)
+
+ override def setName(name : String) =
+ base.setName(name)
+
+ override def setPath(path : String) =
+ base.setPath(path)
+
+ override def setReadable(readable : Boolean) =
+ base.setReadable(readable)
+
+ override def setWriteable(writeable : Boolean) =
+ base.setWriteable(writeable)
+
+ override def setSymlinkPath(symlinkPath : String) =
+ base.setSymlinkPath(symlinkPath)
+
+ 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("isa", VFSManager.getVFSForProtocol("file").getCapabilities()) {
+ private var baseVFS = VFSManager.getVFSForProtocol("file")
+
+ private def cutPath(path : String) =
+ if (path.startsWith("isa:")) path.substring(4) else path
+
+ override def createVFSSession(path : String, comp : Component) =
+ baseVFS.createVFSSession(cutPath(path), comp)
+
+ override def getCapabilities() =
+ baseVFS.getCapabilities()
+
+ override def getExtendedAttributes() =
+ baseVFS.getExtendedAttributes()
+
+ override def getParentOfPath(path : String) =
+ "isa:" + baseVFS.getParentOfPath(cutPath(path))
+
+ override def constructPath(parent : String, path : String) =
+ "isa:" + baseVFS.constructPath(cutPath(parent), path)
+
+ override def getFileName(path : String) =
+ baseVFS.getFileName(path)
+
+ override def getFileSeparator() =
+ baseVFS.getFileSeparator()
+
+ override def getTwoStageSaveName(path : String) =
+ "isa:" + baseVFS.getTwoStageSaveName(cutPath(path))
+
+ override def _canonPath(session : Object, path : String, comp : Component) =
+ "isa:" + 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 _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) =
+ 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 _listFiles(session : Object, path : String, comp : Component) =
+ (baseVFS._listFiles(session, cutPath(path), comp)
+ .map(file => VFS.mapFile(this, file)))
+
+ 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) =
+ 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 _saveComplete(session : Object, buffer : Buffer, path : String,
+ comp : Component) =
+ baseVFS._saveComplete(session, buffer, cutPath(path), comp)
+}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/proofdocument/ProofDocument.scala Sun Oct 19 16:51:55 2008 +0200
@@ -0,0 +1,236 @@
+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
+ // spurious end of a token but also:
+ // Bug ID: 5050507 Pattern.matches throws StackOverflow Error
+ // http://bugs.sun.com/bugdatabase/view_bug.do?bug_id=5050507
+
+ val tokenPattern =
+ Pattern.compile(
+ "\\{\\*([^*]|\\*[^}]|\\*\\z)*(\\z|\\*\\})|" +
+ "\\(\\*([^*]|\\*[^)]|\\*\\z)*(\\z|\\*\\))|" +
+ "(\\?'?|')[A-Za-z_0-9.]*|" +
+ "[A-Za-z_0-9.]+|" +
+ "[!#$%&*+-/<=>?@^_|~]+|" +
+ "\"([^\\\\\"]?(\\\\(.|\\z))?)*+(\"|\\z)|" +
+ "`([^\\\\`]?(\\\\(.|\\z))?)*+(`|\\z)|" +
+ "[()\\[\\]{}:;]", Pattern.MULTILINE)
+
+}
+
+abstract class ProofDocument[C](text : Text) {
+ import ProofDocument._
+
+ protected var firstToken : Token[C] = null
+ protected var lastToken : Token[C] = null
+ private var active = false
+
+ {
+ text.changes.add(e => textChanged(e.start, e.added, e.removed))
+ }
+
+ def activate() : Unit =
+ if (! active) {
+ active = true
+ textChanged(0, text.length, 0)
+ }
+
+ protected def tokens(start : Token[C], stop : Token[C]) =
+ new Iterator[Token[C]]() {
+ var current = start
+ def hasNext() = current != stop && current != null
+ def next() = { val save = current ; current = current.next ; save }
+ }
+
+ protected def tokens(start : Token[C]) : Iterator[Token[C]] =
+ tokens(start, null)
+
+ protected def tokens() : Iterator[Token[C]] =
+ tokens(firstToken, null)
+
+ private def checkStart(t : Token[C], P : (Int) => Boolean)
+ = t != null && P(t.start)
+
+ private def checkStop(t : Token[C], P : (Int) => Boolean)
+ = t != null && P(t.stop)
+
+ private def scan(s : Token[C], f : (Token[C]) => Boolean) : Token[C] = {
+ var current = s
+ while (current != null) {
+ val next = current.next
+ if (next == null || f(next))
+ return current
+ current = next
+ }
+ return null
+ }
+
+ private def textChanged(start : Int, addedLen : Int, removedLen : Int) {
+ if (active == false)
+ return
+
+ var beforeChange =
+ if (checkStop(firstToken, _ < start)) scan(firstToken, _.stop >= start)
+ else null
+
+ var firstRemoved =
+ if (beforeChange != null) beforeChange.next
+ else if (checkStart(firstToken, _ <= start + removedLen)) firstToken
+ else null
+
+ var lastRemoved = scan(firstRemoved, _.start > start + removedLen)
+
+ var shiftToken =
+ if (lastRemoved != null) lastRemoved
+ else if (checkStart(firstToken, _ > start)) firstToken
+ else null
+
+ while(shiftToken != null) {
+ shiftToken.shift(addedLen - removedLen, start)
+ shiftToken = shiftToken.next
+ }
+
+ // scan changed tokens until the end of the text or a matching token is
+ // found which is beyond the changed area
+ val matchStart = if (beforeChange == null) 0 else beforeChange.stop
+ var firstAdded : Token[C] = null
+ var lastAdded : Token[C] = null
+
+ val matcher = tokenPattern.matcher(text.content(matchStart, text.length))
+ var finished = false
+ var position = 0
+ while(matcher.find(position) && ! finished) {
+ position = matcher.end()
+
+ val newToken = new Token[C](matcher.start() + matchStart,
+ matcher.end() + matchStart,
+ isStartKeyword(matcher.group()),
+ matcher.end() - matcher.start() > 2 &&
+ matcher.group().substring(0, 2) == "(*")
+
+ if (firstAdded == null)
+ firstAdded = newToken
+ else {
+ newToken.previous = lastAdded
+ lastAdded.next = newToken
+ }
+ lastAdded = newToken
+
+ while(checkStop(lastRemoved, _ < newToken.stop) &&
+ lastRemoved.next != null)
+ lastRemoved = lastRemoved.next
+
+ if (newToken.stop >= start + addedLen &&
+ checkStop(lastRemoved, _ == newToken.stop) )
+ finished = true
+ }
+
+ var afterChange = if (lastRemoved != null) lastRemoved.next else null
+
+ // remove superflous first token-change
+ if (firstAdded != null && firstAdded == firstRemoved &&
+ firstAdded.stop < start) {
+ beforeChange = firstRemoved
+ if (lastRemoved == firstRemoved) {
+ lastRemoved = null
+ firstRemoved = null
+ }
+ else {
+ firstRemoved = firstRemoved.next
+ if (firstRemoved == null)
+ System.err.println("ERROR")
+ assert(firstRemoved != null)
+ }
+
+ if (lastAdded == firstAdded) {
+ lastAdded = null
+ firstAdded = null
+ }
+ if (firstAdded != null)
+ firstAdded = firstAdded.next
+ }
+
+ // remove superflous last token-change
+ if (lastAdded != null && lastAdded == lastRemoved &&
+ lastAdded.start > start + addedLen) {
+ afterChange = lastRemoved
+ if (firstRemoved == lastRemoved) {
+ firstRemoved = null
+ lastRemoved = null
+ }
+ else {
+ lastRemoved = lastRemoved.previous
+ if (lastRemoved == null)
+ System.err.println("ERROR")
+ assert(lastRemoved != null)
+ }
+
+ if (lastAdded == firstAdded) {
+ lastAdded = null
+ firstAdded = null
+ }
+ else
+ lastAdded = lastAdded.previous
+ }
+
+ if (firstRemoved == null && firstAdded == null)
+ return
+
+ if (firstToken == null) {
+ firstToken = firstAdded
+ lastToken = lastAdded
+ }
+ else {
+ // cut removed tokens out of list
+ if (firstRemoved != null)
+ firstRemoved.previous = null
+ if (lastRemoved != null)
+ lastRemoved.next = null
+
+ if (firstToken == firstRemoved)
+ if (firstAdded != null)
+ firstToken = firstAdded
+ else
+ firstToken = afterChange
+
+ if (lastToken == lastRemoved)
+ if (lastAdded != null)
+ lastToken = lastAdded
+ else
+ lastToken = beforeChange
+
+ // insert new tokens into list
+ if (firstAdded != null) {
+ firstAdded.previous = beforeChange
+ if (beforeChange != null)
+ beforeChange.next = firstAdded
+ else
+ firstToken = firstAdded
+ }
+ else if (beforeChange != null)
+ beforeChange.next = afterChange
+
+ if (lastAdded != null) {
+ lastAdded.next = afterChange
+ if (afterChange != null)
+ afterChange.previous = lastAdded
+ else
+ lastToken = lastAdded
+ }
+ else if (afterChange != null)
+ afterChange.previous = beforeChange
+ }
+
+ tokenChanged(beforeChange, afterChange, firstRemoved)
+ }
+
+ protected def isStartKeyword(str : String) : Boolean;
+
+ protected def tokenChanged(start : Token[C], stop : Token[C],
+ removed : Token[C])
+}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/proofdocument/Text.scala Sun Oct 19 16:51:55 2008 +0200
@@ -0,0 +1,14 @@
+package isabelle.proofdocument
+
+import isabelle.utils.EventSource
+
+object Text {
+ 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]
+}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/proofdocument/Token.scala Sun Oct 19 16:51:55 2008 +0200
@@ -0,0 +1,31 @@
+package isabelle.proofdocument
+
+class Token[C](var start : Int, var stop : Int, val isCommandStart : Boolean,
+ val isComment : Boolean) {
+ var next : Token[C] = null
+ var previous : Token[C] = null
+ var command : C = null.asInstanceOf[C]
+
+ def length = stop - start
+
+ def shift(offset : Int, bottomClamp : Int) {
+ start = bottomClamp max (start + offset)
+ stop = bottomClamp max (stop + offset)
+ }
+
+ override def hashCode() : Int = (31 + start) * 31 + stop
+
+ override def equals(obj : Any) : Boolean = {
+ if (super.equals(obj))
+ return true;
+
+ if (null == obj)
+ return false;
+
+ obj match {
+ case other: Token[_] =>
+ (start == other.start) && (stop == other.stop)
+ case other: Any => false
+ }
+ }
+}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/proofdocument/tests/TestProofDocument.scala Sun Oct 19 16:51:55 2008 +0200
@@ -0,0 +1,139 @@
+package isabelle.proofdocument.tests
+
+import org.testng.annotations._
+import org.testng.Assert._
+
+import isabelle.proofdocument._
+import isabelle.utils.EventSource
+
+class TextMockup() extends Text {
+ var content = ""
+ val changes = new EventSource[Text.Changed]
+
+ def content(start : Int, stop : Int) = content.substring(start, stop)
+ def length = content.length
+
+ def change(start : Int, added : String, removed : Int) {
+ content = content.substring(0, start) + added + content.substring(start + removed)
+ changes.fire(new Text.Changed(start, added.length, removed))
+ }
+}
+
+class ProofDocumentTest(text : Text) extends ProofDocument[String](text) {
+ var start : Token[String] = null
+ var stop : Token[String] = null
+ var removed : Token[String] = null
+
+ def isStartKeyword(s : String) : Boolean = false
+
+ def tokenChanged(start_ : Token[String], stop_ : Token[String],
+ removed_ : Token[String]) {
+ start = start_
+ stop = stop_
+ removed = removed_
+ }
+
+ override def tokens = super.tokens
+ override def tokens(s : Token[String]) = super.tokens(s)
+ override def tokens(s : Token[String], e : Token[String]) = super.tokens(s, e)
+
+ def first = firstToken
+ def last = lastToken
+
+ def checkLinks(first : Token[String], last : Token[String]) {
+ var iter = first
+ var prev : Token[String] = null
+
+ while(iter != null) {
+ assert(iter.previous == prev)
+ prev = iter
+ iter = iter.next
+ }
+ if (last != null)
+ assert(prev == last)
+ }
+}
+
+class TestProofDocument {
+ private def ranges(ts : Iterator[Token[String]]) =
+ (for (t <- ts) yield (t.start, t.stop)).toList
+
+ @Test
+ def testParsing() {
+ def check(tokens : String*) = {
+ var content = ""
+ var structure = Nil : List[(Int, Int)]
+
+ for(tok <- tokens) {
+ if (tok != " ")
+ structure = (content.length, content.length + tok.length) :: structure
+ content = content + tok
+ }
+
+ val text = new TextMockup()
+ val document = new ProofDocumentTest(text)
+ text.change(0, content, 0)
+ document.checkLinks(document.first, document.last)
+ assertEquals(ranges(document.tokens), structure.reverse)
+ }
+
+ check("lemma", " " , "fixes", " ", "A", " ", ":", ":", " ", "'a", " ",
+ "shows", "\"True\"", " ", "using", "`A = A`", "by", "(", "auto", " ",
+ "simp", " ", "add", ":", "refl", ")")
+ }
+
+ @Test
+ def testChanging() {
+ val text = new TextMockup()
+ val document = new ProofDocumentTest(text)
+
+ def compare(start : Int, add : String, remove : Int) {
+ val oldDocument = ranges(document.tokens)
+ text.change(start, add, remove)
+ document.checkLinks(document.first, document.last)
+ document.checkLinks(document.removed, null)
+
+ val offset = remove - add.length
+ val before = if (document.start == null) Nil
+ else ranges(document.tokens(document.first, document.start.next))
+ val after = (for(t <- document.tokens(document.stop))
+ yield (t.start + offset, t.stop + offset)).toList
+ val removed = ranges(document.tokens(document.removed))
+ assertEquals((before ++ removed ++ after).length, oldDocument.length,
+ "Mismatch on token count")
+ assertEquals(before, oldDocument.take(before.length),
+ "Tokens before changed part")
+ assertEquals(after, oldDocument.drop(before.length + removed.length),
+ "Tokens before changed part")
+
+ val newText = new TextMockup()
+ val newDocument = new ProofDocumentTest(newText)
+ newText.change(0, text.content, 0)
+ newDocument.checkLinks(newDocument.first, newDocument.last)
+
+ assertEquals(ranges(document.tokens), ranges(newDocument.tokens),
+ "Mismatch on entirely reparsed document")
+ }
+
+ val s = """lemma fixes a :: nat assumes T: \"A\" shows \"B ==> A\" using `A` by auto"""
+ compare(0, s, text.content.length)
+ compare(0, "(*", 0)
+ compare(text.content.length, "*)", 0)
+ compare(0, "", 2)
+ compare(1, "", 7)
+
+ compare(0, "test :: 12 34", text.content.length)
+ compare(6, "", 1)
+ compare(6, ":", 0)
+ compare(8, "56", 2)
+ compare(2, "", 4)
+
+ compare(0, "test :: 12 34", text.content.length)
+ compare(5, "test 1 2", 0)
+ compare(4, " test 2 3", 0)
+
+ compare(0, "theory Scratch\nimports Main\nbegin\n\nlemma test_x: fixes X :: nat shows \"∃ X. X > 0\" by auto\n\nend", text.content.length)
+ compare(72, "", 11)
+ compare(71, "", 1)
+ }
+}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/prover/Command.scala Sun Oct 19 16:51:55 2008 +0200
@@ -0,0 +1,65 @@
+package isabelle.prover
+
+import isabelle.proofdocument.Token
+import isabelle.{ YXML, XML }
+
+object Command {
+ object Phase 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 first : Token[Command], val last : Token[Command]) {
+ import Command._
+
+ {
+ var t = first
+ while(t != null) {
+ t.command = this
+ t = if (t == last) null else t.next
+ }
+ }
+
+ val id : Long = generateId
+ var phase = Phase.UNPROCESSED
+
+ var results = Nil : List[XML.Tree]
+
+ def idString = java.lang.Long.toString(id, 36)
+ def document = 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)
+ }
+
+ 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 = {
+ var i = last
+ while (i != first && i.isComment)
+ i = i.previous
+ i.stop
+ }
+}
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/prover/CommandChangeInfo.scala Sun Oct 19 16:51:55 2008 +0200
@@ -0,0 +1,3 @@
+package isabelle.prover
+
+class CommandChangeInfo(val command : Command)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/prover/Document.scala Sun Oct 19 16:51:55 2008 +0200
@@ -0,0 +1,152 @@
+package isabelle.prover
+
+import isabelle.proofdocument.{ ProofDocument, Token, Text }
+
+import isabelle.utils.EventSource
+
+object Document {
+ class StructureChange(val beforeChange : Command,
+ val addedCommands : List[Command],
+ val removedCommands : List[Command])
+}
+
+class Document(text : Text, prover : Prover) extends ProofDocument[Command](text)
+{
+ val structuralChanges = new EventSource[Document.StructureChange]()
+
+ def isStartKeyword(s : String) = prover.commandKeywords.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 =>
+ System.err.println("NPE!")
+ throw error
+ }
+ }
+ }
+
+ def getContent(cmd : Command) = text.content(cmd.properStart, cmd.properStop)
+
+ 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],
+ 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
+ if (t.command != last)
+ removedCommands = t.command :: removedCommands
+ last = t.command
+ }
+
+ var before : Command = null
+ if (! removedCommands.isEmpty) {
+ if (first.first == removed) {
+ if (start == null)
+ before = null
+ else
+ before = start.command
+ }
+ else
+ before = first.previous
+ }
+
+ var addedCommands : List[Command] = Nil
+ var scan : Token[Command] = null
+ if (start != null) {
+ val next = start.next
+ if (first != null && first.first != removed) {
+ scan = first.first
+ if (before == null)
+ before = first.previous
+ }
+ else if (next != null && next != stop) {
+ if (next.isCommandStart) {
+ before = start.command
+ scan = next
+ }
+ else if (first == null || first.first == removed) {
+ first = start.command
+ removedCommands = first :: removedCommands
+ scan = first.first
+ if (before == null)
+ before = first.previous
+ }
+ else {
+ scan = first.first
+ if (before == null)
+ before = first.previous
+ }
+ }
+ }
+ else
+ scan = firstToken
+
+ var stopScan : Token[Command] = null
+ if (stop != null) {
+ if (stop == stop.command.first)
+ stopScan = stop
+ else
+ stopScan = stop.command.last.next
+ }
+ else if (last != null)
+ 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.isCommandStart)
+ finished = true
+ else
+ overrun = true
+ }
+
+ if (scan.isCommandStart && cmdStart != null && !finished) {
+ if (! overrun) {
+ addedCommands = new Command(cmdStart, cmdStop) :: addedCommands
+ cmdStart = scan
+ cmdStop = scan
+ }
+ else
+ finished = true
+ }
+ else if (! finished) {
+ if (cmdStart == null)
+ cmdStart = scan
+ cmdStop = scan
+ }
+ if (overrun && !finished) {
+ if (scan.command != last)
+ removedCommands = scan.command :: removedCommands
+ last = scan.command
+ }
+
+ if (!finished)
+ scan = scan.next
+ }
+
+ if (cmdStart != null)
+ addedCommands = new Command(cmdStart, cmdStop) :: addedCommands
+
+ // relink commands
+ addedCommands = addedCommands.reverse
+ removedCommands = removedCommands.reverse
+
+ structuralChanges.fire(new Document.StructureChange(before, addedCommands,
+ removedCommands))
+ }
+}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/prover/Prover.scala Sun Oct 19 16:51:55 2008 +0200
@@ -0,0 +1,185 @@
+package isabelle.prover
+
+import scala.collection.mutable.{ HashMap, HashSet }
+
+import java.util.Properties
+
+import javax.swing.SwingUtilities
+
+import isabelle.proofdocument.{ ProofDocument, Text }
+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 isabelle.utils.EventSource
+
+import Command.Phase
+
+class Prover() {
+ val converter = new Interpretation()
+
+ private var _logic = "HOL"
+ private var process = null : IsabelleProcess
+ private var commands = new HashMap[String, Command]
+
+ val commandKeywords = new HashSet[String]
+ private var initialized = false
+
+ val activated = new EventSource[Unit]
+ val commandInfo = new EventSource[CommandChangeInfo]
+ val outputInfo = new EventSource[String]
+ var document = null : Document
+
+ var workerThread = 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(())
+ }
+ )
+ }
+ else {
+ val tree = parse_failsafe(converter.decode(r.result))
+ tree match {
+ case Elem("message", _, List(Elem("command_decl", List(("name", name),
+ ("kind", _)), _))) =>
+ commandKeywords.addEntry(name)
+ case _ =>
+ if (st != null)
+ handleResult(st, r, tree)
+ }
+ }
+
+ }
+ }
+ }
+
+ def handleResult(st : Command, r : Result, tree : XML.Tree) {
+ def fireChange() =
+ inUIThread(() => commandInfo.fire(new CommandChangeInfo(st)))
+
+ r.kind match {
+ case IsabelleProcess.Kind.ERROR =>
+ if (st.phase != Phase.REMOVED && st.phase != Phase.REMOVE)
+ st.phase = Phase.FAILED
+ st.addResult(tree)
+ fireChange()
+
+ case IsabelleProcess.Kind.WRITELN =>
+ st.addResult(tree)
+ fireChange()
+
+ case IsabelleProcess.Kind.PRIORITY =>
+ st.addResult(tree)
+ fireChange()
+
+ case IsabelleProcess.Kind.WARNING =>
+ st.addResult(tree)
+ fireChange()
+
+ case IsabelleProcess.Kind.STATUS =>
+ val state = tree match { case Elem("message", _,
+ Elem (name, _, _) :: _) => name
+ case _ => null }
+ if (st.phase != Phase.REMOVED && st.phase != Phase.REMOVE) {
+ state match {
+ case "finished" =>
+ st.phase = Phase.FINISHED
+ fireChange()
+
+ case "unprocessed" =>
+ st.phase = Phase.UNPROCESSED
+ fireChange()
+
+ case "failed" =>
+ st.phase = Phase.FAILED
+ fireChange()
+
+ case "removed" =>
+ commands.removeKey(st.idString)
+ st.phase = Phase.REMOVED
+ fireChange()
+
+ case _ =>
+ }
+ }
+ case _ =>
+ }
+ }
+
+ def logic = _logic
+
+ def start(logic : String) {
+ if (logic != null)
+ _logic = logic
+ process = new IsabelleProcess("-m", "xsymbols", _logic)
+ workerThread.start
+ }
+
+ def stop() {
+ process.kill
+ }
+
+ private def inUIThread(runnable : () => Unit) {
+ SwingUtilities invokeAndWait new Runnable() {
+ override def run() { runnable() }
+ }
+ }
+
+ def setDocument(text : Text, path : String) {
+ this.document = new Document(text, this)
+ process.ML("ThyLoad.add_path " + encode_string(path))
+
+ document.structuralChanges.add(changes => {
+ for (cmd <- changes.removedCommands) remove(cmd)
+ for (cmd <- changes.addedCommands) send(cmd)
+ })
+ if (initialized) {
+ document.activate()
+ activated.fire(())
+ }
+ }
+
+ private def send(cmd : Command) {
+ commands.put(cmd.idString, cmd)
+
+ val props = new Properties()
+ props.setProperty("id", cmd.idString)
+ props.setProperty("offset", "1")
+
+ 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
+ }
+
+ def remove(cmd : Command) {
+ cmd.phase = Phase.REMOVE
+ process.output_sync("Isar.remove " + encode_string(cmd.idString))
+ }
+}
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/utils/EventSource.scala Sun Oct 19 16:51:55 2008 +0200
@@ -0,0 +1,12 @@
+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