src/Pure/Thy/sessions.scala
changeset 67219 81e9804b2014
parent 67216 99815211970c
child 67284 0094d938c53b
     1.1 --- a/src/Pure/Thy/sessions.scala	Sat Dec 16 20:02:40 2017 +0100
     1.2 +++ b/src/Pure/Thy/sessions.scala	Sat Dec 16 21:53:07 2017 +0100
     1.3 @@ -31,6 +31,7 @@
     1.4      val empty: Known = Known()
     1.5  
     1.6      def make(local_dir: Path, bases: List[Base],
     1.7 +      sessions: List[String] = Nil,
     1.8        theories: List[Document.Node.Name] = Nil,
     1.9        loaded_files: List[(String, List[Path])] = Nil): Known =
    1.10      {
    1.11 @@ -46,6 +47,9 @@
    1.12          theories.iterator.filter(name => name.path.canonical_file.toPath.startsWith(local_path))
    1.13        }
    1.14  
    1.15 +      val known_sessions =
    1.16 +        (sessions.toSet /: bases)({ case (known, base) => known ++ base.known.sessions })
    1.17 +
    1.18        val known_theories =
    1.19          (Map.empty[String, Document.Node.Name] /: (bases_iterator(false) ++ theories.iterator))({
    1.20            case (known, name) =>
    1.21 @@ -74,13 +78,16 @@
    1.22        val known_loaded_files =
    1.23          (loaded_files.toMap /: bases.map(base => base.known.loaded_files))(_ ++ _)
    1.24  
    1.25 -      Known(known_theories, known_theories_local,
    1.26 +      Known(
    1.27 +        known_sessions,
    1.28 +        known_theories, known_theories_local,
    1.29          known_files.iterator.map(p => (p._1, p._2.reverse)).toMap,
    1.30          known_loaded_files)
    1.31      }
    1.32    }
    1.33  
    1.34    sealed case class Known(
    1.35 +    sessions: Set[String] = Set.empty,
    1.36      theories: Map[String, Document.Node.Name] = Map.empty,
    1.37      theories_local: Map[String, Document.Node.Name] = Map.empty,
    1.38      files: Map[JFile, List[Document.Node.Name]] = Map.empty,
    1.39 @@ -298,6 +305,7 @@
    1.40  
    1.41              val known =
    1.42                Known.make(info.dir, List(imports_base),
    1.43 +                sessions = List(info.name),
    1.44                  theories = dependencies.theories,
    1.45                  loaded_files = loaded_files)
    1.46