--- 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 */
--- 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)
--- 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)
--- 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 =
--- 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(_))))
}
--- 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) {