diff -r 31dd98471e88 -r f1f983484878 src/Pure/Thy/html.scala --- 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 ++= "" + output_string(Symbol.control_name(sym).get) + s ++= "" + output_hidden(output_string(Symbol.control_suffix)) + } + else output_string(sym) } }