# HG changeset patch # User wenzelm # Date 1509468988 -3600 # Node ID 1c3d0c12bb5192333cab7c0ba521f413e79c301e # Parent e1bde71bace6720936488a566ba3a1a6f3eb3c04 clarified signature; diff -r e1bde71bace6 -r 1c3d0c12bb51 src/Pure/ML/ml_console.scala --- a/src/Pure/ML/ml_console.scala Tue Oct 31 17:15:49 2017 +0100 +++ b/src/Pure/ML/ml_console.scala Tue Oct 31 17:56:28 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(options, logic, dirs))) + else Some(Sessions.session_base_info(options, logic, dirs).check)) val process_output = Future.thread[Unit]("process_output") { try { var result = new StringBuilder(100) diff -r e1bde71bace6 -r 1c3d0c12bb51 src/Pure/Thy/sessions.scala --- a/src/Pure/Thy/sessions.scala Tue Oct 31 17:15:49 2017 +0100 +++ b/src/Pure/Thy/sessions.scala Tue Oct 31 17:56:28 2017 +0100 @@ -318,34 +318,33 @@ Deps(session_bases, Known.make(Path.current, session_bases.toList.map(_._2))) } - def session_base_errors( + + /* 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, dirs: List[Path] = Nil, inlined_files: Boolean = false, - all_known: Boolean = false): (List[String], Base) = + all_known: Boolean = false): Base_Info = { val full_sessions = load(options, dirs = dirs) val global_theories = full_sessions.global_theories val (_, selected_sessions) = full_sessions.selection(Selection(sessions = List(session))) - 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) - (deps.errors, base) - } + val deps = + Sessions.deps(if (all_known) full_sessions else selected_sessions, + global_theories, inlined_files = inlined_files) - def session_base( - options: Options, - session: String, - dirs: List[Path] = Nil, - inlined_files: Boolean = false, - all_known: Boolean = false): Base = - { - val (errs, base) = - session_base_errors(options, session, dirs = dirs, - inlined_files = inlined_files, all_known = all_known) - if (errs.isEmpty) base else error(cat_lines(errs)) + val base = if (all_known) deps(session).copy(known = deps.all_known) else deps(session) + + Base_Info(base, deps.errors) } diff -r e1bde71bace6 -r 1c3d0c12bb51 src/Tools/VSCode/src/build_vscode.scala --- a/src/Tools/VSCode/src/build_vscode.scala Tue Oct 31 17:15:49 2017 +0100 +++ b/src/Tools/VSCode/src/build_vscode.scala Tue Oct 31 17:56:28 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(options, logic).overall_syntax.keywords + val keywords = Sessions.session_base_info(options, logic).check.overall_syntax.keywords val output_path = extension_dir + Path.explode(Grammar.default_output(logic)) progress.echo(output_path.implode) diff -r e1bde71bace6 -r 1c3d0c12bb51 src/Tools/VSCode/src/grammar.scala --- a/src/Tools/VSCode/src/grammar.scala Tue Oct 31 17:15:49 2017 +0100 +++ b/src/Tools/VSCode/src/grammar.scala Tue Oct 31 17:56:28 2017 +0100 @@ -157,7 +157,8 @@ val more_args = getopts(args) if (more_args.nonEmpty) getopts.usage() - val keywords = Sessions.session_base(Options.init(), logic, dirs).overall_syntax.keywords + val keywords = + Sessions.session_base_info(Options.init(), logic, dirs).check.overall_syntax.keywords val output_path = output getOrElse Path.explode(default_output(logic)) Output.writeln(output_path.implode) diff -r e1bde71bace6 -r 1c3d0c12bb51 src/Tools/VSCode/src/server.scala --- a/src/Tools/VSCode/src/server.scala Tue Oct 31 17:15:49 2017 +0100 +++ b/src/Tools/VSCode/src/server.scala Tue Oct 31 17:56:28 2017 +0100 @@ -269,7 +269,8 @@ } val session_base = - Sessions.session_base(options, session_name, dirs = session_dirs, all_known = all_known) + Sessions.session_base_info( + options, session_name, dirs = session_dirs, all_known = all_known).check val resources = new VSCode_Resources(options, session_base, log) { override def commit(change: Session.Change): Unit = diff -r e1bde71bace6 -r 1c3d0c12bb51 src/Tools/jEdit/src/jedit_resources.scala --- a/src/Tools/jEdit/src/jedit_resources.scala Tue Oct 31 17:15:49 2017 +0100 +++ b/src/Tools/jEdit/src/jedit_resources.scala Tue Oct 31 17:56:28 2017 +0100 @@ -24,15 +24,15 @@ object JEdit_Resources { def apply(options: Options): JEdit_Resources = - { - val (errs, base) = JEdit_Sessions.session_base(options) - new JEdit_Resources(errs, base) - } + new JEdit_Resources(JEdit_Sessions.session_base_info(options)) } -class JEdit_Resources private(val session_errors: List[String], session_base: Sessions.Base) - extends Resources(session_base) +class JEdit_Resources private(session_base_info: Sessions.Base_Info) + extends Resources(session_base_info.base) { + def session_errors: List[String] = session_base_info.errors + + /* document node name */ def known_file(path: String): Option[Document.Node.Name] = diff -r e1bde71bace6 -r 1c3d0c12bb51 src/Tools/jEdit/src/jedit_sessions.scala --- a/src/Tools/jEdit/src/jedit_sessions.scala Tue Oct 31 17:15:49 2017 +0100 +++ b/src/Tools/jEdit/src/jedit_sessions.scala Tue Oct 31 17:56:28 2017 +0100 @@ -49,12 +49,12 @@ def session_name(options: Options): String = session_info(options).name - def session_base(options: Options): (List[String], Sessions.Base) = + def session_base_info(options: Options): Sessions.Base_Info = { - val (errs, base) = - Sessions.session_base_errors( - options, session_name(options), dirs = JEdit_Sessions.session_dirs(), all_known = true) - (errs, base.platform_path) + Sessions.session_base_info(options, + session_name(options), + dirs = JEdit_Sessions.session_dirs(), + all_known = true).platform_path } def session_build_mode(): String = Isabelle_System.getenv("JEDIT_BUILD_MODE")