# HG changeset patch
# User wenzelm
# Date 1636139186 -3600
# Node ID dff89ef81c21f16d79a0a969933ed7472c70a673
# Parent  9d7f95c43584b7b8897ff3393b24a5d270ec5c87
tuned;

diff -r 9d7f95c43584 -r dff89ef81c21 src/Pure/Thy/presentation.scala
--- a/src/Pure/Thy/presentation.scala	Fri Nov 05 19:53:35 2021 +0100
+++ b/src/Pure/Thy/presentation.scala	Fri Nov 05 20:06:26 2021 +0100
@@ -461,17 +461,16 @@
           case List(XML.Elem(Markup("span", List("id" -> _)), _)) => None
           case _ =>
             Some {
+              val entities =
+                theory_by_name.get(context.node.theory).flatMap(_.entity_by_range.get(range))
+                  .getOrElse(Nil)
               val body1 =
                 if (context.seen_ranges.contains(range)) {
                   HTML.entity_def(HTML.span(HTML.id(html_context.offset_ref(range)), body))
                 }
                 else HTML.span(body)
-              theory_by_name.get(context.node.theory).flatMap(_.entity_by_range.get(range)) match {
-                case Some(entities) =>
-                  entities.map(html_context.export_ref).foldLeft(body1) {
-                    case (elem, id) => HTML.entity_def(HTML.span(HTML.id(id), List(elem)))
-                  }
-                case None => body1
+              entities.map(html_context.export_ref).foldLeft(body1) {
+                case (elem, id) => HTML.entity_def(HTML.span(HTML.id(id), List(elem)))
               }
             }
         }