src/Pure/Thy/latex.ML

 LaTeX presentation elements -- based on outer lexical syntax.
 *)
 
 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
   val output_basic: Token.T -> string
   val output_markup: string -> string -> string

   val modes: string list
 end;
 
 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