# HG changeset patch # User wenzelm # Date 1413877822 -7200 # Node ID 6e7b009e6d94a6a247b75c009f7f4c73d7b23050 # Parent 42398b610f865c1699949e756defd44caefb70d5 clarified verbatim line breaks, e.g. relevant for Implementation mldecls; diff -r 42398b610f86 -r 6e7b009e6d94 src/Pure/PIDE/resources.ML --- a/src/Pure/PIDE/resources.ML Mon Oct 20 23:17:28 2014 +0200 +++ b/src/Pure/PIDE/resources.ML Tue Oct 21 09:50:22 2014 +0200 @@ -224,7 +224,7 @@ space_explode "/" name |> map Latex.output_ascii |> space_implode (Latex.output_ascii "/" ^ "\\discretionary{}{}{}") - |> Thy_Output.enclose_isabelle_tt ctxt + |> enclose "\\isatt{" "}" end; in diff -r 42398b610f86 -r 6e7b009e6d94 src/Pure/Thy/thy_output.ML --- a/src/Pure/Thy/thy_output.ML Mon Oct 20 23:17:28 2014 +0200 +++ b/src/Pure/Thy/thy_output.ML Tue Oct 21 09:50:22 2014 +0200 @@ -35,7 +35,6 @@ Token.src -> 'a list -> Pretty.T list val output: Proof.context -> Pretty.T list -> string val verbatim_text: Proof.context -> string -> string - val enclose_isabelle_tt: Proof.context -> string -> string end; structure Thy_Output: THY_OUTPUT = @@ -470,10 +469,6 @@ fun tweak_line ctxt s = if Config.get ctxt display then s else Symbol.strip_blanks s; -fun tweak_lines ctxt s = - if Config.get ctxt display then s - else s |> split_lines |> map Symbol.strip_blanks |> space_implode " "; - fun pretty_text ctxt = Pretty.chunks o map Pretty.str o map (tweak_line ctxt) o split_lines; @@ -643,18 +638,18 @@ (* verbatim text *) -fun enclose_isabelle_tt ctxt = - if Config.get ctxt display - then enclose "\\begin{isabellett}%\n" "%\n\\end{isabellett}" - else enclose "\\isatt{" "}"; +fun verbatim_text ctxt = + if Config.get ctxt display then + Latex.output_ascii #> + enclose "\\begin{isabellett}%\n" "%\n\\end{isabellett}" + else + split_lines #> + map (Latex.output_ascii #> enclose "\\isatt{" "}") #> + space_implode "\\isasep\\isanewline%\n"; -fun verbatim_text ctxt = - tweak_lines ctxt - #> Latex.output_ascii - #> enclose_isabelle_tt ctxt; - -val _ = Theory.setup - (antiquotation @{binding verbatim} (Scan.lift Args.text) (verbatim_text o #context)); +val _ = + Theory.setup + (antiquotation @{binding verbatim} (Scan.lift Args.text) (verbatim_text o #context)); (* ML text *)