tuned;
authorwenzelm
Fri, 05 Nov 2021 20:34:44 +0100
changeset 74707 a44d14207050
parent 74706 84e8595a0ec7
child 74708 b2df121ccfc1
tuned;
src/Pure/Thy/presentation.scala
--- a/src/Pure/Thy/presentation.scala	Fri Nov 05 20:26:07 2021 +0100
+++ b/src/Pure/Thy/presentation.scala	Fri Nov 05 20:34:44 2021 +0100
@@ -430,7 +430,7 @@
           map(link => HTML.text("View ") ::: List(link))).flatten
     }
 
-    val theory_by_name: Map[String, Export_Theory.Theory] =
+    val theory_exports: Map[String, Export_Theory.Theory] =
       (for ((_, entry) <- base.known_theories.iterator) yield {
         val thy_name = entry.name.theory
         val theory =
@@ -461,7 +461,7 @@
           case _ =>
             Some {
               val entities =
-                theory_by_name.get(context.node.theory).flatMap(_.entity_by_range.get(range))
+                theory_exports.get(context.node.theory).flatMap(_.entity_by_range.get(range))
                   .getOrElse(Nil)
               val body1 =
                 if (context.seen_ranges.contains(range)) {
@@ -477,7 +477,7 @@
 
       def entity_ref(thy_name: String, kind: String, name: String): Option[String] =
         for {
-          thy <- theory_by_name.get(thy_name)
+          thy <- theory_exports.get(thy_name)
           entity <- thy.entity_by_kname.get(Export_Theory.export_kind_name(kind, name))
         } yield entity.kname