--- a/src/Pure/Thy/latex.ML Mon Oct 20 14:11:14 2014 +0200
+++ b/src/Pure/Thy/latex.ML Mon Oct 20 16:52:36 2014 +0200
@@ -6,6 +6,7 @@
signature LATEX =
sig
+ val output_ascii: string -> string
val output_known_symbols: (string -> bool) * (string -> bool) ->
Symbol.symbol list -> string
val output_symbols: Symbol.symbol list -> string
@@ -30,6 +31,18 @@
structure Latex: LATEX =
struct
+(* literal ASCII *)
+
+val output_ascii =
+ translate_string
+ (fn " " => "\\ "
+ | "\t" => "\\ "
+ | "\n" => "\\isanewline\n"
+ | s =>
+ if exists_string (fn s' => s = s') "#$%^&_{}~\\"
+ then enclose "{\\char`\\" "}" s else s);
+
+
(* symbol output *)
local