# HG changeset patch
# User wenzelm
# Date 1199635045 -3600
# Node ID 606850a6fc1a0a324d9cc1ae579d49c9a65a76a3
# Parent dfca7b555e5c0c06533f1e935da51f13b040c93f
basic setup for Isabelle/jEdit plugin;
diff -r dfca7b555e5c -r 606850a6fc1a lib/jedit/plugin/Isabelle.props
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/lib/jedit/plugin/Isabelle.props Sun Jan 06 16:57:25 2008 +0100
@@ -0,0 +1,25 @@
+## Isabelle plugin properties
+## $Id$
+
+#identification
+plugin.isabelle.IsabellePlugin.name = Isabelle
+plugin.isabelle.IsabellePlugin.author = Makarius
+plugin.isabelle.IsabellePlugin.version = 0.0.1
+plugin.isabelle.IsabellePlugin.description = Basic Isabelle support
+
+#system parameters
+plugin.isabelle.IsabellePlugin.activate = defer
+plugin.isabelle.IsabellePlugin.usePluginHome = false
+
+#dependencies
+plugin.isabelle.IsabellePlugin.depend.0 = jdk 1.5
+plugin.isabelle.IsabellePlugin.depend.1 = jedit 04.03.00.00
+plugin.isabelle.IsabellePlugin.depend.2 = plugin errorlist.ErrorListPlugin 1.7
+plugin.isabelle.IsabellePlugin.depend.3 = plugin sidekick.SideKickPlugin 0.7.4
+plugin.isabelle.IsabellePlugin.depend.4 = plugin console.ConsolePlugin 4.3.4
+
+#dockable component
+isabelle.label = Isabelle
+isabelle.title = Isabelle
+isabelle.longtitle = Basic Isabelle process
+
diff -r dfca7b555e5c -r 606850a6fc1a lib/jedit/plugin/dockables.xml
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/lib/jedit/plugin/dockables.xml Sun Jan 06 16:57:25 2008 +0100
@@ -0,0 +1,10 @@
+
+
+
+
+
+
+ new isabelle.IsabelleDock(view, position);
+
+
+
diff -r dfca7b555e5c -r 606850a6fc1a lib/jedit/plugin/isabelle/IsabelleDock.scala
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/lib/jedit/plugin/isabelle/IsabelleDock.scala Sun Jan 06 16:57:25 2008 +0100
@@ -0,0 +1,152 @@
+/* Title: jedit/plugin/IsabelleDock.scala
+ ID: $Id$
+ Author: Makarius
+
+Dockable window for Isabelle process control.
+*/
+
+package isabelle
+
+import org.gjt.sp.jedit.View
+import org.gjt.sp.jedit.gui.DefaultFocusComponent
+import org.gjt.sp.jedit.gui.DockableWindowManager
+import org.gjt.sp.jedit.gui.RolloverButton
+import org.gjt.sp.jedit.gui.HistoryTextField
+import org.gjt.sp.jedit.GUIUtilities
+
+import java.awt.Color
+import java.awt.Insets
+import java.awt.BorderLayout
+import java.awt.Dimension
+import java.awt.event.ActionListener
+import java.awt.event.ActionEvent
+import javax.swing.BoxLayout
+import javax.swing.JPanel
+import javax.swing.JScrollPane
+import javax.swing.JTextPane
+import javax.swing.text.{StyledDocument, StyleConstants}
+import javax.swing.SwingUtilities
+import javax.swing.Icon
+import javax.swing.Box
+import javax.swing.JTextField
+import javax.swing.JComboBox
+import javax.swing.DefaultComboBoxModel
+
+
+class IsabelleDock(view: View, position: String)
+ extends JPanel(new BorderLayout) with DefaultFocusComponent
+{
+ private val text = new HistoryTextField("isabelle", false, true)
+ private val logicCombo = new JComboBox
+
+ {
+ // output pane
+ val pane = new JTextPane
+ pane.setEditable(false)
+ add(BorderLayout.CENTER, new JScrollPane(pane))
+ if (position == DockableWindowManager.FLOATING)
+ setPreferredSize(new Dimension(1000, 500))
+
+ val doc = pane.getDocument.asInstanceOf[StyledDocument]
+
+ def makeStyle(name: String, bg: Boolean, color: Color) = {
+ val style = doc.addStyle(name, null)
+ if (bg) StyleConstants.setBackground(style, color)
+ else StyleConstants.setForeground(style, color)
+ style
+ }
+ val rawStyle = makeStyle("raw", false, Color.GRAY)
+ val infoStyle = makeStyle("info", true, new Color(160, 255, 160))
+ val warningStyle = makeStyle("warning", true, new Color(255, 255, 160))
+ val errorStyle = makeStyle("error", true, new Color(255, 160, 160))
+
+ IsabellePlugin.addPermanentConsumer (result =>
+ if (result != null && !result.isSystem) {
+ SwingUtilities.invokeLater(new Runnable {
+ def run = {
+ val logic = IsabellePlugin.isabelle.session
+ logicCombo.setModel(new DefaultComboBoxModel(Array(logic).asInstanceOf[Array[AnyRef]]))
+ logicCombo.setPrototypeDisplayValue("AAAA") // FIXME ??
+
+ val doc = pane.getDocument.asInstanceOf[StyledDocument]
+ val style = result.kind match {
+ case IsabelleProcess.Result.Kind.WARNING => warningStyle
+ case IsabelleProcess.Result.Kind.ERROR => errorStyle
+ case IsabelleProcess.Result.Kind.TRACING => infoStyle
+ case _ => if (result.isRaw) rawStyle else null
+ }
+ doc.insertString(doc.getLength, result.result, style)
+ if (!result.isRaw) doc.insertString(doc.getLength, "\n", style)
+ pane.setCaretPosition(doc.getLength)
+ }
+ })
+ })
+
+
+ // control box
+ val box = new Box(BoxLayout.X_AXIS)
+ add(BorderLayout.SOUTH, box)
+
+
+ // logic combo
+ logicCombo.setToolTipText("Isabelle logics")
+ logicCombo.setRequestFocusEnabled(false)
+ logicCombo.setModel(new DefaultComboBoxModel(Array("default").asInstanceOf[Array[AnyRef]]))
+ box.add(logicCombo)
+
+
+ // mode combo
+ val modeIsar = "Isar"
+ val modeML = "ML"
+ val modes = Array(modeIsar, modeML)
+ var mode = modeIsar
+
+ val modeCombo = new JComboBox
+ modeCombo.setToolTipText("Toplevel mode")
+ modeCombo.setRequestFocusEnabled(false)
+ modeCombo.setModel(new DefaultComboBoxModel(modes.asInstanceOf[Array[AnyRef]]))
+ modeCombo.setPrototypeDisplayValue("AAAA")
+ modeCombo.addActionListener(new ActionListener {
+ def actionPerformed(evt: ActionEvent): Unit = {
+ mode = modeCombo.getSelectedItem.asInstanceOf[String]
+ }
+ })
+ box.add(modeCombo)
+
+
+ // input field
+ text.setToolTipText("Command line")
+ text.addActionListener(new ActionListener {
+ def actionPerformed(evt: ActionEvent): Unit = {
+ val command = text.getText
+ if (command.length > 0) {
+ if (mode == modeIsar)
+ IsabellePlugin.isabelle.command(command)
+ else if (mode == modeML)
+ IsabellePlugin.isabelle.ML(command)
+ text.setText("")
+ }
+ }
+ })
+ box.add(text)
+
+
+ // buttons
+ def iconButton(icon: String, tip: String, action: => Unit) = {
+ val button = new RolloverButton(GUIUtilities.loadIcon(icon))
+ button.setToolTipText(tip)
+ button.setMargin(new Insets(0,0,0,0))
+ button.setRequestFocusEnabled(false)
+ button.addActionListener(new ActionListener {
+ def actionPerformed(evt: ActionEvent): Unit = action
+ })
+ box.add(button)
+ }
+
+ iconButton("Cancel.png", "Stop", IsabellePlugin.isabelle.interrupt)
+ iconButton("Clear.png", "Clear", pane.setText(""))
+ }
+
+ def focusOnDefaultComponent: Unit = text.requestFocus
+}
+
diff -r dfca7b555e5c -r 606850a6fc1a lib/jedit/plugin/isabelle/IsabelleParser.scala
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/lib/jedit/plugin/isabelle/IsabelleParser.scala Sun Jan 06 16:57:25 2008 +0100
@@ -0,0 +1,33 @@
+/* Title: jedit/plugin/IsabelleParser.scala
+ ID: $Id$
+ Author: Makarius
+
+Isabelle parser setup for Sidekick plugin.
+*/
+
+package isabelle
+
+import org.gjt.sp.jedit.Buffer
+import org.gjt.sp.util.Log
+
+import sidekick.SideKickParsedData
+import sidekick.SideKickParser
+import errorlist.DefaultErrorSource
+
+
+class IsabelleParser extends SideKickParser("isabelle") {
+ private var text: String = null
+ private var data: SideKickParsedData = null
+ private var buffer: Buffer = null
+
+ // FIXME dummy -- no functionality yet
+ def parse(buf: Buffer, e: DefaultErrorSource): SideKickParsedData = {
+ buffer = buf
+ buffer.readLock()
+ text = buffer.getText(0, buffer.getLength())
+ data = new SideKickParsedData(buffer.getName())
+ buffer.readUnlock()
+ data
+ }
+}
+
diff -r dfca7b555e5c -r 606850a6fc1a lib/jedit/plugin/isabelle/IsabellePlugin.scala
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/lib/jedit/plugin/isabelle/IsabellePlugin.scala Sun Jan 06 16:57:25 2008 +0100
@@ -0,0 +1,139 @@
+/* Title: jedit/plugin/IsabellePlugin.scala
+ ID: $Id$
+ Author: Makarius
+
+Isabelle/jEdit plugin -- main setup.
+*/
+
+package isabelle
+
+import isabelle.IsabelleProcess
+
+import org.gjt.sp.jedit.EditPlugin
+import org.gjt.sp.util.Log
+
+import errorlist.DefaultErrorSource
+import errorlist.ErrorSource
+
+import scala.collection.mutable.ListBuffer
+import java.util.Properties
+import java.lang.NumberFormatException
+
+
+/* Global state */
+
+object IsabellePlugin {
+ // unique ids
+ @volatile
+ private var idCount = 0
+
+ def id() : String = synchronized { idCount += 1; "jedit:" + idCount }
+
+ def idProperties(value: String) : Properties = {
+ val props = new Properties
+ props.setProperty("id", value)
+ props
+ }
+
+ def idProperties() : Properties = { idProperties(id()) }
+
+
+ // the error source
+ @volatile
+ var errors: DefaultErrorSource = null
+
+ // the Isabelle process
+ @volatile
+ var isabelle: IsabelleProcess = null
+
+
+ // result consumers
+ type consumer = IsabelleProcess.Result => Boolean
+ private var consumers = new ListBuffer[consumer]
+
+ def addConsumer(consumer: consumer) = synchronized { consumers += consumer }
+
+ def addPermanentConsumer(consumer: IsabelleProcess.Result => Unit) = {
+ addConsumer(result => { consumer(result); false })
+ }
+
+ def delConsumer(consumer: consumer) = synchronized { consumers -= consumer }
+
+ def consume(result: IsabelleProcess.Result) : Unit = {
+ synchronized { consumers.elements.toList } foreach (consumer =>
+ {
+ val finished =
+ try { consumer(result) }
+ catch { case e: Throwable => Log.log(Log.ERROR, this, e); true }
+ if (finished || result == null)
+ delConsumer(consumer)
+ })
+ }
+}
+
+
+/* Main plugin setup */
+
+class IsabellePlugin extends EditPlugin {
+ private var thread: Thread = null
+
+ override def start = {
+ // error source
+ IsabellePlugin.errors = new DefaultErrorSource("isabelle")
+ ErrorSource.registerErrorSource(IsabellePlugin.errors)
+
+ IsabellePlugin.addPermanentConsumer (result =>
+ if (result != null && result.props != null &&
+ (result.kind == IsabelleProcess.Result.Kind.WARNING ||
+ result.kind == IsabelleProcess.Result.Kind.ERROR)) {
+ val typ =
+ if (result.kind == IsabelleProcess.Result.Kind.WARNING) ErrorSource.WARNING
+ else ErrorSource.ERROR
+ val line = result.props.getProperty(IsabelleProcess.Property.LINE)
+ val file = result.props.getProperty(IsabelleProcess.Property.FILE)
+ if (line != null && file != null && result.result.length > 0) {
+ val msg = result.result.split("\n")
+ val err = new DefaultErrorSource.DefaultError(IsabellePlugin.errors,
+ typ, file, Integer.parseInt(line) - 1, 0, 0, msg(0))
+ for (i <- 1 to msg.length - 1)
+ err.addExtraMessage(msg(i))
+ IsabellePlugin.errors.addError(err)
+ }
+ })
+
+ // Isabelle process
+ IsabellePlugin.isabelle = new IsabelleProcess(Array("-m", "builtin_browser"), null)
+ thread = new Thread (new Runnable {
+ def run = {
+ var result: IsabelleProcess.Result = null
+ do {
+ try {
+ result = IsabellePlugin.isabelle.results.take.asInstanceOf[IsabelleProcess.Result]
+ } catch {
+ case _: NullPointerException => null
+ case _: InterruptedException => null
+ }
+ if (result != null) {
+ System.err.println(result) // FIXME
+ IsabellePlugin.consume(result)
+ }
+ if (result.kind == IsabelleProcess.Result.Kind.EXIT) {
+ result = null
+ IsabellePlugin.consume(null)
+ }
+ } while (result != null)
+ }
+ })
+ thread.start
+ }
+
+ override def stop = {
+ IsabellePlugin.isabelle.kill
+ thread.interrupt; thread.join; thread = null
+ IsabellePlugin.isabelle = null
+
+ ErrorSource.unregisterErrorSource(IsabellePlugin.errors)
+ IsabellePlugin.errors = null
+ }
+}
+
diff -r dfca7b555e5c -r 606850a6fc1a lib/jedit/plugin/mk
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/lib/jedit/plugin/mk Sun Jan 06 16:57:25 2008 +0100
@@ -0,0 +1,23 @@
+#!/bin/bash
+# $Id$
+
+set -x
+
+JEDIT_HOME="$HOME/lib/jedit/current"
+PLUGINS="$HOME/.jedit/jars"
+
+
+rm -rf build/ && mkdir -p build
+( cd build; jar xf ../../../classes/isabelle.jar )
+
+scalac -d build \
+ -cp $JEDIT_HOME/jedit.jar:$PLUGINS/SideKick.jar:$PLUGINS/ErrorList.jar:$PLUGINS/Console.jar \
+ isabelle/IsabellePlugin.scala \
+ isabelle/IsabelleDock.scala \
+ isabelle/IsabelleParser.scala \
+&& {
+ cp *.xml *.props build/
+ cd build
+ jar cf ../../isabelle.jar isabelle/*.class *.xml *.props
+}
+
diff -r dfca7b555e5c -r 606850a6fc1a lib/jedit/plugin/services.xml
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/lib/jedit/plugin/services.xml Sun Jan 06 16:57:25 2008 +0100
@@ -0,0 +1,10 @@
+
+
+
+
+
+
+ new isabelle.IsabelleParser();
+
+
+