clarified signature;
authorwenzelm
Tue Oct 31 18:45:33 2017 +0100 (18 months ago)
changeset 669649f2de457b95e
parent 66963 1c3d0c12bb51
child 66965 9cec50354099
clarified signature;
src/Pure/ML/ml_console.scala
src/Pure/Thy/sessions.scala
src/Tools/VSCode/src/build_vscode.scala
src/Tools/VSCode/src/grammar.scala
src/Tools/VSCode/src/server.scala
     1.1 --- a/src/Pure/ML/ml_console.scala	Tue Oct 31 17:56:28 2017 +0100
     1.2 +++ b/src/Pure/ML/ml_console.scala	Tue Oct 31 18:45:33 2017 +0100
     1.3 @@ -75,7 +75,7 @@
     1.4            raw_ml_system = raw_ml_system, store = Sessions.store(system_mode),
     1.5            session_base =
     1.6              if (raw_ml_system) None
     1.7 -            else Some(Sessions.session_base_info(options, logic, dirs).check))
     1.8 +            else Some(Sessions.session_base_info(options, logic, dirs).check_base))
     1.9        val process_output = Future.thread[Unit]("process_output") {
    1.10          try {
    1.11            var result = new StringBuilder(100)
     2.1 --- a/src/Pure/Thy/sessions.scala	Tue Oct 31 17:56:28 2017 +0100
     2.2 +++ b/src/Pure/Thy/sessions.scala	Tue Oct 31 18:45:33 2017 +0100
     2.3 @@ -321,12 +321,6 @@
     2.4  
     2.5    /* base info */
     2.6  
     2.7 -  sealed case class Base_Info(base: Base, errors: List[String])
     2.8 -  {
     2.9 -    def platform_path: Base_Info = copy(base = base.platform_path)
    2.10 -    def check: Base = if (errors.isEmpty) base else error(cat_lines(errors))
    2.11 -  }
    2.12 -
    2.13    def session_base_info(
    2.14      options: Options,
    2.15      session: String,
    2.16 @@ -338,13 +332,19 @@
    2.17      val global_theories = full_sessions.global_theories
    2.18      val (_, selected_sessions) = full_sessions.selection(Selection(sessions = List(session)))
    2.19  
    2.20 -    val deps =
    2.21 -      Sessions.deps(if (all_known) full_sessions else selected_sessions,
    2.22 -        global_theories, inlined_files = inlined_files)
    2.23 -
    2.24 +    val sessions: T = if (all_known) full_sessions else selected_sessions
    2.25 +    val deps = Sessions.deps(sessions, global_theories, inlined_files = inlined_files)
    2.26      val base = if (all_known) deps(session).copy(known = deps.all_known) else deps(session)
    2.27  
    2.28 -    Base_Info(base, deps.errors)
    2.29 +    new Base_Info(sessions, deps, base)
    2.30 +  }
    2.31 +
    2.32 +  final class Base_Info private [Sessions](val sessions: T, val deps: Deps, val base: Base)
    2.33 +  {
    2.34 +    def platform_path: Base_Info = new Base_Info(sessions, deps, base.platform_path)
    2.35 +
    2.36 +    def errors: List[String] = deps.errors
    2.37 +    def check_base: Base = if (errors.isEmpty) base else error(cat_lines(errors))
    2.38    }
    2.39  
    2.40  
     3.1 --- a/src/Tools/VSCode/src/build_vscode.scala	Tue Oct 31 17:56:28 2017 +0100
     3.2 +++ b/src/Tools/VSCode/src/build_vscode.scala	Tue Oct 31 18:45:33 2017 +0100
     3.3 @@ -20,7 +20,7 @@
     3.4    def build_grammar(options: Options, progress: Progress = No_Progress)
     3.5    {
     3.6      val logic = Grammar.default_logic
     3.7 -    val keywords = Sessions.session_base_info(options, logic).check.overall_syntax.keywords
     3.8 +    val keywords = Sessions.session_base_info(options, logic).check_base.overall_syntax.keywords
     3.9  
    3.10      val output_path = extension_dir + Path.explode(Grammar.default_output(logic))
    3.11      progress.echo(output_path.implode)
     4.1 --- a/src/Tools/VSCode/src/grammar.scala	Tue Oct 31 17:56:28 2017 +0100
     4.2 +++ b/src/Tools/VSCode/src/grammar.scala	Tue Oct 31 18:45:33 2017 +0100
     4.3 @@ -158,7 +158,7 @@
     4.4      if (more_args.nonEmpty) getopts.usage()
     4.5  
     4.6      val keywords =
     4.7 -      Sessions.session_base_info(Options.init(), logic, dirs).check.overall_syntax.keywords
     4.8 +      Sessions.session_base_info(Options.init(), logic, dirs).check_base.overall_syntax.keywords
     4.9      val output_path = output getOrElse Path.explode(default_output(logic))
    4.10  
    4.11      Output.writeln(output_path.implode)
     5.1 --- a/src/Tools/VSCode/src/server.scala	Tue Oct 31 17:56:28 2017 +0100
     5.2 +++ b/src/Tools/VSCode/src/server.scala	Tue Oct 31 18:45:33 2017 +0100
     5.3 @@ -270,7 +270,7 @@
     5.4  
     5.5          val session_base =
     5.6            Sessions.session_base_info(
     5.7 -            options, session_name, dirs = session_dirs, all_known = all_known).check
     5.8 +            options, session_name, dirs = session_dirs, all_known = all_known).check_base
     5.9          val resources = new VSCode_Resources(options, session_base, log)
    5.10            {
    5.11              override def commit(change: Session.Change): Unit =