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