tuned;
authorwenzelm
Fri Apr 07 20:25:01 2017 +0200 (2017-04-07)
changeset 65432d938705819bb
parent 65431 4a3e6cda3b94
child 65433 a260181505c1
tuned;
src/Pure/Thy/sessions.scala
src/Pure/Tools/build.scala
src/Pure/Tools/ml_process.scala
     1.1 --- a/src/Pure/Thy/sessions.scala	Fri Apr 07 19:35:39 2017 +0200
     1.2 +++ b/src/Pure/Thy/sessions.scala	Fri Apr 07 20:25:01 2017 +0200
     1.3 @@ -57,6 +57,10 @@
     1.4    {
     1.5      def loaded_theory(name: Document.Node.Name): Boolean =
     1.6        loaded_theories.isDefinedAt(name.theory)
     1.7 +
     1.8 +    def dest_known_theories: List[(String, String)] =
     1.9 +      for ((theory, node_name) <- known_theories.toList)
    1.10 +        yield (theory, node_name.node)
    1.11    }
    1.12  
    1.13    sealed case class Deps(sessions: Map[String, Base])
    1.14 @@ -110,12 +114,6 @@
    1.15              }
    1.16            }
    1.17  
    1.18 -          val known_theories =
    1.19 -            Base.known_theories(
    1.20 -              parent_base :: info.imports.map(sessions(_)), thy_deps.deps.map(_.name))
    1.21 -
    1.22 -          val loaded_theories = thy_deps.loaded_theories
    1.23 -          val keywords = thy_deps.keywords
    1.24            val syntax = thy_deps.syntax
    1.25  
    1.26            val theory_files = thy_deps.deps.map(dep => Path.explode(dep.name.node))
    1.27 @@ -147,9 +145,11 @@
    1.28  
    1.29            val base =
    1.30              Base(global_theories = global_theories,
    1.31 -              loaded_theories = loaded_theories,
    1.32 -              known_theories = known_theories,
    1.33 -              keywords = keywords,
    1.34 +              loaded_theories = thy_deps.loaded_theories,
    1.35 +              known_theories =
    1.36 +                Base.known_theories(
    1.37 +                  parent_base :: info.imports.map(sessions(_)), thy_deps.deps.map(_.name)),
    1.38 +              keywords = thy_deps.keywords,
    1.39                syntax = syntax,
    1.40                sources = all_files.map(p => (p, SHA1.digest(p.file))),
    1.41                session_graph = thy_deps.session_graph(info.parent getOrElse "", parent_base))
     2.1 --- a/src/Pure/Tools/build.scala	Fri Apr 07 19:35:39 2017 +0200
     2.2 +++ b/src/Pure/Tools/build.scala	Fri Apr 07 20:25:01 2017 +0200
     2.3 @@ -197,10 +197,6 @@
     2.4        Future.thread("build") {
     2.5          val parent = info.parent.getOrElse("")
     2.6  
     2.7 -        val known_theories =
     2.8 -          for ((theory, node_name) <- deps(name).known_theories.toList)
     2.9 -            yield (theory, node_name.node)
    2.10 -
    2.11          val args_yxml =
    2.12            YXML.string_of_body(
    2.13              {
    2.14 @@ -214,7 +210,7 @@
    2.15                  (store.browser_info, (info.document_files, (File.standard_path(graph_file),
    2.16                  (parent, (info.chapter, (name, (Path.current,
    2.17                  (info.theories,
    2.18 -                known_theories)))))))))))))
    2.19 +                deps(name).dest_known_theories)))))))))))))
    2.20              })
    2.21  
    2.22          val env =
     3.1 --- a/src/Pure/Tools/ml_process.scala	Fri Apr 07 19:35:39 2017 +0200
     3.2 +++ b/src/Pure/Tools/ml_process.scala	Fri Apr 07 20:25:01 2017 +0200
     3.3 @@ -95,13 +95,10 @@
     3.4        session_base match {
     3.5          case None => Nil
     3.6          case Some(base) =>
     3.7 -          val known_theories =
     3.8 -            for ((theory, node_name) <- base.known_theories.toList)
     3.9 -              yield (theory, node_name.node)
    3.10            List("Resources.set_session_base {known_theories = " +
    3.11              ML_Syntax.print_list(
    3.12                ML_Syntax.print_pair(
    3.13 -                ML_Syntax.print_string, ML_Syntax.print_string))(known_theories) + "}")
    3.14 +                ML_Syntax.print_string, ML_Syntax.print_string))(base.dest_known_theories) + "}")
    3.15        }
    3.16  
    3.17      // process