# 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, _) =>