src/Pure/Thy/latex.ML
changeset 58716 23a380cc45f4
parent 55828 42ac3cfb89f6
child 58727 e3d0a6a012eb
--- 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