src/Tools/jEdit/src/isabelle_logic.scala
author wenzelm
Tue Aug 12 15:46:20 2014 +0200 (2014-08-12)
changeset 57912 dd9550f84106
parent 57612 990ffb84489b
child 60992 89effcb342df
permissions -rw-r--r--
tuned;
     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 val option_name = "jedit_logic"
    19 
    20   private def jedit_logic(): String =
    21     Isabelle_System.default_logic(
    22       Isabelle_System.getenv("JEDIT_LOGIC"),
    23       PIDE.options.string(option_name))
    24 
    25   private class Logic_Entry(val name: String, val description: String)
    26   {
    27     override def toString: String = description
    28   }
    29 
    30   def logic_selector(autosave: Boolean): Option_Component =
    31   {
    32     GUI_Thread.require {}
    33 
    34     val entries =
    35       new Logic_Entry("", "default (" + jedit_logic() + ")") ::
    36         Isabelle_Logic.session_list().map(name => new Logic_Entry(name, name))
    37 
    38     val component = new ComboBox(entries) with Option_Component {
    39       name = option_name
    40       val title = "Logic"
    41       def load: Unit =
    42       {
    43         val logic = PIDE.options.string(option_name)
    44         entries.find(_.name == logic) match {
    45           case Some(entry) => selection.item = entry
    46           case None =>
    47         }
    48       }
    49       def save: Unit = PIDE.options.string(option_name) = selection.item.name
    50     }
    51 
    52     component.load()
    53     if (autosave) {
    54       component.listenTo(component.selection)
    55       component.reactions += { case SelectionChanged(_) => component.save() }
    56     }
    57     component.tooltip = "Logic session name (change requires restart)"
    58     component
    59   }
    60 
    61   def session_args(): List[String] =
    62   {
    63     val modes =
    64       space_explode(',', PIDE.options.string("jedit_print_mode")) :::
    65       space_explode(',', Isabelle_System.getenv("JEDIT_PRINT_MODE"))
    66 
    67     modes.map("-m" + _) ::: List("-r", "-q", jedit_logic())
    68   }
    69 
    70   def session_dirs(): List[Path] = Path.split(Isabelle_System.getenv("JEDIT_SESSION_DIRS"))
    71 
    72   def session_list(): List[String] =
    73   {
    74     val session_tree = Build.find_sessions(PIDE.options.value, dirs = session_dirs())
    75     val (main_sessions, other_sessions) =
    76       session_tree.topological_order.partition(p => p._2.groups.contains("main"))
    77     main_sessions.map(_._1).sorted ::: other_sessions.map(_._1).sorted
    78   }
    79 
    80   def session_content(inlined_files: Boolean): Build.Session_Content =
    81   {
    82     val dirs = session_dirs()
    83     val name = session_args().last
    84     val content = Build.session_content(PIDE.options.value, inlined_files, dirs, name)
    85     content.copy(known_theories =
    86       content.known_theories.mapValues(name => name.map(Isabelle_System.jvm_path(_))))
    87   }
    88 }
    89