clarified signature;
authorwenzelm
Tue Oct 31 17:56:28 2017 +0100 (18 months ago)
changeset 669631c3d0c12bb51
parent 66962 e1bde71bace6
child 66964 9f2de457b95e
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
src/Tools/jEdit/src/jedit_resources.scala
src/Tools/jEdit/src/jedit_sessions.scala
     1.1 --- a/src/Pure/ML/ml_console.scala	Tue Oct 31 17:15:49 2017 +0100
     1.2 +++ b/src/Pure/ML/ml_console.scala	Tue Oct 31 17:56:28 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(options, logic, dirs)))
     1.8 +            else Some(Sessions.session_base_info(options, logic, dirs).check))
     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:15:49 2017 +0100
     2.2 +++ b/src/Pure/Thy/sessions.scala	Tue Oct 31 17:56:28 2017 +0100
     2.3 @@ -318,34 +318,33 @@
     2.4      Deps(session_bases, Known.make(Path.current, session_bases.toList.map(_._2)))
     2.5    }
     2.6  
     2.7 -  def session_base_errors(
     2.8 +
     2.9 +  /* base info */
    2.10 +
    2.11 +  sealed case class Base_Info(base: Base, errors: List[String])
    2.12 +  {
    2.13 +    def platform_path: Base_Info = copy(base = base.platform_path)
    2.14 +    def check: Base = if (errors.isEmpty) base else error(cat_lines(errors))
    2.15 +  }
    2.16 +
    2.17 +  def session_base_info(
    2.18      options: Options,
    2.19      session: String,
    2.20      dirs: List[Path] = Nil,
    2.21      inlined_files: Boolean = false,
    2.22 -    all_known: Boolean = false): (List[String], Base) =
    2.23 +    all_known: Boolean = false): Base_Info =
    2.24    {
    2.25      val full_sessions = load(options, dirs = dirs)
    2.26      val global_theories = full_sessions.global_theories
    2.27      val (_, selected_sessions) = full_sessions.selection(Selection(sessions = List(session)))
    2.28  
    2.29 -    val sessions: T = if (all_known) full_sessions else selected_sessions
    2.30 -    val deps = Sessions.deps(sessions, global_theories, inlined_files = inlined_files)
    2.31 -    val base = if (all_known) deps(session).copy(known = deps.all_known) else deps(session)
    2.32 -    (deps.errors, base)
    2.33 -  }
    2.34 +    val deps =
    2.35 +      Sessions.deps(if (all_known) full_sessions else selected_sessions,
    2.36 +        global_theories, inlined_files = inlined_files)
    2.37  
    2.38 -  def session_base(
    2.39 -    options: Options,
    2.40 -    session: String,
    2.41 -    dirs: List[Path] = Nil,
    2.42 -    inlined_files: Boolean = false,
    2.43 -    all_known: Boolean = false): Base =
    2.44 -  {
    2.45 -    val (errs, base) =
    2.46 -      session_base_errors(options, session, dirs = dirs,
    2.47 -        inlined_files = inlined_files, all_known = all_known)
    2.48 -    if (errs.isEmpty) base else error(cat_lines(errs))
    2.49 +    val base = if (all_known) deps(session).copy(known = deps.all_known) else deps(session)
    2.50 +
    2.51 +    Base_Info(base, deps.errors)
    2.52    }
    2.53  
    2.54  
     3.1 --- a/src/Tools/VSCode/src/build_vscode.scala	Tue Oct 31 17:15:49 2017 +0100
     3.2 +++ b/src/Tools/VSCode/src/build_vscode.scala	Tue Oct 31 17:56:28 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(options, logic).overall_syntax.keywords
     3.8 +    val keywords = Sessions.session_base_info(options, logic).check.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:15:49 2017 +0100
     4.2 +++ b/src/Tools/VSCode/src/grammar.scala	Tue Oct 31 17:56:28 2017 +0100
     4.3 @@ -157,7 +157,8 @@
     4.4      val more_args = getopts(args)
     4.5      if (more_args.nonEmpty) getopts.usage()
     4.6  
     4.7 -    val keywords = Sessions.session_base(Options.init(), logic, dirs).overall_syntax.keywords
     4.8 +    val keywords =
     4.9 +      Sessions.session_base_info(Options.init(), logic, dirs).check.overall_syntax.keywords
    4.10      val output_path = output getOrElse Path.explode(default_output(logic))
    4.11  
    4.12      Output.writeln(output_path.implode)
     5.1 --- a/src/Tools/VSCode/src/server.scala	Tue Oct 31 17:15:49 2017 +0100
     5.2 +++ b/src/Tools/VSCode/src/server.scala	Tue Oct 31 17:56:28 2017 +0100
     5.3 @@ -269,7 +269,8 @@
     5.4          }
     5.5  
     5.6          val session_base =
     5.7 -          Sessions.session_base(options, session_name, dirs = session_dirs, all_known = all_known)
     5.8 +          Sessions.session_base_info(
     5.9 +            options, session_name, dirs = session_dirs, all_known = all_known).check
    5.10          val resources = new VSCode_Resources(options, session_base, log)
    5.11            {
    5.12              override def commit(change: Session.Change): Unit =
     6.1 --- a/src/Tools/jEdit/src/jedit_resources.scala	Tue Oct 31 17:15:49 2017 +0100
     6.2 +++ b/src/Tools/jEdit/src/jedit_resources.scala	Tue Oct 31 17:56:28 2017 +0100
     6.3 @@ -24,15 +24,15 @@
     6.4  object JEdit_Resources
     6.5  {
     6.6    def apply(options: Options): JEdit_Resources =
     6.7 -  {
     6.8 -    val (errs, base) = JEdit_Sessions.session_base(options)
     6.9 -    new JEdit_Resources(errs, base)
    6.10 -  }
    6.11 +    new JEdit_Resources(JEdit_Sessions.session_base_info(options))
    6.12  }
    6.13  
    6.14 -class JEdit_Resources private(val session_errors: List[String], session_base: Sessions.Base)
    6.15 -  extends Resources(session_base)
    6.16 +class JEdit_Resources private(session_base_info: Sessions.Base_Info)
    6.17 +  extends Resources(session_base_info.base)
    6.18  {
    6.19 +  def session_errors: List[String] = session_base_info.errors
    6.20 +
    6.21 +
    6.22    /* document node name */
    6.23  
    6.24    def known_file(path: String): Option[Document.Node.Name] =
     7.1 --- a/src/Tools/jEdit/src/jedit_sessions.scala	Tue Oct 31 17:15:49 2017 +0100
     7.2 +++ b/src/Tools/jEdit/src/jedit_sessions.scala	Tue Oct 31 17:56:28 2017 +0100
     7.3 @@ -49,12 +49,12 @@
     7.4  
     7.5    def session_name(options: Options): String = session_info(options).name
     7.6  
     7.7 -  def session_base(options: Options): (List[String], Sessions.Base) =
     7.8 +  def session_base_info(options: Options): Sessions.Base_Info =
     7.9    {
    7.10 -    val (errs, base) =
    7.11 -      Sessions.session_base_errors(
    7.12 -        options, session_name(options), dirs = JEdit_Sessions.session_dirs(), all_known = true)
    7.13 -    (errs, base.platform_path)
    7.14 +    Sessions.session_base_info(options,
    7.15 +      session_name(options),
    7.16 +      dirs = JEdit_Sessions.session_dirs(),
    7.17 +      all_known = true).platform_path
    7.18    }
    7.19  
    7.20    def session_build_mode(): String = Isabelle_System.getenv("JEDIT_BUILD_MODE")