# 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,