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

}