--- a/etc/isabelle.css Wed Nov 03 22:03:56 2021 +0100
+++ b/etc/isabelle.css Wed Nov 03 22:55:22 2021 +0100
@@ -122,3 +122,30 @@
}
.tooltip pre { margin: 1px; white-space: pre-wrap; }
+
+
+/* formal entities */
+
+.entity_def {
+ color: inherit;
+ text-decoration: inherit;
+}
+
+.entity_def:hover {
+ color: inherit;
+ text-decoration: inherit;
+ background-color: rgba(50,50,50,20%);
+}
+
+.entity_ref {
+ color: inherit;
+ text-decoration: inherit;
+ border: 0.5px solid rgba(0,0,0,0);
+}
+
+.entity_ref:hover {
+ color: inherit;
+ text-decoration: inherit;
+ background-color: rgba(50,50,50,20%);
+ border: 0.5px solid black;
+}
--- a/src/Pure/Thy/html.scala Wed Nov 03 22:03:56 2021 +0100
+++ b/src/Pure/Thy/html.scala Wed Nov 03 22:55:22 2021 +0100
@@ -24,6 +24,9 @@
def height(h: Int): Attribute = new Attribute("height", h.toString)
def size(w: Int, h: Int)(elem: XML.Elem): XML.Elem = width(w)(height(h)(elem))
+ val entity_def: Attribute = class_("entity_def")
+ val entity_ref: Attribute = class_("entity_ref")
+
/* structured markup operators */
--- a/src/Pure/Thy/presentation.scala Wed Nov 03 22:03:56 2021 +0100
+++ b/src/Pure/Thy/presentation.scala Wed Nov 03 22:55:22 2021 +0100
@@ -477,13 +477,14 @@
Some {
val body1 =
if (context.seen_ranges.contains(range)) {
- HTML.span(HTML.id(html_context.offset_ref(range)), body)
+ HTML.entity_def(HTML.span(HTML.id(html_context.offset_ref(range)), body))
}
else HTML.span(body)
export_ranges.get(context.node).flatMap(_.get(range)) match {
case Some(entities) =>
entities.map(html_context.export_ref).foldLeft(body1) {
- case (elem, id) => HTML.span(HTML.id(id), List(elem))
+ case (elem, id) =>
+ HTML.entity_def(HTML.span(HTML.id(id), List(elem)))
}
case None => body1
}
@@ -525,7 +526,7 @@
html_file = node_file(node_name)
html_ref <- entity_ref(theory, name).orElse(offset_ref(context, theory, props))
} yield {
- HTML.link(html_dir + html_file + "#" + html_ref, body)
+ HTML.entity_ref(HTML.link(html_dir + html_file + "#" + html_ref, body))
}
case _ => None
}