--- /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
+}
+