1/*  Title:      Tools/jEdit/src/jedit_sessions.scala
2    Author:     Makarius
3
4Isabelle/jEdit session information, based on implicit process environment
5and explicit options.
6*/
7
8package isabelle.jedit
9
10
11import isabelle._
12
13import scala.swing.ComboBox
14import scala.swing.event.SelectionChanged
15
16
17object JEdit_Sessions
18{
19  /* session options */
20
21  def session_options(options: Options): Options =
22    Isabelle_System.getenv("JEDIT_ML_PROCESS_POLICY") match {
23      case "" => options
24      case s => options.string.update("ML_process_policy", s)
25    }
26
27  def session_dirs(): List[Path] =
28    Path.split(Isabelle_System.getenv("JEDIT_SESSION_DIRS"))
29
30  def session_build_mode(): String = Isabelle_System.getenv("JEDIT_BUILD_MODE")
31
32
33  /* raw logic info */
34
35  private val jedit_logic_option = "jedit_logic"
36
37  def logic_name(options: Options): String =
38    Isabelle_System.default_logic(
39      Isabelle_System.getenv("JEDIT_LOGIC"),
40      options.string(jedit_logic_option))
41
42  def logic_ancestor: Option[String] = proper_string(Isabelle_System.getenv("JEDIT_LOGIC_ANCESTOR"))
43  def logic_requirements: Boolean = Isabelle_System.getenv("JEDIT_LOGIC_REQUIREMENTS") == "true"
44  def logic_focus: Boolean = Isabelle_System.getenv("JEDIT_LOGIC_FOCUS") == "true"
45  def logic_include_sessions: List[String] =
46    space_explode(':', Isabelle_System.getenv("JEDIT_INCLUDE_SESSIONS"))
47
48  def logic_info(options: Options): Option[Sessions.Info] =
49    try {
50      Sessions.load_structure(session_options(options), dirs = session_dirs()).
51        get(logic_name(options))
52    }
53    catch { case ERROR(_) => None }
54
55  def logic_root(options: Options): Position.T =
56    if (logic_requirements) logic_info(options).map(_.pos) getOrElse Position.none
57    else Position.none
58
59
60  /* logic selector */
61
62  private class Logic_Entry(val name: String, val description: String)
63  {
64    override def toString: String = description
65  }
66
67  def logic_selector(options: Options_Variable, autosave: Boolean): Option_Component =
68  {
69    GUI_Thread.require {}
70
71    val session_list =
72    {
73      val sessions_structure = Sessions.load_structure(options.value, dirs = session_dirs())
74      val (main_sessions, other_sessions) =
75        sessions_structure.imports_topological_order.
76          partition(name => sessions_structure(name).groups.contains("main"))
77      main_sessions.sorted ::: other_sessions.sorted
78    }
79
80    val entries =
81      new Logic_Entry("", "default (" + logic_name(options.value) + ")") ::
82        session_list.map(name => new Logic_Entry(name, name))
83
84    val component = new ComboBox(entries) with Option_Component {
85      name = jedit_logic_option
86      val title = "Logic"
87      def load: Unit =
88      {
89        val logic = options.string(jedit_logic_option)
90        entries.find(_.name == logic) match {
91          case Some(entry) => selection.item = entry
92          case None =>
93        }
94      }
95      def save: Unit = options.string(jedit_logic_option) = selection.item.name
96    }
97
98    component.load()
99    if (autosave) {
100      component.listenTo(component.selection)
101      component.reactions += { case SelectionChanged(_) => component.save() }
102    }
103    component.tooltip = "Logic session name (change requires restart)"
104    component
105  }
106
107
108  /* session build process */
109
110  def session_base_info(options: Options): Sessions.Base_Info =
111    Sessions.base_info(options,
112      dirs = JEdit_Sessions.session_dirs(),
113      include_sessions = logic_include_sessions,
114      session = logic_name(options),
115      session_ancestor = logic_ancestor,
116      session_requirements = logic_requirements,
117      session_focus = logic_focus,
118      all_known = !logic_focus)
119
120  def session_build(
121    options: Options, progress: Progress = No_Progress, no_build: Boolean = false): Int =
122  {
123    val mode = session_build_mode()
124
125    Build.build(session_options(options), progress = progress, build_heap = true,
126      no_build = no_build, system_mode = mode == "" || mode == "system",
127      dirs = session_dirs(), infos = PIDE.resources.session_base_info.infos,
128      sessions = List(PIDE.resources.session_name)).rc
129  }
130
131  def session_start(options: Options)
132  {
133    Isabelle_Process.start(PIDE.session, session_options(options),
134      sessions_structure = Some(PIDE.resources.session_base_info.sessions_structure),
135      logic = PIDE.resources.session_name,
136      store = Some(Sessions.store(options, session_build_mode() == "system")),
137      modes =
138        (space_explode(',', options.string("jedit_print_mode")) :::
139         space_explode(',', Isabelle_System.getenv("JEDIT_PRINT_MODE"))).reverse,
140      phase_changed = PIDE.plugin.session_phase_changed)
141  }
142}
143