# HG changeset patch # User wenzelm # Date 1219597342 -7200 # Node ID c3f7fa72af2ad40d03a09b2ae89d092f619f87b0 # Parent 26e1a7a6695d745adf2a8782bbe4fb333d1812cc rearranged source files; diff -r 26e1a7a6695d -r c3f7fa72af2a lib/jedit/plugin/isabelle/IsabelleDock.scala --- a/lib/jedit/plugin/isabelle/IsabelleDock.scala Sun Aug 24 18:57:43 2008 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,152 +0,0 @@ -/* Title: jedit/plugin/IsabelleDock.scala - ID: $Id$ - Author: Makarius - -Dockable window for Isabelle process control. -*/ - -package isabelle.jedit - -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.is_system) { - 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.Kind.WARNING => warningStyle - case IsabelleProcess.Kind.ERROR => errorStyle - case IsabelleProcess.Kind.TRACING => infoStyle - case _ => if (result.is_raw) rawStyle else null - } - doc.insertString(doc.getLength, IsabellePlugin.result_content(result), style) - if (!result.is_raw) 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 26e1a7a6695d -r c3f7fa72af2a lib/jedit/plugin/isabelle/IsabelleParser.scala --- a/lib/jedit/plugin/isabelle/IsabelleParser.scala Sun Aug 24 18:57:43 2008 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,61 +0,0 @@ -/* Title: jedit/plugin/IsabelleParser.scala - ID: $Id$ - Author: Makarius - -Isabelle parser setup for Sidekick plugin. -*/ - -package isabelle.jedit - -import javax.swing.text.Position -import javax.swing.tree.DefaultMutableTreeNode -import javax.swing.tree.DefaultTreeModel - -import org.gjt.sp.jedit.Buffer -import org.gjt.sp.util.Log - -import sidekick.Asset -import sidekick.SideKickParsedData -import sidekick.SideKickParser -import errorlist.DefaultErrorSource - - -private class IsabelleAsset(name: String, content: String) extends Asset(name) -{ - override def getShortString() = { name } - override def getLongString() = { content } - override def getIcon() = { null } -} - - -class IsabelleParser extends SideKickParser("isabelle") { - private var stopped = false - - override def stop () { stopped = true } - - def parse(buffer: Buffer, e: DefaultErrorSource): SideKickParsedData = { - stopped = false - - var text: String = null - var data: SideKickParsedData = null - - try { - buffer.readLock() - text = buffer.getText(0, buffer.getLength()) - data = new SideKickParsedData(buffer.getName()) - - val asset = new IsabelleAsset("theory", null) - asset.setStart(buffer.createPosition(0)) - asset.setEnd(buffer.createPosition(buffer.getLength())) - - val node = new DefaultMutableTreeNode(asset) - data.root.insert(node, node.getChildCount()) - - } finally { - buffer.readUnlock() - } - - data - } -} - diff -r 26e1a7a6695d -r c3f7fa72af2a lib/jedit/plugin/isabelle/IsabellePlugin.scala --- a/lib/jedit/plugin/isabelle/IsabellePlugin.scala Sun Aug 24 18:57:43 2008 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,148 +0,0 @@ -/* Title: jedit/plugin/IsabellePlugin.scala - ID: $Id$ - Author: Makarius - -Isabelle/jEdit plugin -- main setup. -*/ - -package isabelle.jedit - -import org.gjt.sp.jedit.EditPlugin -import org.gjt.sp.util.Log - -import errorlist.DefaultErrorSource -import errorlist.ErrorSource - -import java.util.Properties -import java.lang.NumberFormatException - -import scala.collection.mutable.ListBuffer -import scala.io.Source - - -/* 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(Markup.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 content - def result_content(result: IsabelleProcess.Result) = - XML.content(isabelle.result_tree(result)).mkString("") - - - // 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.Kind.WARNING || - result.kind == IsabelleProcess.Kind.ERROR)) { - val typ = - if (result.kind == IsabelleProcess.Kind.WARNING) ErrorSource.WARNING - else ErrorSource.ERROR - (Position.line_of(result.props), Position.file_of(result.props)) match { - case (Some(line), Some(file)) => - val content = IsabellePlugin.result_content(result) - if (content.length > 0) { - val lines = Source.fromString(content).getLines - val err = new DefaultErrorSource.DefaultError(IsabellePlugin.errors, - typ, file, line - 1, 0, 0, lines.next) - for (msg <- lines) err.addExtraMessage(msg) - IsabellePlugin.errors.addError(err) - } - case _ => - } - }) - - - // Isabelle process - IsabellePlugin.isabelle = - new IsabelleProcess("-mno_brackets", "-mno_type_brackets", "-mxsymbols") - thread = new Thread (new Runnable { - def run = { - var result: IsabelleProcess.Result = null - do { - try { - result = IsabellePlugin.isabelle.results.take - } - catch { - case _: NullPointerException => result = null - case _: InterruptedException => result = null - } - if (result != null) { - System.err.println(result) // FIXME - IsabellePlugin.consume(result) - } - if (result.kind == IsabelleProcess.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 26e1a7a6695d -r c3f7fa72af2a lib/jedit/plugin/isabelle_dock.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/lib/jedit/plugin/isabelle_dock.scala Sun Aug 24 19:02:22 2008 +0200 @@ -0,0 +1,152 @@ +/* Title: lib/jedit/plugin/isabelle_dock.scala + ID: $Id$ + Author: Makarius + +Dockable window for Isabelle process control. +*/ + +package isabelle.jedit + +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.is_system) { + 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.Kind.WARNING => warningStyle + case IsabelleProcess.Kind.ERROR => errorStyle + case IsabelleProcess.Kind.TRACING => infoStyle + case _ => if (result.is_raw) rawStyle else null + } + doc.insertString(doc.getLength, IsabellePlugin.result_content(result), style) + if (!result.is_raw) 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 26e1a7a6695d -r c3f7fa72af2a lib/jedit/plugin/isabelle_parser.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/lib/jedit/plugin/isabelle_parser.scala Sun Aug 24 19:02:22 2008 +0200 @@ -0,0 +1,61 @@ +/* Title: lib/jedit/plugin/isabelle_parser.scala + ID: $Id$ + Author: Makarius + +Isabelle parser setup for Sidekick plugin. +*/ + +package isabelle.jedit + +import javax.swing.text.Position +import javax.swing.tree.DefaultMutableTreeNode +import javax.swing.tree.DefaultTreeModel + +import org.gjt.sp.jedit.Buffer +import org.gjt.sp.util.Log + +import sidekick.Asset +import sidekick.SideKickParsedData +import sidekick.SideKickParser +import errorlist.DefaultErrorSource + + +private class IsabelleAsset(name: String, content: String) extends Asset(name) +{ + override def getShortString() = { name } + override def getLongString() = { content } + override def getIcon() = { null } +} + + +class IsabelleParser extends SideKickParser("isabelle") { + private var stopped = false + + override def stop () { stopped = true } + + def parse(buffer: Buffer, e: DefaultErrorSource): SideKickParsedData = { + stopped = false + + var text: String = null + var data: SideKickParsedData = null + + try { + buffer.readLock() + text = buffer.getText(0, buffer.getLength()) + data = new SideKickParsedData(buffer.getName()) + + val asset = new IsabelleAsset("theory", null) + asset.setStart(buffer.createPosition(0)) + asset.setEnd(buffer.createPosition(buffer.getLength())) + + val node = new DefaultMutableTreeNode(asset) + data.root.insert(node, node.getChildCount()) + + } finally { + buffer.readUnlock() + } + + data + } +} + diff -r 26e1a7a6695d -r c3f7fa72af2a lib/jedit/plugin/isabelle_plugin.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/lib/jedit/plugin/isabelle_plugin.scala Sun Aug 24 19:02:22 2008 +0200 @@ -0,0 +1,148 @@ +/* Title: lib/jedit/plugin/isabelle_plugin.scala + ID: $Id$ + Author: Makarius + +Isabelle/jEdit plugin -- main setup. +*/ + +package isabelle.jedit + +import org.gjt.sp.jedit.EditPlugin +import org.gjt.sp.util.Log + +import errorlist.DefaultErrorSource +import errorlist.ErrorSource + +import java.util.Properties +import java.lang.NumberFormatException + +import scala.collection.mutable.ListBuffer +import scala.io.Source + + +/* 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(Markup.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 content + def result_content(result: IsabelleProcess.Result) = + XML.content(isabelle.result_tree(result)).mkString("") + + + // 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.Kind.WARNING || + result.kind == IsabelleProcess.Kind.ERROR)) { + val typ = + if (result.kind == IsabelleProcess.Kind.WARNING) ErrorSource.WARNING + else ErrorSource.ERROR + (Position.line_of(result.props), Position.file_of(result.props)) match { + case (Some(line), Some(file)) => + val content = IsabellePlugin.result_content(result) + if (content.length > 0) { + val lines = Source.fromString(content).getLines + val err = new DefaultErrorSource.DefaultError(IsabellePlugin.errors, + typ, file, line - 1, 0, 0, lines.next) + for (msg <- lines) err.addExtraMessage(msg) + IsabellePlugin.errors.addError(err) + } + case _ => + } + }) + + + // Isabelle process + IsabellePlugin.isabelle = + new IsabelleProcess("-mno_brackets", "-mno_type_brackets", "-mxsymbols") + thread = new Thread (new Runnable { + def run = { + var result: IsabelleProcess.Result = null + do { + try { + result = IsabellePlugin.isabelle.results.take + } + catch { + case _: NullPointerException => result = null + case _: InterruptedException => result = null + } + if (result != null) { + System.err.println(result) // FIXME + IsabellePlugin.consume(result) + } + if (result.kind == IsabelleProcess.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 26e1a7a6695d -r c3f7fa72af2a lib/jedit/plugin/mk --- a/lib/jedit/plugin/mk Sun Aug 24 18:57:43 2008 +0200 +++ b/lib/jedit/plugin/mk Sun Aug 24 19:02:22 2008 +0200 @@ -10,9 +10,9 @@ scalac -d build \ -cp $JEDIT_HOME/jedit.jar:$PLUGINS/SideKick.jar:$PLUGINS/ErrorList.jar:$PLUGINS/Console.jar:../../classes/Pure.jar \ - isabelle/IsabellePlugin.scala \ - isabelle/IsabelleDock.scala \ - isabelle/IsabelleParser.scala \ + isabelle_plugin.scala \ + isabelle_dock.scala \ + isabelle_parser.scala \ && ( cp *.xml *.props build/ cd build