proper pretty printing for latex output, notably for pide_session=true (default);
authorwenzelm
Sun Jul 26 21:53:29 2020 +0200 (2 weeks ago)
changeset 720759c0b835d4cc2
parent 72074 f3e1144a1cec
child 72076 bd9d1ce274c9
proper pretty printing for latex output, notably for pide_session=true (default);
src/Pure/General/pretty.ML
src/Pure/Thy/document_antiquotation.ML
     1.1 --- a/src/Pure/General/pretty.ML	Sat Jul 25 23:23:59 2020 +0200
     1.2 +++ b/src/Pure/General/pretty.ML	Sun Jul 26 21:53:29 2020 +0200
     1.3 @@ -60,6 +60,7 @@
     1.4    val indent: int -> T -> T
     1.5    val unbreakable: T -> T
     1.6    val margin_default: int Unsynchronized.ref
     1.7 +  val regularN: string
     1.8    val symbolicN: string
     1.9    val output_buffer: int option -> T -> Buffer.T
    1.10    val output: int option -> T -> Output.output
    1.11 @@ -346,10 +347,12 @@
    1.12  
    1.13  val margin_default = Unsynchronized.ref ML_Pretty.default_margin;  (*right margin, or page width*)
    1.14  
    1.15 +val regularN = "pretty_regular";
    1.16  val symbolicN = "pretty_symbolic";
    1.17  
    1.18  fun output_buffer margin prt =
    1.19 -  if print_mode_active symbolicN then symbolic prt
    1.20 +  if print_mode_active symbolicN andalso not (print_mode_active regularN)
    1.21 +  then symbolic prt
    1.22    else formatted (the_default (! margin_default) margin) prt;
    1.23  
    1.24  val output = Buffer.content oo output_buffer;
     2.1 --- a/src/Pure/Thy/document_antiquotation.ML	Sat Jul 25 23:23:59 2020 +0200
     2.2 +++ b/src/Pure/Thy/document_antiquotation.ML	Sun Jul 26 21:53:29 2020 +0200
     2.3 @@ -181,7 +181,8 @@
     2.4      val _ = command pos (opts, src) preview_ctxt;
     2.5  
     2.6      val print_ctxt = Context_Position.set_visible false preview_ctxt;
     2.7 -    val print_modes = space_explode "," (Config.get print_ctxt thy_output_modes) @ [Latex.latexN];
     2.8 +    val print_modes =
     2.9 +      space_explode "," (Config.get print_ctxt thy_output_modes) @ [Latex.latexN, Pretty.regularN];
    2.10    in [Print_Mode.with_modes print_modes (fn () => command pos (opts, src) print_ctxt) ()] end;
    2.11  
    2.12  in