# HG changeset patch
# User wenzelm
# Date 1506503467 -7200
# Node ID 190834aa43a7b21fec599668fd358b92aa9f1a29
# Parent  8f863dae78a0ab093f8d7c9f1aa885b8f336016a
tuned;

diff -r 8f863dae78a0 -r 190834aa43a7 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