# HG changeset patch # User wenzelm # Date 1509551031 -3600 # Node ID 806bc39550a5df6277f03c26282cb128eec7dfff # Parent ca73d44d51aaeae2458d96601de9cbfd54dbe094 tuned signature; diff -r ca73d44d51aa -r 806bc39550a5 src/Pure/ML/ml_console.scala --- a/src/Pure/ML/ml_console.scala Wed Nov 01 16:38:15 2017 +0100 +++ b/src/Pure/ML/ml_console.scala Wed Nov 01 16:43:51 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.session_base_info(options, logic, dirs).check_base)) + else Some(Sessions.base_info(options, logic, dirs).check_base)) val process_output = Future.thread[Unit]("process_output") { try { var result = new StringBuilder(100) diff -r ca73d44d51aa -r 806bc39550a5 src/Pure/Thy/sessions.scala --- a/src/Pure/Thy/sessions.scala Wed Nov 01 16:38:15 2017 +0100 +++ b/src/Pure/Thy/sessions.scala Wed Nov 01 16:43:51 2017 +0100 @@ -335,9 +335,7 @@ def check_base: Base = if (errors.isEmpty) base else error(cat_lines(errors)) } - def session_base_info( - options: Options, - session: String, + def base_info(options: Options, session: String, dirs: List[Path] = Nil, all_known: Boolean = false, required_session: Boolean = false): Base_Info = diff -r ca73d44d51aa -r 806bc39550a5 src/Tools/VSCode/src/build_vscode.scala --- a/src/Tools/VSCode/src/build_vscode.scala Wed Nov 01 16:38:15 2017 +0100 +++ b/src/Tools/VSCode/src/build_vscode.scala Wed Nov 01 16:43:51 2017 +0100 @@ -20,7 +20,7 @@ def build_grammar(options: Options, progress: Progress = No_Progress) { val logic = Grammar.default_logic - val keywords = Sessions.session_base_info(options, logic).check_base.overall_syntax.keywords + val keywords = Sessions.base_info(options, logic).check_base.overall_syntax.keywords val output_path = extension_dir + Path.explode(Grammar.default_output(logic)) progress.echo(output_path.implode) diff -r ca73d44d51aa -r 806bc39550a5 src/Tools/VSCode/src/grammar.scala --- a/src/Tools/VSCode/src/grammar.scala Wed Nov 01 16:38:15 2017 +0100 +++ b/src/Tools/VSCode/src/grammar.scala Wed Nov 01 16:43:51 2017 +0100 @@ -158,7 +158,7 @@ if (more_args.nonEmpty) getopts.usage() val keywords = - Sessions.session_base_info(Options.init(), logic, dirs).check_base.overall_syntax.keywords + Sessions.base_info(Options.init(), logic, dirs).check_base.overall_syntax.keywords val output_path = output getOrElse Path.explode(default_output(logic)) Output.writeln(output_path.implode) diff -r ca73d44d51aa -r 806bc39550a5 src/Tools/VSCode/src/server.scala --- a/src/Tools/VSCode/src/server.scala Wed Nov 01 16:38:15 2017 +0100 +++ b/src/Tools/VSCode/src/server.scala Wed Nov 01 16:43:51 2017 +0100 @@ -269,7 +269,7 @@ } val session_base = - Sessions.session_base_info( + Sessions.base_info( options, session_name, dirs = session_dirs, all_known = all_known).check_base val resources = new VSCode_Resources(options, session_base, log) { diff -r ca73d44d51aa -r 806bc39550a5 src/Tools/jEdit/src/jedit_sessions.scala --- a/src/Tools/jEdit/src/jedit_sessions.scala Wed Nov 01 16:38:15 2017 +0100 +++ b/src/Tools/jEdit/src/jedit_sessions.scala Wed Nov 01 16:43:51 2017 +0100 @@ -59,7 +59,7 @@ { val logic = logic_name(options) - Sessions.session_base_info(options, + Sessions.base_info(options, if (logic_parent) logic_info(options).flatMap(_.parent) getOrElse logic else logic, dirs = JEdit_Sessions.session_dirs(), all_known = true,