1.1 --- a/lib/jedit/plugin/isabelle/IsabelleDock.scala Sun Aug 24 18:57:43 2008 +0200
1.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
1.3 @@ -1,152 +0,0 @@
1.4 -/* Title: jedit/plugin/IsabelleDock.scala
1.5 - ID: $Id$
1.6 - Author: Makarius
1.7 -
1.8 -Dockable window for Isabelle process control.
1.9 -*/
1.10 -
1.11 -package isabelle.jedit
1.12 -
1.13 -import org.gjt.sp.jedit.View
1.14 -import org.gjt.sp.jedit.gui.DefaultFocusComponent
1.15 -import org.gjt.sp.jedit.gui.DockableWindowManager
1.16 -import org.gjt.sp.jedit.gui.RolloverButton
1.17 -import org.gjt.sp.jedit.gui.HistoryTextField
1.18 -import org.gjt.sp.jedit.GUIUtilities
1.19 -
1.20 -import java.awt.Color
1.21 -import java.awt.Insets
1.22 -import java.awt.BorderLayout
1.23 -import java.awt.Dimension
1.24 -import java.awt.event.ActionListener
1.25 -import java.awt.event.ActionEvent
1.26 -import javax.swing.BoxLayout
1.27 -import javax.swing.JPanel
1.28 -import javax.swing.JScrollPane
1.29 -import javax.swing.JTextPane
1.30 -import javax.swing.text.{StyledDocument, StyleConstants}
1.31 -import javax.swing.SwingUtilities
1.32 -import javax.swing.Icon
1.33 -import javax.swing.Box
1.34 -import javax.swing.JTextField
1.35 -import javax.swing.JComboBox
1.36 -import javax.swing.DefaultComboBoxModel
1.37 -
1.38 -
1.39 -class IsabelleDock(view: View, position: String)
1.40 - extends JPanel(new BorderLayout) with DefaultFocusComponent
1.41 -{
1.42 - private val text = new HistoryTextField("isabelle", false, true)
1.43 - private val logicCombo = new JComboBox
1.44 -
1.45 - {
1.46 - // output pane
1.47 - val pane = new JTextPane
1.48 - pane.setEditable(false)
1.49 - add(BorderLayout.CENTER, new JScrollPane(pane))
1.50 - if (position == DockableWindowManager.FLOATING)
1.51 - setPreferredSize(new Dimension(1000, 500))
1.52 -
1.53 - val doc = pane.getDocument.asInstanceOf[StyledDocument]
1.54 -
1.55 - def makeStyle(name: String, bg: Boolean, color: Color) = {
1.56 - val style = doc.addStyle(name, null)
1.57 - if (bg) StyleConstants.setBackground(style, color)
1.58 - else StyleConstants.setForeground(style, color)
1.59 - style
1.60 - }
1.61 - val rawStyle = makeStyle("raw", false, Color.GRAY)
1.62 - val infoStyle = makeStyle("info", true, new Color(160, 255, 160))
1.63 - val warningStyle = makeStyle("warning", true, new Color(255, 255, 160))
1.64 - val errorStyle = makeStyle("error", true, new Color(255, 160, 160))
1.65 -
1.66 - IsabellePlugin.addPermanentConsumer (result =>
1.67 - if (result != null && !result.is_system) {
1.68 - SwingUtilities.invokeLater(new Runnable {
1.69 - def run = {
1.70 - val logic = IsabellePlugin.isabelle.session
1.71 - logicCombo.setModel(new DefaultComboBoxModel(Array(logic).asInstanceOf[Array[AnyRef]]))
1.72 - logicCombo.setPrototypeDisplayValue("AAAA") // FIXME ??
1.73 -
1.74 - val doc = pane.getDocument.asInstanceOf[StyledDocument]
1.75 - val style = result.kind match {
1.76 - case IsabelleProcess.Kind.WARNING => warningStyle
1.77 - case IsabelleProcess.Kind.ERROR => errorStyle
1.78 - case IsabelleProcess.Kind.TRACING => infoStyle
1.79 - case _ => if (result.is_raw) rawStyle else null
1.80 - }
1.81 - doc.insertString(doc.getLength, IsabellePlugin.result_content(result), style)
1.82 - if (!result.is_raw) doc.insertString(doc.getLength, "\n", style)
1.83 - pane.setCaretPosition(doc.getLength)
1.84 - }
1.85 - })
1.86 - })
1.87 -
1.88 -
1.89 - // control box
1.90 - val box = new Box(BoxLayout.X_AXIS)
1.91 - add(BorderLayout.SOUTH, box)
1.92 -
1.93 -
1.94 - // logic combo
1.95 - logicCombo.setToolTipText("Isabelle logics")
1.96 - logicCombo.setRequestFocusEnabled(false)
1.97 - logicCombo.setModel(new DefaultComboBoxModel(Array("default").asInstanceOf[Array[AnyRef]]))
1.98 - box.add(logicCombo)
1.99 -
1.100 -
1.101 - // mode combo
1.102 - val modeIsar = "Isar"
1.103 - val modeML = "ML"
1.104 - val modes = Array(modeIsar, modeML)
1.105 - var mode = modeIsar
1.106 -
1.107 - val modeCombo = new JComboBox
1.108 - modeCombo.setToolTipText("Toplevel mode")
1.109 - modeCombo.setRequestFocusEnabled(false)
1.110 - modeCombo.setModel(new DefaultComboBoxModel(modes.asInstanceOf[Array[AnyRef]]))
1.111 - modeCombo.setPrototypeDisplayValue("AAAA")
1.112 - modeCombo.addActionListener(new ActionListener {
1.113 - def actionPerformed(evt: ActionEvent): Unit = {
1.114 - mode = modeCombo.getSelectedItem.asInstanceOf[String]
1.115 - }
1.116 - })
1.117 - box.add(modeCombo)
1.118 -
1.119 -
1.120 - // input field
1.121 - text.setToolTipText("Command line")
1.122 - text.addActionListener(new ActionListener {
1.123 - def actionPerformed(evt: ActionEvent): Unit = {
1.124 - val command = text.getText
1.125 - if (command.length > 0) {
1.126 - if (mode == modeIsar)
1.127 - IsabellePlugin.isabelle.command(command)
1.128 - else if (mode == modeML)
1.129 - IsabellePlugin.isabelle.ML(command)
1.130 - text.setText("")
1.131 - }
1.132 - }
1.133 - })
1.134 - box.add(text)
1.135 -
1.136 -
1.137 - // buttons
1.138 - def iconButton(icon: String, tip: String, action: => Unit) = {
1.139 - val button = new RolloverButton(GUIUtilities.loadIcon(icon))
1.140 - button.setToolTipText(tip)
1.141 - button.setMargin(new Insets(0,0,0,0))
1.142 - button.setRequestFocusEnabled(false)
1.143 - button.addActionListener(new ActionListener {
1.144 - def actionPerformed(evt: ActionEvent): Unit = action
1.145 - })
1.146 - box.add(button)
1.147 - }
1.148 -
1.149 - iconButton("Cancel.png", "Stop", IsabellePlugin.isabelle.interrupt)
1.150 - iconButton("Clear.png", "Clear", pane.setText(""))
1.151 - }
1.152 -
1.153 - def focusOnDefaultComponent: Unit = text.requestFocus
1.154 -}
1.155 -
2.1 --- a/lib/jedit/plugin/isabelle/IsabelleParser.scala Sun Aug 24 18:57:43 2008 +0200
2.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
2.3 @@ -1,61 +0,0 @@
2.4 -/* Title: jedit/plugin/IsabelleParser.scala
2.5 - ID: $Id$
2.6 - Author: Makarius
2.7 -
2.8 -Isabelle parser setup for Sidekick plugin.
2.9 -*/
2.10 -
2.11 -package isabelle.jedit
2.12 -
2.13 -import javax.swing.text.Position
2.14 -import javax.swing.tree.DefaultMutableTreeNode
2.15 -import javax.swing.tree.DefaultTreeModel
2.16 -
2.17 -import org.gjt.sp.jedit.Buffer
2.18 -import org.gjt.sp.util.Log
2.19 -
2.20 -import sidekick.Asset
2.21 -import sidekick.SideKickParsedData
2.22 -import sidekick.SideKickParser
2.23 -import errorlist.DefaultErrorSource
2.24 -
2.25 -
2.26 -private class IsabelleAsset(name: String, content: String) extends Asset(name)
2.27 -{
2.28 - override def getShortString() = { name }
2.29 - override def getLongString() = { content }
2.30 - override def getIcon() = { null }
2.31 -}
2.32 -
2.33 -
2.34 -class IsabelleParser extends SideKickParser("isabelle") {
2.35 - private var stopped = false
2.36 -
2.37 - override def stop () { stopped = true }
2.38 -
2.39 - def parse(buffer: Buffer, e: DefaultErrorSource): SideKickParsedData = {
2.40 - stopped = false
2.41 -
2.42 - var text: String = null
2.43 - var data: SideKickParsedData = null
2.44 -
2.45 - try {
2.46 - buffer.readLock()
2.47 - text = buffer.getText(0, buffer.getLength())
2.48 - data = new SideKickParsedData(buffer.getName())
2.49 -
2.50 - val asset = new IsabelleAsset("theory", null)
2.51 - asset.setStart(buffer.createPosition(0))
2.52 - asset.setEnd(buffer.createPosition(buffer.getLength()))
2.53 -
2.54 - val node = new DefaultMutableTreeNode(asset)
2.55 - data.root.insert(node, node.getChildCount())
2.56 -
2.57 - } finally {
2.58 - buffer.readUnlock()
2.59 - }
2.60 -
2.61 - data
2.62 - }
2.63 -}
2.64 -
3.1 --- a/lib/jedit/plugin/isabelle/IsabellePlugin.scala Sun Aug 24 18:57:43 2008 +0200
3.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
3.3 @@ -1,148 +0,0 @@
3.4 -/* Title: jedit/plugin/IsabellePlugin.scala
3.5 - ID: $Id$
3.6 - Author: Makarius
3.7 -
3.8 -Isabelle/jEdit plugin -- main setup.
3.9 -*/
3.10 -
3.11 -package isabelle.jedit
3.12 -
3.13 -import org.gjt.sp.jedit.EditPlugin
3.14 -import org.gjt.sp.util.Log
3.15 -
3.16 -import errorlist.DefaultErrorSource
3.17 -import errorlist.ErrorSource
3.18 -
3.19 -import java.util.Properties
3.20 -import java.lang.NumberFormatException
3.21 -
3.22 -import scala.collection.mutable.ListBuffer
3.23 -import scala.io.Source
3.24 -
3.25 -
3.26 -/* Global state */
3.27 -
3.28 -object IsabellePlugin {
3.29 - // unique ids
3.30 - @volatile
3.31 - private var idCount = 0
3.32 -
3.33 - def id() : String = synchronized { idCount += 1; "jedit:" + idCount }
3.34 -
3.35 - def idProperties(value: String) : Properties = {
3.36 - val props = new Properties
3.37 - props.setProperty(Markup.ID, value)
3.38 - props
3.39 - }
3.40 -
3.41 - def idProperties() : Properties = { idProperties(id()) }
3.42 -
3.43 -
3.44 - // the error source
3.45 - @volatile
3.46 - var errors: DefaultErrorSource = null
3.47 -
3.48 - // the Isabelle process
3.49 - @volatile
3.50 - var isabelle: IsabelleProcess = null
3.51 -
3.52 -
3.53 - // result content
3.54 - def result_content(result: IsabelleProcess.Result) =
3.55 - XML.content(isabelle.result_tree(result)).mkString("")
3.56 -
3.57 -
3.58 - // result consumers
3.59 - type consumer = IsabelleProcess.Result => Boolean
3.60 - private var consumers = new ListBuffer[consumer]
3.61 -
3.62 - def addConsumer(consumer: consumer) = synchronized { consumers += consumer }
3.63 -
3.64 - def addPermanentConsumer(consumer: IsabelleProcess.Result => Unit) = {
3.65 - addConsumer(result => { consumer(result); false })
3.66 - }
3.67 -
3.68 - def delConsumer(consumer: consumer) = synchronized { consumers -= consumer }
3.69 -
3.70 - def consume(result: IsabelleProcess.Result) : Unit = {
3.71 - synchronized { consumers.elements.toList } foreach (consumer =>
3.72 - {
3.73 - val finished =
3.74 - try { consumer(result) }
3.75 - catch { case e: Throwable => Log.log(Log.ERROR, this, e); true }
3.76 - if (finished || result == null)
3.77 - delConsumer(consumer)
3.78 - })
3.79 - }
3.80 -}
3.81 -
3.82 -
3.83 -/* Main plugin setup */
3.84 -
3.85 -class IsabellePlugin extends EditPlugin {
3.86 - private var thread: Thread = null
3.87 -
3.88 - override def start = {
3.89 - // error source
3.90 - IsabellePlugin.errors = new DefaultErrorSource("isabelle")
3.91 - ErrorSource.registerErrorSource(IsabellePlugin.errors)
3.92 -
3.93 - IsabellePlugin.addPermanentConsumer (result =>
3.94 - if (result != null && result.props != null &&
3.95 - (result.kind == IsabelleProcess.Kind.WARNING ||
3.96 - result.kind == IsabelleProcess.Kind.ERROR)) {
3.97 - val typ =
3.98 - if (result.kind == IsabelleProcess.Kind.WARNING) ErrorSource.WARNING
3.99 - else ErrorSource.ERROR
3.100 - (Position.line_of(result.props), Position.file_of(result.props)) match {
3.101 - case (Some(line), Some(file)) =>
3.102 - val content = IsabellePlugin.result_content(result)
3.103 - if (content.length > 0) {
3.104 - val lines = Source.fromString(content).getLines
3.105 - val err = new DefaultErrorSource.DefaultError(IsabellePlugin.errors,
3.106 - typ, file, line - 1, 0, 0, lines.next)
3.107 - for (msg <- lines) err.addExtraMessage(msg)
3.108 - IsabellePlugin.errors.addError(err)
3.109 - }
3.110 - case _ =>
3.111 - }
3.112 - })
3.113 -
3.114 -
3.115 - // Isabelle process
3.116 - IsabellePlugin.isabelle =
3.117 - new IsabelleProcess("-mno_brackets", "-mno_type_brackets", "-mxsymbols")
3.118 - thread = new Thread (new Runnable {
3.119 - def run = {
3.120 - var result: IsabelleProcess.Result = null
3.121 - do {
3.122 - try {
3.123 - result = IsabellePlugin.isabelle.results.take
3.124 - }
3.125 - catch {
3.126 - case _: NullPointerException => result = null
3.127 - case _: InterruptedException => result = null
3.128 - }
3.129 - if (result != null) {
3.130 - System.err.println(result) // FIXME
3.131 - IsabellePlugin.consume(result)
3.132 - }
3.133 - if (result.kind == IsabelleProcess.Kind.EXIT) {
3.134 - result = null
3.135 - IsabellePlugin.consume(null)
3.136 - }
3.137 - } while (result != null)
3.138 - }
3.139 - })
3.140 - thread.start
3.141 - }
3.142 -
3.143 - override def stop = {
3.144 - IsabellePlugin.isabelle.kill
3.145 - thread.interrupt; thread.join; thread = null
3.146 - IsabellePlugin.isabelle = null
3.147 -
3.148 - ErrorSource.unregisterErrorSource(IsabellePlugin.errors)
3.149 - IsabellePlugin.errors = null
3.150 - }
3.151 -}
4.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
4.2 +++ b/lib/jedit/plugin/isabelle_dock.scala Sun Aug 24 19:02:22 2008 +0200
4.3 @@ -0,0 +1,152 @@
4.4 +/* Title: lib/jedit/plugin/isabelle_dock.scala
4.5 + ID: $Id$
4.6 + Author: Makarius
4.7 +
4.8 +Dockable window for Isabelle process control.
4.9 +*/
4.10 +
4.11 +package isabelle.jedit
4.12 +
4.13 +import org.gjt.sp.jedit.View
4.14 +import org.gjt.sp.jedit.gui.DefaultFocusComponent
4.15 +import org.gjt.sp.jedit.gui.DockableWindowManager
4.16 +import org.gjt.sp.jedit.gui.RolloverButton
4.17 +import org.gjt.sp.jedit.gui.HistoryTextField
4.18 +import org.gjt.sp.jedit.GUIUtilities
4.19 +
4.20 +import java.awt.Color
4.21 +import java.awt.Insets
4.22 +import java.awt.BorderLayout
4.23 +import java.awt.Dimension
4.24 +import java.awt.event.ActionListener
4.25 +import java.awt.event.ActionEvent
4.26 +import javax.swing.BoxLayout
4.27 +import javax.swing.JPanel
4.28 +import javax.swing.JScrollPane
4.29 +import javax.swing.JTextPane
4.30 +import javax.swing.text.{StyledDocument, StyleConstants}
4.31 +import javax.swing.SwingUtilities
4.32 +import javax.swing.Icon
4.33 +import javax.swing.Box
4.34 +import javax.swing.JTextField
4.35 +import javax.swing.JComboBox
4.36 +import javax.swing.DefaultComboBoxModel
4.37 +
4.38 +
4.39 +class IsabelleDock(view: View, position: String)
4.40 + extends JPanel(new BorderLayout) with DefaultFocusComponent
4.41 +{
4.42 + private val text = new HistoryTextField("isabelle", false, true)
4.43 + private val logicCombo = new JComboBox
4.44 +
4.45 + {
4.46 + // output pane
4.47 + val pane = new JTextPane
4.48 + pane.setEditable(false)
4.49 + add(BorderLayout.CENTER, new JScrollPane(pane))
4.50 + if (position == DockableWindowManager.FLOATING)
4.51 + setPreferredSize(new Dimension(1000, 500))
4.52 +
4.53 + val doc = pane.getDocument.asInstanceOf[StyledDocument]
4.54 +
4.55 + def makeStyle(name: String, bg: Boolean, color: Color) = {
4.56 + val style = doc.addStyle(name, null)
4.57 + if (bg) StyleConstants.setBackground(style, color)
4.58 + else StyleConstants.setForeground(style, color)
4.59 + style
4.60 + }
4.61 + val rawStyle = makeStyle("raw", false, Color.GRAY)
4.62 + val infoStyle = makeStyle("info", true, new Color(160, 255, 160))
4.63 + val warningStyle = makeStyle("warning", true, new Color(255, 255, 160))
4.64 + val errorStyle = makeStyle("error", true, new Color(255, 160, 160))
4.65 +
4.66 + IsabellePlugin.addPermanentConsumer (result =>
4.67 + if (result != null && !result.is_system) {
4.68 + SwingUtilities.invokeLater(new Runnable {
4.69 + def run = {
4.70 + val logic = IsabellePlugin.isabelle.session
4.71 + logicCombo.setModel(new DefaultComboBoxModel(Array(logic).asInstanceOf[Array[AnyRef]]))
4.72 + logicCombo.setPrototypeDisplayValue("AAAA") // FIXME ??
4.73 +
4.74 + val doc = pane.getDocument.asInstanceOf[StyledDocument]
4.75 + val style = result.kind match {
4.76 + case IsabelleProcess.Kind.WARNING => warningStyle
4.77 + case IsabelleProcess.Kind.ERROR => errorStyle
4.78 + case IsabelleProcess.Kind.TRACING => infoStyle
4.79 + case _ => if (result.is_raw) rawStyle else null
4.80 + }
4.81 + doc.insertString(doc.getLength, IsabellePlugin.result_content(result), style)
4.82 + if (!result.is_raw) doc.insertString(doc.getLength, "\n", style)
4.83 + pane.setCaretPosition(doc.getLength)
4.84 + }
4.85 + })
4.86 + })
4.87 +
4.88 +
4.89 + // control box
4.90 + val box = new Box(BoxLayout.X_AXIS)
4.91 + add(BorderLayout.SOUTH, box)
4.92 +
4.93 +
4.94 + // logic combo
4.95 + logicCombo.setToolTipText("Isabelle logics")
4.96 + logicCombo.setRequestFocusEnabled(false)
4.97 + logicCombo.setModel(new DefaultComboBoxModel(Array("default").asInstanceOf[Array[AnyRef]]))
4.98 + box.add(logicCombo)
4.99 +
4.100 +
4.101 + // mode combo
4.102 + val modeIsar = "Isar"
4.103 + val modeML = "ML"
4.104 + val modes = Array(modeIsar, modeML)
4.105 + var mode = modeIsar
4.106 +
4.107 + val modeCombo = new JComboBox
4.108 + modeCombo.setToolTipText("Toplevel mode")
4.109 + modeCombo.setRequestFocusEnabled(false)
4.110 + modeCombo.setModel(new DefaultComboBoxModel(modes.asInstanceOf[Array[AnyRef]]))
4.111 + modeCombo.setPrototypeDisplayValue("AAAA")
4.112 + modeCombo.addActionListener(new ActionListener {
4.113 + def actionPerformed(evt: ActionEvent): Unit = {
4.114 + mode = modeCombo.getSelectedItem.asInstanceOf[String]
4.115 + }
4.116 + })
4.117 + box.add(modeCombo)
4.118 +
4.119 +
4.120 + // input field
4.121 + text.setToolTipText("Command line")
4.122 + text.addActionListener(new ActionListener {
4.123 + def actionPerformed(evt: ActionEvent): Unit = {
4.124 + val command = text.getText
4.125 + if (command.length > 0) {
4.126 + if (mode == modeIsar)
4.127 + IsabellePlugin.isabelle.command(command)
4.128 + else if (mode == modeML)
4.129 + IsabellePlugin.isabelle.ML(command)
4.130 + text.setText("")
4.131 + }
4.132 + }
4.133 + })
4.134 + box.add(text)
4.135 +
4.136 +
4.137 + // buttons
4.138 + def iconButton(icon: String, tip: String, action: => Unit) = {
4.139 + val button = new RolloverButton(GUIUtilities.loadIcon(icon))
4.140 + button.setToolTipText(tip)
4.141 + button.setMargin(new Insets(0,0,0,0))
4.142 + button.setRequestFocusEnabled(false)
4.143 + button.addActionListener(new ActionListener {
4.144 + def actionPerformed(evt: ActionEvent): Unit = action
4.145 + })
4.146 + box.add(button)
4.147 + }
4.148 +
4.149 + iconButton("Cancel.png", "Stop", IsabellePlugin.isabelle.interrupt)
4.150 + iconButton("Clear.png", "Clear", pane.setText(""))
4.151 + }
4.152 +
4.153 + def focusOnDefaultComponent: Unit = text.requestFocus
4.154 +}
4.155 +
5.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
5.2 +++ b/lib/jedit/plugin/isabelle_parser.scala Sun Aug 24 19:02:22 2008 +0200
5.3 @@ -0,0 +1,61 @@
5.4 +/* Title: lib/jedit/plugin/isabelle_parser.scala
5.5 + ID: $Id$
5.6 + Author: Makarius
5.7 +
5.8 +Isabelle parser setup for Sidekick plugin.
5.9 +*/
5.10 +
5.11 +package isabelle.jedit
5.12 +
5.13 +import javax.swing.text.Position
5.14 +import javax.swing.tree.DefaultMutableTreeNode
5.15 +import javax.swing.tree.DefaultTreeModel
5.16 +
5.17 +import org.gjt.sp.jedit.Buffer
5.18 +import org.gjt.sp.util.Log
5.19 +
5.20 +import sidekick.Asset
5.21 +import sidekick.SideKickParsedData
5.22 +import sidekick.SideKickParser
5.23 +import errorlist.DefaultErrorSource
5.24 +
5.25 +
5.26 +private class IsabelleAsset(name: String, content: String) extends Asset(name)
5.27 +{
5.28 + override def getShortString() = { name }
5.29 + override def getLongString() = { content }
5.30 + override def getIcon() = { null }
5.31 +}
5.32 +
5.33 +
5.34 +class IsabelleParser extends SideKickParser("isabelle") {
5.35 + private var stopped = false
5.36 +
5.37 + override def stop () { stopped = true }
5.38 +
5.39 + def parse(buffer: Buffer, e: DefaultErrorSource): SideKickParsedData = {
5.40 + stopped = false
5.41 +
5.42 + var text: String = null
5.43 + var data: SideKickParsedData = null
5.44 +
5.45 + try {
5.46 + buffer.readLock()
5.47 + text = buffer.getText(0, buffer.getLength())
5.48 + data = new SideKickParsedData(buffer.getName())
5.49 +
5.50 + val asset = new IsabelleAsset("theory", null)
5.51 + asset.setStart(buffer.createPosition(0))
5.52 + asset.setEnd(buffer.createPosition(buffer.getLength()))
5.53 +
5.54 + val node = new DefaultMutableTreeNode(asset)
5.55 + data.root.insert(node, node.getChildCount())
5.56 +
5.57 + } finally {
5.58 + buffer.readUnlock()
5.59 + }
5.60 +
5.61 + data
5.62 + }
5.63 +}
5.64 +
6.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
6.2 +++ b/lib/jedit/plugin/isabelle_plugin.scala Sun Aug 24 19:02:22 2008 +0200
6.3 @@ -0,0 +1,148 @@
6.4 +/* Title: lib/jedit/plugin/isabelle_plugin.scala
6.5 + ID: $Id$
6.6 + Author: Makarius
6.7 +
6.8 +Isabelle/jEdit plugin -- main setup.
6.9 +*/
6.10 +
6.11 +package isabelle.jedit
6.12 +
6.13 +import org.gjt.sp.jedit.EditPlugin
6.14 +import org.gjt.sp.util.Log
6.15 +
6.16 +import errorlist.DefaultErrorSource
6.17 +import errorlist.ErrorSource
6.18 +
6.19 +import java.util.Properties
6.20 +import java.lang.NumberFormatException
6.21 +
6.22 +import scala.collection.mutable.ListBuffer
6.23 +import scala.io.Source
6.24 +
6.25 +
6.26 +/* Global state */
6.27 +
6.28 +object IsabellePlugin {
6.29 + // unique ids
6.30 + @volatile
6.31 + private var idCount = 0
6.32 +
6.33 + def id() : String = synchronized { idCount += 1; "jedit:" + idCount }
6.34 +
6.35 + def idProperties(value: String) : Properties = {
6.36 + val props = new Properties
6.37 + props.setProperty(Markup.ID, value)
6.38 + props
6.39 + }
6.40 +
6.41 + def idProperties() : Properties = { idProperties(id()) }
6.42 +
6.43 +
6.44 + // the error source
6.45 + @volatile
6.46 + var errors: DefaultErrorSource = null
6.47 +
6.48 + // the Isabelle process
6.49 + @volatile
6.50 + var isabelle: IsabelleProcess = null
6.51 +
6.52 +
6.53 + // result content
6.54 + def result_content(result: IsabelleProcess.Result) =
6.55 + XML.content(isabelle.result_tree(result)).mkString("")
6.56 +
6.57 +
6.58 + // result consumers
6.59 + type consumer = IsabelleProcess.Result => Boolean
6.60 + private var consumers = new ListBuffer[consumer]
6.61 +
6.62 + def addConsumer(consumer: consumer) = synchronized { consumers += consumer }
6.63 +
6.64 + def addPermanentConsumer(consumer: IsabelleProcess.Result => Unit) = {
6.65 + addConsumer(result => { consumer(result); false })
6.66 + }
6.67 +
6.68 + def delConsumer(consumer: consumer) = synchronized { consumers -= consumer }
6.69 +
6.70 + def consume(result: IsabelleProcess.Result) : Unit = {
6.71 + synchronized { consumers.elements.toList } foreach (consumer =>
6.72 + {
6.73 + val finished =
6.74 + try { consumer(result) }
6.75 + catch { case e: Throwable => Log.log(Log.ERROR, this, e); true }
6.76 + if (finished || result == null)
6.77 + delConsumer(consumer)
6.78 + })
6.79 + }
6.80 +}
6.81 +
6.82 +
6.83 +/* Main plugin setup */
6.84 +
6.85 +class IsabellePlugin extends EditPlugin {
6.86 + private var thread: Thread = null
6.87 +
6.88 + override def start = {
6.89 + // error source
6.90 + IsabellePlugin.errors = new DefaultErrorSource("isabelle")
6.91 + ErrorSource.registerErrorSource(IsabellePlugin.errors)
6.92 +
6.93 + IsabellePlugin.addPermanentConsumer (result =>
6.94 + if (result != null && result.props != null &&
6.95 + (result.kind == IsabelleProcess.Kind.WARNING ||
6.96 + result.kind == IsabelleProcess.Kind.ERROR)) {
6.97 + val typ =
6.98 + if (result.kind == IsabelleProcess.Kind.WARNING) ErrorSource.WARNING
6.99 + else ErrorSource.ERROR
6.100 + (Position.line_of(result.props), Position.file_of(result.props)) match {
6.101 + case (Some(line), Some(file)) =>
6.102 + val content = IsabellePlugin.result_content(result)
6.103 + if (content.length > 0) {
6.104 + val lines = Source.fromString(content).getLines
6.105 + val err = new DefaultErrorSource.DefaultError(IsabellePlugin.errors,
6.106 + typ, file, line - 1, 0, 0, lines.next)
6.107 + for (msg <- lines) err.addExtraMessage(msg)
6.108 + IsabellePlugin.errors.addError(err)
6.109 + }
6.110 + case _ =>
6.111 + }
6.112 + })
6.113 +
6.114 +
6.115 + // Isabelle process
6.116 + IsabellePlugin.isabelle =
6.117 + new IsabelleProcess("-mno_brackets", "-mno_type_brackets", "-mxsymbols")
6.118 + thread = new Thread (new Runnable {
6.119 + def run = {
6.120 + var result: IsabelleProcess.Result = null
6.121 + do {
6.122 + try {
6.123 + result = IsabellePlugin.isabelle.results.take
6.124 + }
6.125 + catch {
6.126 + case _: NullPointerException => result = null
6.127 + case _: InterruptedException => result = null
6.128 + }
6.129 + if (result != null) {
6.130 + System.err.println(result) // FIXME
6.131 + IsabellePlugin.consume(result)
6.132 + }
6.133 + if (result.kind == IsabelleProcess.Kind.EXIT) {
6.134 + result = null
6.135 + IsabellePlugin.consume(null)
6.136 + }
6.137 + } while (result != null)
6.138 + }
6.139 + })
6.140 + thread.start
6.141 + }
6.142 +
6.143 + override def stop = {
6.144 + IsabellePlugin.isabelle.kill
6.145 + thread.interrupt; thread.join; thread = null
6.146 + IsabellePlugin.isabelle = null
6.147 +
6.148 + ErrorSource.unregisterErrorSource(IsabellePlugin.errors)
6.149 + IsabellePlugin.errors = null
6.150 + }
6.151 +}
7.1 --- a/lib/jedit/plugin/mk Sun Aug 24 18:57:43 2008 +0200
7.2 +++ b/lib/jedit/plugin/mk Sun Aug 24 19:02:22 2008 +0200
7.3 @@ -10,9 +10,9 @@
7.4
7.5 scalac -d build \
7.6 -cp $JEDIT_HOME/jedit.jar:$PLUGINS/SideKick.jar:$PLUGINS/ErrorList.jar:$PLUGINS/Console.jar:../../classes/Pure.jar \
7.7 - isabelle/IsabellePlugin.scala \
7.8 - isabelle/IsabelleDock.scala \
7.9 - isabelle/IsabelleParser.scala \
7.10 + isabelle_plugin.scala \
7.11 + isabelle_dock.scala \
7.12 + isabelle_parser.scala \
7.13 && (
7.14 cp *.xml *.props build/
7.15 cd build