tuned;
authorwenzelm
Wed, 27 Sep 2017 11:11:07 +0200
changeset 66697 190834aa43a7
parent 66696 8f863dae78a0
child 66698 5b9dc3f7bcde
tuned;
src/Pure/PIDE/resources.scala
--- a/src/Pure/PIDE/resources.scala	Tue Sep 26 22:30:54 2017 +0200
+++ b/src/Pure/PIDE/resources.scala	Wed Sep 27 11:11:07 2017 +0200
@@ -72,14 +72,14 @@
   def pure_files(syntax: Outer_Syntax, session: String, dir: Path): List[Path] =
     if (Sessions.is_pure(session)) {
       val roots =
-        for { (name, theory) <- Thy_Header.ml_roots }
-        yield ((dir + Path.explode(name)).expand, theory)
+        for { (name, _) <- Thy_Header.ml_roots }
+        yield (dir + Path.explode(name)).expand
       val files =
         for {
-          (path, theory) <- roots
+          (path, (_, theory)) <- roots zip Thy_Header.ml_roots
           file <- loaded_files(syntax, Document.Node.Name(path.implode, path.dir.implode, theory))
         } yield file
-      roots.map(_._1) ::: files
+      roots ::: files
     }
     else Nil