# HG changeset patch
# User wenzelm
# Date 1459287688 -7200
# Node ID c35012b86e6f7fceb0912cf3af416455e6b55cc3
# Parent  76b814ccce619e06b6a9ecef35a68aee9124f17d
proper session dirs for "isabelle jedit" and "isabelle console" with options -d and -l;

diff -r 76b814ccce61 -r c35012b86e6f src/Pure/System/isabelle_process.scala
--- 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
diff -r 76b814ccce61 -r c35012b86e6f src/Pure/Tools/ml_console.scala
--- 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") {
diff -r 76b814ccce61 -r c35012b86e6f src/Tools/jEdit/src/isabelle_logic.scala
--- 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")))
   }