diff -r 2fd0c33fe440 -r a1a316442a9b src/Pure/Thy/document_output.ML
--- a/src/Pure/Thy/document_output.ML	Sat Nov 13 16:43:04 2021 +0100
+++ b/src/Pure/Thy/document_output.ML	Sat Nov 13 17:22:10 2021 +0100
@@ -211,8 +211,8 @@
 
 (* command spans *)
 
-type command = string * Position.T;   (*name, position*)
-type source = (token * (string * int)) list;        (*token, markup flag, meta-comment depth*)
+type command = string * Position.T;  (*name, position*)
+type source = (token * (string * int)) list;  (*token, markup flag, meta-comment depth*)
 
 datatype span = Span of command * (source * source * source * source) * bool;