# HG changeset patch
# User wenzelm
# Date 1516387288 -3600
# Node ID 1a279ad4c6a46a98a299931bbe4cbddcd4c7332b
# Parent  90def2b0630594a848c44ea01d15fac3768ceb7a
disable "display" style in marginal (line) comment;

diff -r 90def2b06305 -r 1a279ad4c6a4 src/Pure/Thy/thy_output.ML
--- a/src/Pure/Thy/thy_output.ML	Fri Jan 19 19:09:25 2018 +0100
+++ b/src/Pure/Thy/thy_output.ML	Fri Jan 19 19:41:28 2018 +0100
@@ -99,8 +99,10 @@
       let
         val body = Symbol_Pos.cartouche_content syms;
         val source = Input.source true (Symbol_Pos.implode body) (Symbol_Pos.range body);
+        val ctxt' = ctxt
+          |> Config.put Document_Antiquotation.thy_output_display false;
       in
-        output_text ctxt {markdown = false} source
+        output_text ctxt' {markdown = false} source
         |> Latex.enclose_body "%\n\\isamarkupcmt{" "%\n}"
       end
   | (SOME Comment.Cancel, _) =>