lib/jedit/plugin/isabelle_dock.scala

rearranged source files;

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