src/Pure/Thy/html.scala
changeset 67255 f1f983484878
parent 66212 f41396c15bb1
child 67336 3ee6da378183
--- a/src/Pure/Thy/html.scala	Fri Dec 22 14:35:29 2017 +0100
+++ b/src/Pure/Thy/html.scala	Fri Dec 22 15:49:44 2017 +0100
@@ -56,7 +56,14 @@
           case Some(html) =>
             output_hidden(output_string(sym)); s ++= html
           case None =>
-            output_string(sym)
+            if (hidden && Symbol.is_control_encoded(sym)) {
+              output_hidden(output_string(Symbol.control_prefix))
+              s ++= "<span class=\"control\">"
+              output_string(Symbol.control_name(sym).get)
+              s ++= "</span>"
+              output_hidden(output_string(Symbol.control_suffix))
+            }
+            else output_string(sym)
         }
       }