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