--- 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));