1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/lib/jedit/plugin/isabelle_dock.scala Sun Aug 24 19:02:22 2008 +0200
1.3 @@ -0,0 +1,152 @@
1.4 +/* Title: lib/jedit/plugin/isabelle_dock.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 +