# HG changeset patch
# User wenzelm
# Date 1489417140 -3600
# Node ID 8cfdf420b64317e243bf0cf7c176e551e3d92fb8
# Parent  eb89ad5ae115fed5f7cab97a9d83f7573eb03135
tuned signature;

diff -r eb89ad5ae115 -r 8cfdf420b643 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Mon Mar 13 15:32:19 2017 +0100
+++ b/src/Pure/Tools/build.scala	Mon Mar 13 15:59:00 2017 +0100
@@ -211,16 +211,13 @@
 
   def session_base(
     options: Options,
-    inlined_files: Boolean,
-    dirs: List[Path],
-    session: String): Sessions.Base =
+    session_name: String,
+    session_dirs: List[Path] = Nil,
+    inlined_files: Boolean = false): Sessions.Base =
   {
-    session_dependencies(options, inlined_files, dirs, List(session))(session)
+    session_dependencies(options, inlined_files, session_dirs, List(session_name))(session_name)
   }
 
-  def outer_syntax(options: Options, dirs: List[Path], session: String): Outer_Syntax =
-    session_base(options, false, dirs, session).syntax
-
 
   /* jobs */
 
diff -r eb89ad5ae115 -r 8cfdf420b643 src/Tools/VSCode/src/build_vscode.scala
--- a/src/Tools/VSCode/src/build_vscode.scala	Mon Mar 13 15:32:19 2017 +0100
+++ b/src/Tools/VSCode/src/build_vscode.scala	Mon Mar 13 15:59:00 2017 +0100
@@ -49,7 +49,7 @@
   def build_grammar(options: Options, progress: Progress = No_Progress)
   {
     val logic = Grammar.default_logic
-    val keywords = Build.outer_syntax(options, Nil, logic).keywords
+    val keywords = Build.session_base(options, logic).syntax.keywords
 
     val output_path = extension_dir + Path.explode(Grammar.default_output(logic))
     progress.echo(output_path.implode)
diff -r eb89ad5ae115 -r 8cfdf420b643 src/Tools/VSCode/src/grammar.scala
--- a/src/Tools/VSCode/src/grammar.scala	Mon Mar 13 15:32:19 2017 +0100
+++ b/src/Tools/VSCode/src/grammar.scala	Mon Mar 13 15:59:00 2017 +0100
@@ -159,7 +159,7 @@
     val more_args = getopts(args)
     if (more_args.nonEmpty) getopts.usage()
 
-    val keywords = Build.outer_syntax(Options.init(), dirs, logic).keywords
+    val keywords = Build.session_base(Options.init(), logic, dirs).syntax.keywords
     val output_path = output getOrElse Path.explode(default_output(logic))
 
     Output.writeln(output_path.implode)
diff -r eb89ad5ae115 -r 8cfdf420b643 src/Tools/VSCode/src/server.scala
--- a/src/Tools/VSCode/src/server.scala	Mon Mar 13 15:32:19 2017 +0100
+++ b/src/Tools/VSCode/src/server.scala	Mon Mar 13 15:59:00 2017 +0100
@@ -212,7 +212,7 @@
           }
         }
 
-        val base = Build.session_base(options, false, session_dirs, session_name)
+        val base = Build.session_base(options, session_name, session_dirs)
         val resources = new VSCode_Resources(options, base, log)
           {
             override def commit(change: Session.Change): Unit =
diff -r eb89ad5ae115 -r 8cfdf420b643 src/Tools/jEdit/src/jedit_sessions.scala
--- a/src/Tools/jEdit/src/jedit_sessions.scala	Mon Mar 13 15:32:19 2017 +0100
+++ b/src/Tools/jEdit/src/jedit_sessions.scala	Mon Mar 13 15:59:00 2017 +0100
@@ -79,10 +79,10 @@
     main_sessions.map(_._1).sorted ::: other_sessions.map(_._1).sorted
   }
 
-  def session_base(inlined_files: Boolean): Sessions.Base =
+  def session_base(): Sessions.Base =
   {
     val base =
-      try { Build.session_base(PIDE.options.value, inlined_files, session_dirs(), session_name()) }
+      try { Build.session_base(PIDE.options.value, session_name(), session_dirs()) }
       catch { case ERROR(_) => Sessions.Base.empty }
     base.copy(known_theories = base.known_theories.mapValues(a => a.map(File.platform_path(_))))
   }
diff -r eb89ad5ae115 -r 8cfdf420b643 src/Tools/jEdit/src/plugin.scala
--- a/src/Tools/jEdit/src/plugin.scala	Mon Mar 13 15:32:19 2017 +0100
+++ b/src/Tools/jEdit/src/plugin.scala	Mon Mar 13 15:59:00 2017 +0100
@@ -389,7 +389,7 @@
 
       JEdit_Lib.jedit_text_areas.foreach(Completion_Popup.Text_Area.init _)
 
-      val resources = new JEdit_Resources(JEdit_Sessions.session_base(false))
+      val resources = new JEdit_Resources(JEdit_Sessions.session_base())
 
       PIDE.session.stop()
       PIDE.session = new Session(resources) {