# HG changeset patch
# User wenzelm
# Date 1515870093 -3600
# Node ID c4a10621c72e62f6aaed12b7bd1b5beacdbff66e
# Parent  c4c8787ed66914e9bc0942cf20b406597c2f17b0
allow TeX comment % in formal comment body, but avoid extra space (cf. d7c6054b2ab1);

diff -r c4c8787ed669 -r c4a10621c72e src/Pure/Thy/thy_output.ML
--- a/src/Pure/Thy/thy_output.ML	Sat Jan 13 19:50:37 2018 +0100
+++ b/src/Pure/Thy/thy_output.ML	Sat Jan 13 20:01:33 2018 +0100
@@ -124,7 +124,7 @@
         val source = Input.source true (Symbol_Pos.implode body) (Symbol_Pos.range body);
       in
         output_text ctxt {markdown = false} source
-        |> Latex.enclose_body "%\n\\isamarkupcmt{" "}"
+        |> Latex.enclose_body "%\n\\isamarkupcmt{" "%\n}"
       end);
 
 in