src/Tools/jEdit/src/jedit_options.scala

more operations;

/*  Title:      Tools/jEdit/src/jedit_options.scala
    Author:     Makarius

Options for Isabelle/jEdit.
*/

package isabelle.jedit


import isabelle._

import java.awt.{Font, Color}
import javax.swing.{InputVerifier, JComponent, UIManager}
import javax.swing.text.JTextComponent

import scala.swing.{Component, CheckBox, TextArea}

import org.gjt.sp.jedit.gui.ColorWellButton
import org.gjt.sp.jedit.{jEdit, AbstractOptionPane}


object JEdit_Options {
  /* typed access and GUI components */

  class Access[A](access: Options.Access_Variable[A], val name: String) {
    def description: String = access.options.value.description(name)
    def apply(): A = access.apply(name)
    def update(x: A): Unit = change(_ => x)
    def change(f: A => A): Unit = {
      val x0 = apply()
      access.change(name, f)
      val x1 = apply()
      if (x0 != x1) changed()
    }
    def changed(): Unit = GUI_Thread.require { PIDE.session.update_options(access.options.value) }
  }

  class Bool_Access(name: String) extends Access(PIDE.options.bool, name) {
    def set(): Unit = update(true)
    def reset(): Unit = update(false)
    def toggle(): Unit = change(b => !b)
  }

  class Bool_GUI(access: Bool_Access, label: String)
  extends GUI.Check(label, init = access()) {
    def load(): Unit = { selected = access() }
    override def clicked(state: Boolean): Unit = access.update(state)
  }


  /* specific options */

  object continuous_checking extends Bool_Access("editor_continuous_checking") {
    override def changed(): Unit = {
      super.changed()
      PIDE.plugin.deps_changed()
    }

    class GUI extends Bool_GUI(this, "Continuous checking") {
      tooltip = "Continuous checking of proof document (visible and required parts)"
    }
  }

  object output_state extends Bool_Access("editor_output_state") {
    override def changed(): Unit = GUI_Thread.require {
      super.changed()
      PIDE.editor.flush_edits(hidden = true)
      PIDE.editor.flush()
    }

    class GUI extends Bool_GUI(this, "Proof state") {
      tooltip = "Output of proof state (normally shown on State panel)"
    }
  }



  /* editor pane for plugin options */

  trait Entry extends Component {
    val title: String
    def load(): Unit
    def save(): Unit
  }

  abstract class Isabelle_Options(name: String) extends AbstractOptionPane(name) {
    protected val components: List[(String, List[Entry])]

    override def _init(): Unit = {
      val dummy_property = "options.isabelle.dummy"

      for ((s, cs) <- components) {
        if (s.nonEmpty) {
          jEdit.setProperty(dummy_property, s)
          addSeparator(dummy_property)
          jEdit.setProperty(dummy_property, null)
        }
        for (c <- cs) addComponent(c.title, c.peer)
      }
    }

    override def _save(): Unit = {
      for ((_, cs) <- components; c <- cs) c.save()
    }
  }

  class Isabelle_General_Options extends Isabelle_Options("isabelle-general") {
    val options: JEdit_Options = PIDE.options

    private val predefined =
      List(
        JEdit_Sessions.logic_selector(options),
        JEdit_Sessions.document_selector(options),
        JEdit_Spell_Checker.dictionaries_selector())

    protected val components: List[(String, List[Entry])] =
      options.make_components(predefined,
        (for ((name, opt) <- options.value.opt_iterator if opt.public) yield name).toSet)
  }

  class Isabelle_Rendering_Options extends Isabelle_Options("isabelle-rendering") {
    private val predefined =
      (for {
        (name, opt) <- PIDE.options.value.opt_iterator
        if name.endsWith("_color") && opt.section == "Rendering of Document Content"
      } yield PIDE.options.make_color_component(opt)).toList

    assert(predefined.nonEmpty)

    protected val components: List[(String, List[Entry])] =
      PIDE.options.make_components(predefined, _ => false)
  }
}

class JEdit_Options(init_options: Options) extends Options_Variable(init_options) {
  def color_value(s: String): Color = Color_Value(string(s))

  def make_color_component(opt: Options.Opt): JEdit_Options.Entry = {
    GUI_Thread.require {}

    val opt_name = opt.name
    val opt_title = opt.title_jedit

    val button = new ColorWellButton(Color_Value(opt.value))
    val component =
      new Component with JEdit_Options.Entry {
        override lazy val peer: JComponent = button
        name = opt_name
        val title: String = opt_title
        def load(): Unit = button.setSelectedColor(Color_Value(string(opt_name)))
        def save(): Unit = string(opt_name) = Color_Value.print(button.getSelectedColor)
      }
    component.tooltip = GUI.tooltip_lines(opt.print_default)
    component
  }

  def make_component(opt: Options.Opt): JEdit_Options.Entry = {
    GUI_Thread.require {}

    val opt_name = opt.name
    val opt_title = opt.title_jedit

    val component =
      if (opt.typ == Options.Bool)
        new CheckBox with JEdit_Options.Entry {
          name = opt_name
          val title: String = opt_title
          def load(): Unit = selected = bool(opt_name)
          def save(): Unit = bool(opt_name) = selected
        }
      else {
        val default_font = GUI.copy_font(UIManager.getFont("TextField.font"))
        val text_area =
          new TextArea with JEdit_Options.Entry {
            if (default_font != null) font = default_font
            name = opt_name
            val title: String = opt_title
            def load(): Unit = text = value.check_name(opt_name).value
            def save(): Unit =
              try { JEdit_Options.this += (opt_name, text) }
              catch {
                case ERROR(msg) =>
                  GUI.error_dialog(this.peer, "Failed to update options",
                    GUI.scrollable_text(msg))
              }
          }
        text_area.peer.setInputVerifier({
            case text: JTextComponent =>
              try { value + (opt_name, text.getText); true }
              catch { case ERROR(_) => false }
            case _ => true
          })
        GUI.plain_focus_traversal(text_area.peer)
        text_area
      }
    component.load()
    component.tooltip = GUI.tooltip_lines(opt.print_default)
    component
  }

  def make_components(
    predefined: List[JEdit_Options.Entry],
    filter: String => Boolean
  ) : List[(String, List[JEdit_Options.Entry])] = {
    def mk_component(opt: Options.Opt): List[JEdit_Options.Entry] =
      predefined.find(opt.name == _.name) match {
        case Some(c) => List(c)
        case None => if (filter(opt.name)) List(make_component(opt)) else Nil
      }
    value.sections.sortBy(_._1).map(
        { case (a, opts) => (a, opts.sortBy(_.title_jedit).flatMap(mk_component)) })
      .filterNot(_._2.isEmpty)
  }
}