src/Tools/jEdit/src/jedit_sessions.scala
changeset 62973 744266e32612
parent 62972 0eedd78c2b47
child 62974 f17602cbf76a
equal deleted inserted replaced
62972:0eedd78c2b47 62973:744266e32612
       
     1 /*  Title:      Tools/jEdit/src/jedit_sessions.scala
       
     2     Author:     Makarius
       
     3 
       
     4 Isabelle/jEdit session information.
       
     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 JEdit_Sessions
       
    17 {
       
    18   /* session info */
       
    19 
       
    20   private val option_name = "jedit_logic"
       
    21 
       
    22   def session_name(): String =
       
    23     Isabelle_System.default_logic(
       
    24       Isabelle_System.getenv("JEDIT_LOGIC"),
       
    25       PIDE.options.string(option_name))
       
    26 
       
    27   def session_dirs(): List[Path] = Path.split(Isabelle_System.getenv("JEDIT_SESSION_DIRS"))
       
    28 
       
    29   def session_build_mode(): String = Isabelle_System.getenv("JEDIT_BUILD_MODE")
       
    30 
       
    31   def session_build(progress: Progress = Ignore_Progress, no_build: Boolean = false): Int =
       
    32   {
       
    33     val mode = session_build_mode()
       
    34 
       
    35     Build.build(options = PIDE.options.value, progress = progress,
       
    36       build_heap = true, no_build = no_build, system_mode = mode == "" || mode == "system",
       
    37       dirs = session_dirs(), sessions = List(session_name())).rc
       
    38   }
       
    39 
       
    40   def session_start()
       
    41   {
       
    42     val modes =
       
    43       (space_explode(',', PIDE.options.string("jedit_print_mode")) :::
       
    44        space_explode(',', Isabelle_System.getenv("JEDIT_PRINT_MODE"))).reverse
       
    45     PIDE.session.start(receiver =>
       
    46       Isabelle_Process(PIDE.options.value, logic = session_name(), dirs = session_dirs(),
       
    47         modes = modes, receiver = receiver,
       
    48         store = Sessions.store(session_build_mode() == "system")))
       
    49   }
       
    50 
       
    51   def session_list(): List[String] =
       
    52   {
       
    53     val session_tree = Sessions.load(PIDE.options.value, dirs = session_dirs())
       
    54     val (main_sessions, other_sessions) =
       
    55       session_tree.topological_order.partition(p => p._2.groups.contains("main"))
       
    56     main_sessions.map(_._1).sorted ::: other_sessions.map(_._1).sorted
       
    57   }
       
    58 
       
    59   def session_content(inlined_files: Boolean): Build.Session_Content =
       
    60   {
       
    61     val content =
       
    62       Build.session_content(PIDE.options.value, inlined_files, session_dirs(), session_name())
       
    63     content.copy(known_theories =
       
    64       content.known_theories.mapValues(name => name.map(File.platform_path(_))))
       
    65   }
       
    66 
       
    67 
       
    68   /* logic selector */
       
    69 
       
    70   private class Logic_Entry(val name: String, val description: String)
       
    71   {
       
    72     override def toString: String = description
       
    73   }
       
    74 
       
    75   def logic_selector(autosave: Boolean): Option_Component =
       
    76   {
       
    77     GUI_Thread.require {}
       
    78 
       
    79     val entries =
       
    80       new Logic_Entry("", "default (" + session_name() + ")") ::
       
    81         JEdit_Sessions.session_list().map(name => new Logic_Entry(name, name))
       
    82 
       
    83     val component = new ComboBox(entries) with Option_Component {
       
    84       name = option_name
       
    85       val title = "Logic"
       
    86       def load: Unit =
       
    87       {
       
    88         val logic = PIDE.options.string(option_name)
       
    89         entries.find(_.name == logic) match {
       
    90           case Some(entry) => selection.item = entry
       
    91           case None =>
       
    92         }
       
    93       }
       
    94       def save: Unit = PIDE.options.string(option_name) = selection.item.name
       
    95     }
       
    96 
       
    97     component.load()
       
    98     if (autosave) {
       
    99       component.listenTo(component.selection)
       
   100       component.reactions += { case SelectionChanged(_) => component.save() }
       
   101     }
       
   102     component.tooltip = "Logic session name (change requires restart)"
       
   103     component
       
   104   }
       
   105 }