--- a/src/Pure/ML/ml_console.scala Tue Oct 31 17:56:28 2017 +0100
+++ b/src/Pure/ML/ml_console.scala Tue Oct 31 18:45:33 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))
+ else Some(Sessions.session_base_info(options, logic, dirs).check_base))
val process_output = Future.thread[Unit]("process_output") {
try {
var result = new StringBuilder(100)
--- a/src/Pure/Thy/sessions.scala Tue Oct 31 17:56:28 2017 +0100
+++ b/src/Pure/Thy/sessions.scala Tue Oct 31 18:45:33 2017 +0100
@@ -321,12 +321,6 @@
/* base info */
- sealed case class Base_Info(base: Base, errors: List[String])
- {
- def platform_path: Base_Info = copy(base = base.platform_path)
- def check: Base = if (errors.isEmpty) base else error(cat_lines(errors))
- }
-
def session_base_info(
options: Options,
session: String,
@@ -338,13 +332,19 @@
val global_theories = full_sessions.global_theories
val (_, selected_sessions) = full_sessions.selection(Selection(sessions = List(session)))
- val deps =
- Sessions.deps(if (all_known) full_sessions else selected_sessions,
- global_theories, inlined_files = inlined_files)
-
+ val sessions: T = if (all_known) full_sessions else selected_sessions
+ val deps = Sessions.deps(sessions, global_theories, inlined_files = inlined_files)
val base = if (all_known) deps(session).copy(known = deps.all_known) else deps(session)
- Base_Info(base, deps.errors)
+ new Base_Info(sessions, deps, base)
+ }
+
+ final class Base_Info private [Sessions](val sessions: T, val deps: Deps, val base: Base)
+ {
+ def platform_path: Base_Info = new Base_Info(sessions, deps, base.platform_path)
+
+ def errors: List[String] = deps.errors
+ def check_base: Base = if (errors.isEmpty) base else error(cat_lines(errors))
}
--- a/src/Tools/VSCode/src/build_vscode.scala Tue Oct 31 17:56:28 2017 +0100
+++ b/src/Tools/VSCode/src/build_vscode.scala Tue Oct 31 18:45:33 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.overall_syntax.keywords
+ val keywords = Sessions.session_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)
--- a/src/Tools/VSCode/src/grammar.scala Tue Oct 31 17:56:28 2017 +0100
+++ b/src/Tools/VSCode/src/grammar.scala Tue Oct 31 18:45:33 2017 +0100
@@ -158,7 +158,7 @@
if (more_args.nonEmpty) getopts.usage()
val keywords =
- Sessions.session_base_info(Options.init(), logic, dirs).check.overall_syntax.keywords
+ Sessions.session_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)
--- a/src/Tools/VSCode/src/server.scala Tue Oct 31 17:56:28 2017 +0100
+++ b/src/Tools/VSCode/src/server.scala Tue Oct 31 18:45:33 2017 +0100
@@ -270,7 +270,7 @@
val session_base =
Sessions.session_base_info(
- options, session_name, dirs = session_dirs, all_known = all_known).check
+ options, session_name, dirs = session_dirs, all_known = all_known).check_base
val resources = new VSCode_Resources(options, session_base, log)
{
override def commit(change: Session.Change): Unit =