clarified verbatim line breaks, e.g. relevant for Implementation mldecls;
authorwenzelm
Tue Oct 21 09:50:22 2014 +0200 (2014-10-21 ago)
changeset 587416e7b009e6d94
parent 58728 42398b610f86
child 58742 bb55a3530709
clarified verbatim line breaks, e.g. relevant for Implementation mldecls;
src/Pure/PIDE/resources.ML
src/Pure/Thy/thy_output.ML
     1.1 --- a/src/Pure/PIDE/resources.ML	Mon Oct 20 23:17:28 2014 +0200
     1.2 +++ b/src/Pure/PIDE/resources.ML	Tue Oct 21 09:50:22 2014 +0200
     1.3 @@ -224,7 +224,7 @@
     1.4      space_explode "/" name
     1.5      |> map Latex.output_ascii
     1.6      |> space_implode (Latex.output_ascii "/" ^ "\\discretionary{}{}{}")
     1.7 -    |> Thy_Output.enclose_isabelle_tt ctxt
     1.8 +    |> enclose "\\isatt{" "}"
     1.9    end;
    1.10  
    1.11  in
     2.1 --- a/src/Pure/Thy/thy_output.ML	Mon Oct 20 23:17:28 2014 +0200
     2.2 +++ b/src/Pure/Thy/thy_output.ML	Tue Oct 21 09:50:22 2014 +0200
     2.3 @@ -35,7 +35,6 @@
     2.4      Token.src -> 'a list -> Pretty.T list
     2.5    val output: Proof.context -> Pretty.T list -> string
     2.6    val verbatim_text: Proof.context -> string -> string
     2.7 -  val enclose_isabelle_tt: Proof.context -> string -> string
     2.8  end;
     2.9  
    2.10  structure Thy_Output: THY_OUTPUT =
    2.11 @@ -470,10 +469,6 @@
    2.12  fun tweak_line ctxt s =
    2.13    if Config.get ctxt display then s else Symbol.strip_blanks s;
    2.14  
    2.15 -fun tweak_lines ctxt s =
    2.16 -  if Config.get ctxt display then s
    2.17 -  else s |> split_lines |> map Symbol.strip_blanks |> space_implode " ";
    2.18 -
    2.19  fun pretty_text ctxt =
    2.20    Pretty.chunks o map Pretty.str o map (tweak_line ctxt) o split_lines;
    2.21  
    2.22 @@ -643,18 +638,18 @@
    2.23  
    2.24  (* verbatim text *)
    2.25  
    2.26 -fun enclose_isabelle_tt ctxt =
    2.27 -  if Config.get ctxt display
    2.28 -  then enclose "\\begin{isabellett}%\n" "%\n\\end{isabellett}"
    2.29 -  else enclose "\\isatt{" "}";
    2.30 +fun verbatim_text ctxt =
    2.31 +  if Config.get ctxt display then
    2.32 +    Latex.output_ascii #>
    2.33 +    enclose "\\begin{isabellett}%\n" "%\n\\end{isabellett}"
    2.34 +  else
    2.35 +    split_lines #>
    2.36 +    map (Latex.output_ascii #> enclose "\\isatt{" "}") #>
    2.37 +    space_implode "\\isasep\\isanewline%\n";
    2.38  
    2.39 -fun verbatim_text ctxt =
    2.40 -  tweak_lines ctxt
    2.41 -  #> Latex.output_ascii
    2.42 -  #> enclose_isabelle_tt ctxt;
    2.43 -
    2.44 -val _ = Theory.setup
    2.45 -  (antiquotation @{binding verbatim} (Scan.lift Args.text) (verbatim_text o #context));
    2.46 +val _ =
    2.47 +  Theory.setup
    2.48 +    (antiquotation @{binding verbatim} (Scan.lift Args.text) (verbatim_text o #context));
    2.49  
    2.50  
    2.51  (* ML text *)