diff --git a/src/Tools/jEdit/src/isabelle_session.scala b/src/Tools/jEdit/src/isabelle_session.scala --- a/src/Tools/jEdit/src/isabelle_session.scala +++ b/src/Tools/jEdit/src/isabelle_session.scala @@ -1,104 +1,98 @@ /* Title: Tools/jEdit/src/isabelle_session.scala Author: Makarius Access Isabelle session information via virtual file-system. */ package isabelle.jedit import isabelle._ import java.awt.Component import java.io.InputStream import org.gjt.sp.jedit.View import org.gjt.sp.jedit.io.{VFS => JEdit_VFS, VFSFile} import org.gjt.sp.jedit.browser.VFSBrowser object Isabelle_Session { - /* sessions structure */ - - def sessions_structure(): Sessions.Structure = - JEdit_Sessions.sessions_structure(PIDE.options.value) - - /* virtual file-system */ val vfs_prefix = "isabelle-session:" class Session_Entry(name: String, path: String, marker: String) extends VFSFile(name, path, vfs_prefix + name, VFSFile.FILE, 0L, false) { override def getPathMarker: String = marker override def getExtendedAttribute(att: String): String = if (att == JEdit_VFS.EA_SIZE) null else super.getExtendedAttribute(att) } class VFS extends Isabelle_VFS( vfs_prefix, read = true, browse = true, low_latency = true, non_awt_session = true ) { override def _listFiles( vfs_session: AnyRef, url: String, component: Component ): Array[VFSFile] = { explode_url(url, component = component) match { case None => null case Some(elems) => - val sessions = sessions_structure() + val sessions = JEdit_Sessions.sessions_structure() elems match { case Nil => sessions.chapters.iterator.map(p => make_entry(p._1, is_dir = true)).toArray case List(chapter) => sessions.chapters.get(chapter) match { case None => null case Some(infos) => infos.map(info => { val name = chapter + "/" + info.name val path = Position.File.unapply(info.pos) match { case Some(path) => File.platform_path(path) case None => null } val marker = Position.Line.unapply(info.pos) match { case Some(line) => "+line:" + line case None => null } new Session_Entry(name, path, marker) }).toArray } case _ => null } } } } /* open browser */ def open_browser(view: View): Unit = { val path = PIDE.maybe_snapshot(view) match { case None => "" case Some(snapshot) => - val sessions = sessions_structure() + val sessions = JEdit_Sessions.sessions_structure() val session = PIDE.resources.session_base.theory_qualifier(snapshot.node_name) val chapter = sessions.get(session) match { case Some(info) => info.chapter case None => Sessions.UNSORTED } chapter } VFSBrowser.browseDirectory(view, vfs_prefix + path) } } diff --git a/src/Tools/jEdit/src/jedit_sessions.scala b/src/Tools/jEdit/src/jedit_sessions.scala --- a/src/Tools/jEdit/src/jedit_sessions.scala +++ b/src/Tools/jEdit/src/jedit_sessions.scala @@ -1,147 +1,151 @@ /* Title: Tools/jEdit/src/jedit_sessions.scala Author: Makarius Isabelle/jEdit session information, based on implicit process environment and explicit options. */ package isabelle.jedit import isabelle._ import scala.swing.ComboBox import scala.swing.event.SelectionChanged object JEdit_Sessions { /* session options */ def session_dirs: List[Path] = Path.split(Isabelle_System.getenv("JEDIT_SESSION_DIRS")).filterNot(p => p.implode == "-") def session_no_build: Boolean = Isabelle_System.getenv("JEDIT_NO_BUILD") == "true" def session_options(options: Options): Options = { val options1 = Isabelle_System.getenv("JEDIT_BUILD_MODE") match { case "default" => options case mode => options.bool.update("system_heaps", mode == "system") } val options2 = Isabelle_System.getenv("JEDIT_ML_PROCESS_POLICY") match { case "" => options1 case s => options1.string.update("ML_process_policy", s) } options2 } - def sessions_structure(options: Options, dirs: List[Path] = session_dirs): Sessions.Structure = + def sessions_structure( + options: Options = PIDE.options.value, + dirs: List[Path] = session_dirs + ): Sessions.Structure = { Sessions.load_structure(session_options(options), dirs = dirs) + } /* raw logic info */ private val jedit_logic_option = "jedit_logic" def logic_name(options: Options): String = Isabelle_System.default_logic( Isabelle_System.getenv("JEDIT_LOGIC"), options.string(jedit_logic_option)) def logic_ancestor: Option[String] = proper_string(Isabelle_System.getenv("JEDIT_LOGIC_ANCESTOR")) def logic_requirements: Boolean = Isabelle_System.getenv("JEDIT_LOGIC_REQUIREMENTS") == "true" def logic_include_sessions: List[String] = space_explode(':', Isabelle_System.getenv("JEDIT_INCLUDE_SESSIONS")) def logic_info(options: Options): Option[Sessions.Info] = - try { sessions_structure(options).get(logic_name(options)) } + try { sessions_structure(options = options).get(logic_name(options)) } catch { case ERROR(_) => None } def logic_root(options: Options): Position.T = if (logic_requirements) logic_info(options).map(_.pos) getOrElse Position.none else Position.none /* logic selector */ private class Logic_Entry(val name: String, val description: String) { override def toString: String = description } def logic_selector(options: Options_Variable, autosave: Boolean): Option_Component = { GUI_Thread.require {} val session_list = { - val sessions = sessions_structure(options.value) + val sessions = sessions_structure(options = options.value) val (main_sessions, other_sessions) = sessions.imports_topological_order.partition(name => sessions(name).groups.contains("main")) main_sessions.sorted ::: other_sessions.sorted } val entries = new Logic_Entry("", "default (" + logic_name(options.value) + ")") :: session_list.map(name => new Logic_Entry(name, name)) val component = new ComboBox(entries) with Option_Component { name = jedit_logic_option val title = "Logic" def load(): Unit = { val logic = options.string(jedit_logic_option) entries.find(_.name == logic) match { case Some(entry) => selection.item = entry case None => } } def save(): Unit = options.string(jedit_logic_option) = selection.item.name } component.load() if (autosave) { component.listenTo(component.selection) component.reactions += { case SelectionChanged(_) => component.save() } } component.tooltip = "Logic session name (change requires restart)" component } /* session build process */ def session_base_info(options: Options): Sessions.Base_Info = Sessions.base_info(options, dirs = JEdit_Sessions.session_dirs, include_sessions = logic_include_sessions, session = logic_name(options), session_ancestor = logic_ancestor, session_requirements = logic_requirements) def session_build( options: Options, progress: Progress = new Progress, no_build: Boolean = false ): Int = { Build.build(session_options(options), selection = Sessions.Selection.session(PIDE.resources.session_base.session_name), progress = progress, build_heap = true, no_build = no_build, dirs = session_dirs, infos = PIDE.resources.session_base_info.infos).rc } def session_start(options0: Options): Unit = { val session = PIDE.session val options = session_options(options0) val sessions_structure = PIDE.resources.session_base_info.sessions_structure val store = Sessions.store(options) session.phase_changed += PIDE.plugin.session_phase_changed Isabelle_Process.start(session, options, sessions_structure, store, logic = PIDE.resources.session_base.session_name, modes = (space_explode(',', options.string("jedit_print_mode")) ::: space_explode(',', Isabelle_System.getenv("JEDIT_PRINT_MODE"))).reverse) } }