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 */