# HG changeset patch
# User wenzelm
# Date 1509618418 -3600
# Node ID 25665e7775b7e4ba6dbd84e06bff05704c3da0bf
# Parent  7f8c1dd7576a32b4782d3f8163e5440a0a57427f
tuned;

diff -r 7f8c1dd7576a -r 25665e7775b7 src/Pure/ML/ml_console.scala
--- a/src/Pure/ML/ml_console.scala	Thu Nov 02 11:25:37 2017 +0100
+++ b/src/Pure/ML/ml_console.scala	Thu Nov 02 11:26:58 2017 +0100
@@ -75,7 +75,7 @@
           raw_ml_system = raw_ml_system, store = Sessions.store(system_mode),
           session_base =
             if (raw_ml_system) None
-            else Some(Sessions.base_info(options, logic, dirs).check_base))
+            else Some(Sessions.base_info(options, logic, dirs = dirs).check_base))
       val process_output = Future.thread[Unit]("process_output") {
         try {
           var result = new StringBuilder(100)
diff -r 7f8c1dd7576a -r 25665e7775b7 src/Tools/VSCode/src/grammar.scala
--- a/src/Tools/VSCode/src/grammar.scala	Thu Nov 02 11:25:37 2017 +0100
+++ b/src/Tools/VSCode/src/grammar.scala	Thu Nov 02 11:26:58 2017 +0100
@@ -158,7 +158,7 @@
     if (more_args.nonEmpty) getopts.usage()
 
     val keywords =
-      Sessions.base_info(Options.init(), logic, dirs).check_base.overall_syntax.keywords
+      Sessions.base_info(Options.init(), logic, dirs = dirs).check_base.overall_syntax.keywords
     val output_path = output getOrElse Path.explode(default_output(logic))
 
     Output.writeln(output_path.implode)
diff -r 7f8c1dd7576a -r 25665e7775b7 src/Tools/jEdit/src/jedit_sessions.scala
--- a/src/Tools/jEdit/src/jedit_sessions.scala	Thu Nov 02 11:25:37 2017 +0100
+++ b/src/Tools/jEdit/src/jedit_sessions.scala	Thu Nov 02 11:26:58 2017 +0100
@@ -106,10 +106,10 @@
 
   def session_base_info(options: Options): Sessions.Base_Info =
     Sessions.base_info(options,
+      dirs = JEdit_Sessions.session_dirs(),
       session =
         if (logic_parent) logic_info(options).flatMap(_.parent) getOrElse logic_name(options)
         else logic_name(options),
-      dirs = JEdit_Sessions.session_dirs(),
       ancestor_session = logic_ancestor,
       all_known = !logic_focus,
       focus_session = logic_focus,