diff -r fb8a7962f2ae -r 688a7dd22cbb src/Pure/Thy/html.scala
--- a/src/Pure/Thy/html.scala	Mon May 08 12:04:58 2017 +0200
+++ b/src/Pure/Thy/html.scala	Mon May 08 14:08:27 2017 +0200
@@ -103,6 +103,7 @@
   val par = new Operator("p")
   val emph = new Operator("em")
   val bold = new Operator("b")
+  val code = new Operator("code")
 
   val title = new Heading("title")
   val chapter = new Heading("h1")