# HG changeset patch
# User wenzelm
# Date 1506516505 -7200
# Node ID 5174ce7c84f0d16b6ae868b319db9646058a613f
# Parent  16fd7655d39d14c10be945a17c0de974ac3158f0
clarified: more uniform results;

diff -r 16fd7655d39d -r 5174ce7c84f0 src/Pure/PIDE/resources.scala
--- a/src/Pure/PIDE/resources.scala	Wed Sep 27 13:29:52 2017 +0200
+++ b/src/Pure/PIDE/resources.scala	Wed Sep 27 14:48:25 2017 +0200
@@ -66,7 +66,7 @@
         val spans = syntax.parse_spans(text)
         val dir = Path.explode(name.master_dir)
         spans.iterator.map(Command.span_files(syntax, _)._1).flatten.
-          map(a => dir + Path.explode(a)).toList
+          map(a => (dir + Path.explode(a)).expand).toList
       }
       else Nil
     }