src/Tools/jEdit/src/isabelle_logic.scala
author wenzelm
Wed Dec 05 19:25:57 2012 +0100 (2012-12-05)
changeset 50375 c101127a7f37
parent 50205 788c8263e634
child 50380 b1cb76418760
permissions -rw-r--r--
clarified logic argument: session name, not path name;
tuned;
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@50375
    30
  private val option_name = "jedit_logic"
wenzelm@49270
    31
wenzelm@49246
    32
  def logic_selector(autosave: Boolean): Option_Component =
wenzelm@49246
    33
  {
wenzelm@49246
    34
    Swing_Thread.require()
wenzelm@49246
    35
wenzelm@49246
    36
    val entries =
wenzelm@49246
    37
      new Logic_Entry("", "default (" + default_logic() + ")") ::
wenzelm@49246
    38
        Isabelle_System.find_logics().map(name => new Logic_Entry(name, name))
wenzelm@49246
    39
wenzelm@49246
    40
    val component = new ComboBox(entries) with Option_Component {
wenzelm@50375
    41
      name = option_name
wenzelm@49270
    42
      val title = "Logic"
wenzelm@49247
    43
      def load: Unit =
wenzelm@49247
    44
      {
wenzelm@50375
    45
        val logic = PIDE.options.string(option_name)
wenzelm@49247
    46
        entries.find(_.name == logic) match {
wenzelm@49247
    47
          case Some(entry) => selection.item = entry
wenzelm@49247
    48
          case None =>
wenzelm@49247
    49
        }
wenzelm@49247
    50
      }
wenzelm@50375
    51
      def save: Unit = PIDE.options.string(option_name) = selection.item.name
wenzelm@49246
    52
    }
wenzelm@49246
    53
wenzelm@49247
    54
    component.load()
wenzelm@49246
    55
    if (autosave) {
wenzelm@49246
    56
      component.listenTo(component.selection)
wenzelm@49246
    57
      component.reactions += { case SelectionChanged(_) => component.save() }
wenzelm@49246
    58
    }
wenzelm@50375
    59
    component.tooltip = PIDE.options.value.check_name(option_name).print_default
wenzelm@49246
    60
    component
wenzelm@49246
    61
  }
wenzelm@49246
    62
wenzelm@49246
    63
  def session_args(): List[String] =
wenzelm@49246
    64
  {
wenzelm@49246
    65
    val modes = space_explode(',', Isabelle_System.getenv("JEDIT_PRINT_MODE")).map("-m" + _)
wenzelm@49246
    66
    val logic =
wenzelm@50375
    67
      PIDE.options.string(option_name) match {
wenzelm@49246
    68
        case "" => default_logic()
wenzelm@49246
    69
        case logic => logic
wenzelm@49246
    70
      }
wenzelm@49246
    71
    modes ::: List(logic)
wenzelm@49246
    72
  }
wenzelm@49246
    73
wenzelm@49246
    74
  def session_content(inlined_files: Boolean): Build.Session_Content =
wenzelm@49246
    75
  {
wenzelm@49246
    76
    val dirs = Path.split(Isabelle_System.getenv("JEDIT_SESSION_DIRS"))
wenzelm@50375
    77
    val name = session_args().last
wenzelm@49246
    78
    Build.session_content(inlined_files, dirs, name).check_errors
wenzelm@49246
    79
  }
wenzelm@49246
    80
}
wenzelm@49246
    81