# HG changeset patch
# User wenzelm
# Date 1635976522 -3600
# Node ID 0efa6a8b6e2035f2e7ee052d2840daa389e27541
# Parent  e04806c89b10d0bcae1de4b9a95b04e1a38ae500
clarified link style: similar to Isabelle/jEdit;

diff -r e04806c89b10 -r 0efa6a8b6e20 etc/isabelle.css
--- 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;
+}
diff -r e04806c89b10 -r 0efa6a8b6e20 src/Pure/Thy/html.scala
--- 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 */
 
diff -r e04806c89b10 -r 0efa6a8b6e20 src/Pure/Thy/presentation.scala
--- 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
         }