# 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(); + + +