src/Pure/PIDE/resources.scala

     if (syntax.load_commands_in(text)) {
       val spans = syntax.parse_spans(text)
       spans.iterator.map(Command.span_files(syntax, _)._1).flatten.toList
     }
     else Nil
+
+  def loaded_files(syntax: Outer_Syntax, name: Document.Node.Name): List[Path] =
+  {
+    val text = with_thy_reader(name, reader => Symbol.decode(reader.source.toString))
+    val dir = Path.explode(name.master_dir)
+    loaded_files(syntax, text).map(a => dir + Path.explode(a))
+  }
 
   def theory_qualifier(name: Document.Node.Name): String =
     session_base.global_theories.getOrElse(name.theory, Long_Name.qualifier(name.theory))
 
   def theory_name(qualifier: String, theory0: String): (Boolean, String) =