diff -r b808eddc83cf -r bda424c5819f src/Pure/PIDE/command_span.scala
--- a/src/Pure/PIDE/command_span.scala	Fri Nov 27 11:50:23 2020 +0100
+++ b/src/Pure/PIDE/command_span.scala	Fri Nov 27 14:00:54 2020 +0100
@@ -67,6 +67,18 @@
       }
       (source, Span(kind, content1.toList))
     }
+
+    def loaded_files(syntax: Outer_Syntax): (List[String], Int) =
+      syntax.load_command(name) match {
+        case Some(exts) =>
+          find_file(clean_tokens(content)) match {
+            case Some((file, i)) =>
+              if (exts.isEmpty) (List(file), i)
+              else (exts.map(ext => file + "." + ext), i)
+            case None => (Nil, -1)
+          }
+        case None => (Nil, -1)
+      }
   }
 
   val empty: Span = Span(Ignored_Span, Nil)
@@ -78,6 +90,28 @@
   }
 
 
+  /* loaded files */
+
+  def clean_tokens(tokens: List[Token]): List[(Token, Int)] =
+  {
+    def clean(toks: List[(Token, Int)]): List[(Token, Int)] =
+      toks match {
+        case (t1, i1) :: (t2, i2) :: rest =>
+          if (t1.is_keyword && t1.source == "%" && t2.is_name) clean(rest)
+          else (t1, i1) :: clean((t2, i2) :: rest)
+        case _ => toks
+      }
+    clean(tokens.zipWithIndex.filter({ case (t, _) => t.is_proper }))
+  }
+
+  def find_file(tokens: List[(Token, Int)]): Option[(String, Int)] =
+    if (tokens.exists({ case (t, _) => t.is_command })) {
+      tokens.dropWhile({ case (t, _) => !t.is_command }).
+        collectFirst({ case (t, i) if t.is_embedded => (t.content, i) })
+    }
+    else None
+
+
   /* XML data representation */
 
   def encode: XML.Encode.T[Span] = (span: Span) =>