src/Pure/Thy/sessions.scala
changeset 67493 c4e9e0c50487
parent 67472 bddfa23a4ea9
child 67846 bdf6933f7ac9
     1.1 --- a/src/Pure/Thy/sessions.scala	Tue Jan 23 17:58:09 2018 +0100
     1.2 +++ b/src/Pure/Thy/sessions.scala	Tue Jan 23 19:25:39 2018 +0100
     1.3 @@ -40,7 +40,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 +      sessions: List[(String, Position.T)] = Nil,
     1.9        theories: List[Document.Node.Name] = Nil,
    1.10        loaded_files: List[(String, List[Path])] = Nil): Known =
    1.11      {
    1.12 @@ -57,7 +57,7 @@
    1.13        }
    1.14  
    1.15        val known_sessions =
    1.16 -        (sessions.toSet /: bases)({ case (known, base) => known ++ base.known.sessions })
    1.17 +        (sessions.toMap /: bases)({ case (known, base) => known ++ base.known.sessions })
    1.18  
    1.19        val known_theories =
    1.20          (Map.empty[String, Document.Node.Name] /: (bases_iterator(false) ++ theories.iterator))({
    1.21 @@ -96,7 +96,7 @@
    1.22    }
    1.23  
    1.24    sealed case class Known(
    1.25 -    sessions: Set[String] = Set.empty,
    1.26 +    sessions: Map[String, Position.T] = Map.empty,
    1.27      theories: Map[String, Document.Node.Name] = Map.empty,
    1.28      theories_local: Map[String, Document.Node.Name] = Map.empty,
    1.29      files: Map[JFile, List[Document.Node.Name]] = Map.empty,
    1.30 @@ -317,7 +317,7 @@
    1.31  
    1.32              val known =
    1.33                Known.make(info.dir, List(imports_base),
    1.34 -                sessions = List(info.name),
    1.35 +                sessions = List(info.name -> info.pos),
    1.36                  theories = dependencies.theories,
    1.37                  loaded_files = loaded_files)
    1.38