src/Pure/Thy/document_output.ML

--- a/src/Pure/Thy/document_output.ML	Tue Sep 28 10:47:18 2021 +0200
+++ b/src/Pure/Thy/document_output.ML	Tue Sep 28 16:01:13 2021 +0200
@@ -156,6 +156,7 @@
     | Token.Alt_String => output false "{\\isacharbackquoteopen}" "{\\isacharbackquoteclose}"
     | Token.Verbatim => output true "{\\isacharverbatimopen}" "{\\isacharverbatimclose}"
     | Token.Cartouche => output false "{\\isacartoucheopen}" "{\\isacartoucheclose}"
+    | Token.Control control => output_body ctxt false "" "" (Antiquote.control_symbols control)
     | _ => output false "" "")
   end handle ERROR msg => error (msg ^ Position.here (Token.pos_of tok));