src/Pure/Thy/export_theory.scala

       thms.iterator.map(_.no_content) ++
       classes.iterator.map(_.no_content) ++
       locales.iterator.map(_.no_content) ++
       locale_dependencies.iterator.map(_.no_content) ++
       (for { (_, xs) <- others; x <- xs.iterator } yield x.no_content)
+
+    lazy val entity_by_range: Map[Symbol.Range, List[Entity[No_Content]]] =
+      entity_iterator.toList.groupBy(_.range)
+
+    lazy val entity_by_kname: Map[String, Entity[No_Content]] =
+      entity_iterator.map(entity => (entity.kname, entity)).toMap
 
     lazy val entity_kinds: Set[String] =
       entity_iterator.map(_.kind).toSet
 
     def cache(cache: Term.Cache): Theory =

     else {
       provider(Export.THEORY_PREFIX + "parents")
         .map(entry => split_lines(entry.uncompressed.text))
     }
   }
+
+  def no_theory: Theory =
+    Theory("", Nil, Nil, Nil, Nil, Nil, Nil, Nil, Nil, Nil, Nil, Nil, Nil, Nil, Nil, Map.empty)
 
   def read_theory(provider: Export.Provider, session_name: String, theory_name: String,
     cache: Term.Cache = Term.Cache.none): Theory =
   {
     val parents =

   def export_kind(kind: String): String =
     if (kind == Markup.TYPE_NAME) Kind.TYPE
     else if (kind == Markup.CONSTANT) Kind.CONST
     else kind
 
+  def export_kind_name(kind: String, name: String): String =
+    name + "|" + export_kind(kind)
+
   abstract class Content[T]
   {
     def cache(cache: Term.Cache): T
   }
   sealed case class No_Content() extends Content[No_Content]

     pos: Position.T,
     id: Option[Long],
     serial: Long,
     content: Option[A])
   {
+    val kname: String = export_kind_name(kind, name)
+    val range: Symbol.Range = Position.Range.unapply(pos).getOrElse(Text.Range.offside)
+
     def export_kind: String = Export_Theory.export_kind(kind)
     override def toString: String = export_kind + " " + quote(name)
 
     def the_content: A =
       if (content.isDefined) content.get else error("No content for " + toString)