tuned;
authorwenzelm
Thu Nov 02 11:26:58 2017 +0100 (18 months ago)
changeset 6698925665e7775b7
parent 66988 7f8c1dd7576a
child 66990 b23adab22e67
tuned;
src/Pure/ML/ml_console.scala
src/Tools/VSCode/src/grammar.scala
src/Tools/jEdit/src/jedit_sessions.scala
     1.1 --- a/src/Pure/ML/ml_console.scala	Thu Nov 02 11:25:37 2017 +0100
     1.2 +++ b/src/Pure/ML/ml_console.scala	Thu Nov 02 11:26:58 2017 +0100
     1.3 @@ -75,7 +75,7 @@
     1.4            raw_ml_system = raw_ml_system, store = Sessions.store(system_mode),
     1.5            session_base =
     1.6              if (raw_ml_system) None
     1.7 -            else Some(Sessions.base_info(options, logic, dirs).check_base))
     1.8 +            else Some(Sessions.base_info(options, logic, dirs = dirs).check_base))
     1.9        val process_output = Future.thread[Unit]("process_output") {
    1.10          try {
    1.11            var result = new StringBuilder(100)
     2.1 --- a/src/Tools/VSCode/src/grammar.scala	Thu Nov 02 11:25:37 2017 +0100
     2.2 +++ b/src/Tools/VSCode/src/grammar.scala	Thu Nov 02 11:26:58 2017 +0100
     2.3 @@ -158,7 +158,7 @@
     2.4      if (more_args.nonEmpty) getopts.usage()
     2.5  
     2.6      val keywords =
     2.7 -      Sessions.base_info(Options.init(), logic, dirs).check_base.overall_syntax.keywords
     2.8 +      Sessions.base_info(Options.init(), logic, dirs = dirs).check_base.overall_syntax.keywords
     2.9      val output_path = output getOrElse Path.explode(default_output(logic))
    2.10  
    2.11      Output.writeln(output_path.implode)
     3.1 --- a/src/Tools/jEdit/src/jedit_sessions.scala	Thu Nov 02 11:25:37 2017 +0100
     3.2 +++ b/src/Tools/jEdit/src/jedit_sessions.scala	Thu Nov 02 11:26:58 2017 +0100
     3.3 @@ -106,10 +106,10 @@
     3.4  
     3.5    def session_base_info(options: Options): Sessions.Base_Info =
     3.6      Sessions.base_info(options,
     3.7 +      dirs = JEdit_Sessions.session_dirs(),
     3.8        session =
     3.9          if (logic_parent) logic_info(options).flatMap(_.parent) getOrElse logic_name(options)
    3.10          else logic_name(options),
    3.11 -      dirs = JEdit_Sessions.session_dirs(),
    3.12        ancestor_session = logic_ancestor,
    3.13        all_known = !logic_focus,
    3.14        focus_session = logic_focus,