src/Pure/Isar/outer_syntax.scala

         (if (files.isEmpty) "" else " (" + commas_quote(files) + ")")
     }).toList.sorted.mkString("keywords\n  ", " and\n  ", "")
 
   def keyword_kind_files(name: String): Option[(String, List[String])] = keywords.get(name)
   def keyword_kind(name: String): Option[String] = keyword_kind_files(name).map(_._1)
+
+  def thy_load(span: List[Token]): Option[List[String]] =
+    keywords.get(Command.name(span)) match {
+      case Some((Keyword.THY_LOAD, files)) => Some(files)
+      case _ => None
+    }
 
   def thy_load_commands: List[(String, List[String])] =
     (for ((name, (Keyword.THY_LOAD, files)) <- keywords.iterator) yield (name, files)).toList
 
   def + (name: String, kind: (String, List[String]), replace: Option[String]): Outer_Syntax =