--- a/src/Tools/jEdit/src/isabelle_options.scala Wed Mar 15 11:07:07 2017 +0100
+++ b/src/Tools/jEdit/src/isabelle_options.scala Wed Mar 15 12:41:22 2017 +0100
@@ -42,7 +42,8 @@
val options = PIDE.options
private val predefined =
- List(JEdit_Sessions.logic_selector(false), JEdit_Spell_Checker.dictionaries_selector())
+ List(JEdit_Sessions.logic_selector(options.value, false),
+ JEdit_Spell_Checker.dictionaries_selector())
protected val components =
options.make_components(predefined,
--- a/src/Tools/jEdit/src/jedit_sessions.scala Wed Mar 15 11:07:07 2017 +0100
+++ b/src/Tools/jEdit/src/jedit_sessions.scala Wed Mar 15 12:41:22 2017 +0100
@@ -1,7 +1,8 @@
/* Title: Tools/jEdit/src/jedit_sessions.scala
Author: Makarius
-Isabelle/jEdit session information.
+Isabelle/jEdit session information, based on implicit process environment
+and explicit options.
*/
package isabelle.jedit
@@ -23,22 +24,22 @@
def session_dirs(): List[Path] = Path.split(Isabelle_System.getenv("JEDIT_SESSION_DIRS"))
- def session_options(): Options =
+ def session_options(options: Options): Options =
Isabelle_System.getenv("JEDIT_ML_PROCESS_POLICY") match {
- case "" => PIDE.options.value
- case s => PIDE.options.value.string("ML_process_policy") = s
+ case "" => options
+ case s => options.string("ML_process_policy") = s
}
- def session_info(): Info =
+ def session_info(options: Options): Info =
{
val logic =
Isabelle_System.default_logic(
Isabelle_System.getenv("JEDIT_LOGIC"),
- PIDE.options.string(option_name))
+ options.string(option_name))
(for {
tree <-
- try { Some(Sessions.load(session_options(), dirs = session_dirs())) }
+ try { Some(Sessions.load(session_options(options), dirs = session_dirs())) }
catch { case ERROR(_) => None }
info <- tree.lift(logic)
parent <- info.parent
@@ -46,44 +47,45 @@
} yield Info(parent, info.pos)) getOrElse Info(logic, Position.none)
}
- def session_name(): String = session_info().name
+ def session_name(options: Options): String = session_info(options).name
def session_build_mode(): String = Isabelle_System.getenv("JEDIT_BUILD_MODE")
- def session_build(progress: Progress = No_Progress, no_build: Boolean = false): Int =
+ def session_build(
+ options: Options, progress: Progress = No_Progress, no_build: Boolean = false): Int =
{
val mode = session_build_mode()
- Build.build(options = session_options(), progress = progress,
+ Build.build(options = session_options(options), progress = progress,
build_heap = true, no_build = no_build, system_mode = mode == "" || mode == "system",
- dirs = session_dirs(), sessions = List(session_name())).rc
+ dirs = session_dirs(), sessions = List(session_name(options))).rc
}
- def session_start()
+ def session_start(options: Options)
{
val modes =
- (space_explode(',', PIDE.options.string("jedit_print_mode")) :::
+ (space_explode(',', options.string("jedit_print_mode")) :::
space_explode(',', Isabelle_System.getenv("JEDIT_PRINT_MODE"))).reverse
- Isabelle_Process.start(PIDE.session, session_options(),
- logic = session_name(), dirs = session_dirs(), modes = modes,
+ Isabelle_Process.start(PIDE.session, session_options(options),
+ logic = session_name(options), dirs = session_dirs(), modes = modes,
store = Sessions.store(session_build_mode() == "system"),
phase_changed = PIDE.plugin.session_phase_changed)
}
- def session_list(): List[String] =
+ def session_list(options: Options): List[String] =
{
- val session_tree = Sessions.load(PIDE.options.value, dirs = session_dirs())
+ val session_tree = Sessions.load(options, dirs = session_dirs())
val (main_sessions, other_sessions) =
session_tree.topological_order.partition(p => p._2.groups.contains("main"))
main_sessions.map(_._1).sorted ::: other_sessions.map(_._1).sorted
}
- def session_base(): Sessions.Base =
+ def session_base(options: Options): Sessions.Base =
{
val base =
- try { Sessions.session_base(PIDE.options.value, session_name(), session_dirs()) }
- catch { case ERROR(_) => Sessions.pure_base(PIDE.options.value) }
+ try { Sessions.session_base(options, session_name(options), session_dirs()) }
+ catch { case ERROR(_) => Sessions.pure_base(options) }
base.copy(known_theories =
for ((a, b) <- base.known_theories) yield (a, b.map(File.platform_path(_))))
}
@@ -96,26 +98,26 @@
override def toString: String = description
}
- def logic_selector(autosave: Boolean): Option_Component =
+ def logic_selector(options: Options, autosave: Boolean): Option_Component =
{
GUI_Thread.require {}
val entries =
- new Logic_Entry("", "default (" + session_name() + ")") ::
- session_list().map(name => new Logic_Entry(name, name))
+ new Logic_Entry("", "default (" + session_name(options) + ")") ::
+ session_list(options).map(name => new Logic_Entry(name, name))
val component = new ComboBox(entries) with Option_Component {
name = option_name
val title = "Logic"
def load: Unit =
{
- val logic = PIDE.options.string(option_name)
+ val logic = options.string(option_name)
entries.find(_.name == logic) match {
case Some(entry) => selection.item = entry
case None =>
}
}
- def save: Unit = PIDE.options.string(option_name) = selection.item.name
+ def save: Unit = options.string(option_name) = selection.item.name
}
component.load()
--- a/src/Tools/jEdit/src/plugin.scala Wed Mar 15 11:07:07 2017 +0100
+++ b/src/Tools/jEdit/src/plugin.scala Wed Mar 15 12:41:22 2017 +0100
@@ -302,12 +302,12 @@
val view = jEdit.getActiveView()
- Session_Build.session_build(view)
+ Session_Build.check_dialog(view)
Keymap_Merge.check_dialog(view)
JEdit_Editor.hyperlink_position(true, Document.Snapshot.init,
- JEdit_Sessions.session_info().open_root).foreach(_.follow(view))
+ JEdit_Sessions.session_info(options.value).open_root).foreach(_.follow(view))
case msg: BufferUpdate
if msg.getWhat == BufferUpdate.LOAD_STARTED || msg.getWhat == BufferUpdate.CLOSING =>
@@ -382,7 +382,7 @@
JEdit_Lib.jedit_text_areas.foreach(Completion_Popup.Text_Area.init _)
- val resources = new JEdit_Resources(JEdit_Sessions.session_base())
+ val resources = new JEdit_Resources(JEdit_Sessions.session_base(options.value))
PIDE.session.stop()
PIDE.session = new Session(resources) {
--- a/src/Tools/jEdit/src/session_build.scala Wed Mar 15 11:07:07 2017 +0100
+++ b/src/Tools/jEdit/src/session_build.scala Wed Mar 15 12:41:22 2017 +0100
@@ -21,13 +21,15 @@
object Session_Build
{
- def session_build(view: View)
+ def check_dialog(view: View)
{
GUI_Thread.require {}
+ val options = PIDE.options.value
try {
if (JEdit_Sessions.session_build_mode() == "none" ||
- JEdit_Sessions.session_build(no_build = true) == 0) JEdit_Sessions.session_start()
+ JEdit_Sessions.session_build(options, no_build = true) == 0)
+ JEdit_Sessions.session_start(options)
else new Dialog(view)
}
catch {
@@ -38,6 +40,9 @@
private class Dialog(view: View) extends JDialog(view)
{
+ val options = PIDE.options.value
+
+
/* text */
private val text = new TextArea {
@@ -162,10 +167,10 @@
setVisible(true)
Standard_Thread.fork("session_build") {
- progress.echo("Build started for Isabelle/" + JEdit_Sessions.session_name() + " ...")
+ progress.echo("Build started for Isabelle/" + JEdit_Sessions.session_name(options) + " ...")
val (out, rc) =
- try { ("", JEdit_Sessions.session_build(progress = progress)) }
+ try { ("", JEdit_Sessions.session_build(options, progress = progress)) }
catch {
case exn: Throwable =>
(Output.error_text(Exn.message(exn)) + "\n", Exn.return_code(exn, 2))
@@ -173,7 +178,7 @@
progress.echo(out + (if (rc == 0) "OK\n" else "Return code: " + rc + "\n"))
- if (rc == 0) JEdit_Sessions.session_start()
+ if (rc == 0) JEdit_Sessions.session_start(options)
else progress.echo("Session build failed -- prover process remains inactive!")
return_code(rc)
--- a/src/Tools/jEdit/src/theories_dockable.scala Wed Mar 15 11:07:07 2017 +0100
+++ b/src/Tools/jEdit/src/theories_dockable.scala Wed Mar 15 12:41:22 2017 +0100
@@ -79,7 +79,7 @@
private val continuous_checking = new Isabelle.Continuous_Checking
continuous_checking.focusable = false
- private val logic = JEdit_Sessions.logic_selector(true)
+ private val logic = JEdit_Sessions.logic_selector(PIDE.options.value, true)
private val controls =
new Wrap_Panel(Wrap_Panel.Alignment.Right)(purge, continuous_checking, session_phase, logic)