diff -r 954f44210b92 -r c4e9e0c50487 src/Pure/Thy/sessions.scala --- a/src/Pure/Thy/sessions.scala Tue Jan 23 17:58:09 2018 +0100 +++ b/src/Pure/Thy/sessions.scala Tue Jan 23 19:25:39 2018 +0100 @@ -40,7 +40,7 @@ val empty: Known = Known() def make(local_dir: Path, bases: List[Base], - sessions: List[String] = Nil, + sessions: List[(String, Position.T)] = Nil, theories: List[Document.Node.Name] = Nil, loaded_files: List[(String, List[Path])] = Nil): Known = { @@ -57,7 +57,7 @@ } val known_sessions = - (sessions.toSet /: bases)({ case (known, base) => known ++ base.known.sessions }) + (sessions.toMap /: bases)({ case (known, base) => known ++ base.known.sessions }) val known_theories = (Map.empty[String, Document.Node.Name] /: (bases_iterator(false) ++ theories.iterator))({ @@ -96,7 +96,7 @@ } sealed case class Known( - sessions: Set[String] = Set.empty, + sessions: Map[String, Position.T] = Map.empty, theories: Map[String, Document.Node.Name] = Map.empty, theories_local: Map[String, Document.Node.Name] = Map.empty, files: Map[JFile, List[Document.Node.Name]] = Map.empty, @@ -317,7 +317,7 @@ val known = Known.make(info.dir, List(imports_base), - sessions = List(info.name), + sessions = List(info.name -> info.pos), theories = dependencies.theories, loaded_files = loaded_files)