proper session dirs for "isabelle jedit" and "isabelle console" with options -d and -l;
--- a/src/Pure/System/isabelle_process.scala Tue Mar 29 22:22:12 2016 +0200
+++ b/src/Pure/System/isabelle_process.scala Tue Mar 29 23:41:28 2016 +0200
@@ -13,6 +13,7 @@
options: Options,
logic: String = "",
args: List[String] = Nil,
+ dirs: List[Path] = Nil,
modes: List[String] = Nil,
receiver: Prover.Receiver = Console.println(_),
store: Sessions.Store = Sessions.store()): Isabelle_Process =
@@ -20,8 +21,8 @@
val channel = System_Channel()
val process =
try {
- ML_Process(options, logic = logic, args = args, modes = modes, store = store,
- channel = Some(channel))
+ ML_Process(options, logic = logic, args = args, dirs = dirs,
+ modes = modes, store = store, channel = Some(channel))
}
catch { case exn @ ERROR(_) => channel.accepted(); throw exn }
process.stdin.close
--- a/src/Pure/Tools/ml_console.scala Tue Mar 29 22:22:12 2016 +0200
+++ b/src/Pure/Tools/ml_console.scala Tue Mar 29 23:41:28 2016 +0200
@@ -70,7 +70,7 @@
// process loop
val process =
- ML_Process(options, logic = logic, args = List("-i"),
+ ML_Process(options, logic = logic, args = List("-i"), dirs = dirs,
modes = if (raw_ml_system) Nil else modes ::: List("ASCII"),
raw_ml_system = raw_ml_system, store = Sessions.store(system_mode))
val process_output = Future.thread[Unit]("process_output") {
--- a/src/Tools/jEdit/src/isabelle_logic.scala Tue Mar 29 22:22:12 2016 +0200
+++ b/src/Tools/jEdit/src/isabelle_logic.scala Tue Mar 29 23:41:28 2016 +0200
@@ -75,8 +75,8 @@
(space_explode(',', PIDE.options.string("jedit_print_mode")) :::
space_explode(',', Isabelle_System.getenv("JEDIT_PRINT_MODE"))).reverse
PIDE.session.start(receiver =>
- Isabelle_Process(
- PIDE.options.value, logic = session_name(), modes = modes, receiver = receiver,
+ Isabelle_Process(PIDE.options.value, logic = session_name(), dirs = session_dirs(),
+ modes = modes, receiver = receiver,
store = Sessions.store(session_build_mode() == "system")))
}