src/Pure/Thy/sessions.scala
changeset 67493 c4e9e0c50487
parent 67471 bddfa23a4ea9
child 67846 bdf6933f7ac9
--- 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)