src/Tools/jEdit/src/isabelle_logic.scala
author wenzelm
Mon Sep 10 19:56:08 2012 +0200 (2012-09-10)
changeset 49248 bff772033a97
parent 49247 ffd9ad9dc35b
child 49270 e5d162d15867
permissions -rw-r--r--
proper multi-line tooltip;
wenzelm@49246
     1
/*  Title:      Tools/jEdit/src/isabelle_logic.scala
wenzelm@49246
     2
    Author:     Makarius
wenzelm@49246
     3
wenzelm@49246
     4
Isabellel logic session.
wenzelm@49246
     5
*/
wenzelm@49246
     6
wenzelm@49246
     7
package isabelle.jedit
wenzelm@49246
     8
wenzelm@49246
     9
wenzelm@49246
    10
import isabelle._
wenzelm@49246
    11
wenzelm@49246
    12
import scala.swing.ComboBox
wenzelm@49246
    13
import scala.swing.event.SelectionChanged
wenzelm@49246
    14
wenzelm@49246
    15
wenzelm@49246
    16
object Isabelle_Logic
wenzelm@49246
    17
{
wenzelm@49246
    18
  private def default_logic(): String =
wenzelm@49246
    19
  {
wenzelm@49246
    20
    val logic = Isabelle_System.getenv("JEDIT_LOGIC")
wenzelm@49246
    21
    if (logic != "") logic
wenzelm@49246
    22
    else Isabelle_System.getenv_strict("ISABELLE_LOGIC")
wenzelm@49246
    23
  }
wenzelm@49246
    24
wenzelm@49246
    25
  private class Logic_Entry(val name: String, val description: String)
wenzelm@49246
    26
  {
wenzelm@49246
    27
    override def toString = description
wenzelm@49246
    28
  }
wenzelm@49246
    29
wenzelm@49246
    30
  def logic_selector(autosave: Boolean): Option_Component =
wenzelm@49246
    31
  {
wenzelm@49246
    32
    Swing_Thread.require()
wenzelm@49246
    33
wenzelm@49246
    34
    val entries =
wenzelm@49246
    35
      new Logic_Entry("", "default (" + default_logic() + ")") ::
wenzelm@49246
    36
        Isabelle_System.find_logics().map(name => new Logic_Entry(name, name))
wenzelm@49246
    37
wenzelm@49246
    38
    val component = new ComboBox(entries) with Option_Component {
wenzelm@49246
    39
      val title = Isabelle.options.title("jedit_logic")
wenzelm@49247
    40
      def load: Unit =
wenzelm@49247
    41
      {
wenzelm@49247
    42
        val logic = Isabelle.options.string("jedit_logic")
wenzelm@49247
    43
        entries.find(_.name == logic) match {
wenzelm@49247
    44
          case Some(entry) => selection.item = entry
wenzelm@49247
    45
          case None =>
wenzelm@49247
    46
        }
wenzelm@49247
    47
      }
wenzelm@49247
    48
      def save: Unit = Isabelle.options.string("jedit_logic") = selection.item.name
wenzelm@49246
    49
    }
wenzelm@49246
    50
wenzelm@49247
    51
    component.load()
wenzelm@49246
    52
    if (autosave) {
wenzelm@49246
    53
      component.listenTo(component.selection)
wenzelm@49246
    54
      component.reactions += { case SelectionChanged(_) => component.save() }
wenzelm@49246
    55
    }
wenzelm@49248
    56
    component.tooltip = Isabelle.tooltip(Isabelle.options.value.check_name("jedit_logic").print)
wenzelm@49246
    57
    component
wenzelm@49246
    58
  }
wenzelm@49246
    59
wenzelm@49246
    60
  def session_args(): List[String] =
wenzelm@49246
    61
  {
wenzelm@49246
    62
    val modes = space_explode(',', Isabelle_System.getenv("JEDIT_PRINT_MODE")).map("-m" + _)
wenzelm@49246
    63
    val logic =
wenzelm@49246
    64
      Isabelle.options.string("jedit_logic") match {
wenzelm@49246
    65
        case "" => default_logic()
wenzelm@49246
    66
        case logic => logic
wenzelm@49246
    67
      }
wenzelm@49246
    68
    modes ::: List(logic)
wenzelm@49246
    69
  }
wenzelm@49246
    70
wenzelm@49246
    71
  def session_content(inlined_files: Boolean): Build.Session_Content =
wenzelm@49246
    72
  {
wenzelm@49246
    73
    val dirs = Path.split(Isabelle_System.getenv("JEDIT_SESSION_DIRS"))
wenzelm@49246
    74
    val name = Path.explode(session_args().last).base.implode  // FIXME more robust
wenzelm@49246
    75
    Build.session_content(inlined_files, dirs, name).check_errors
wenzelm@49246
    76
  }
wenzelm@49246
    77
}
wenzelm@49246
    78