# HG changeset patch
# User haftmann
# Date 1284651111 -7200
# Node ID 465064e8f2691c934fc2ab5c02946abdf9174d25
# Parent  8866d068791a93a6c0333c167b54c79d6abc4dc3
added output_typewriter from doc-src/more_antiquote.ML

diff -r 8866d068791a -r 465064e8f269 src/Pure/Thy/latex.ML
--- a/src/Pure/Thy/latex.ML	Thu Sep 16 17:31:50 2010 +0200
+++ b/src/Pure/Thy/latex.ML	Thu Sep 16 17:31:51 2010 +0200
@@ -13,6 +13,7 @@
   val output_markup: string -> string -> string
   val output_markup_env: string -> string -> string
   val output_verbatim: string -> string
+  val output_typewriter: string -> string
   val markup_true: string
   val markup_false: string
   val begin_delim: string -> string
@@ -97,6 +98,38 @@
 
 end;
 
+fun output_typewriter s =
+  let
+    val parse = Scan.repeat
+      (Scan.this_string "\n" |-- Scan.succeed "\\\\\n\\hspace*{0pt}"
+        || (Scan.this_string " "
+          || Scan.this_string "."
+          || Scan.this_string ","
+          || Scan.this_string ":"
+          || Scan.this_string ";"
+          || Scan.this_string "\"" |-- Scan.succeed "{\\char34}"
+          || Scan.this_string "#" |-- Scan.succeed "{\\char35}"
+          || Scan.this_string "$" |-- Scan.succeed "{\\char36}"
+          || Scan.this_string "%" |-- Scan.succeed "{\\char37}"
+          || Scan.this_string "&" |-- Scan.succeed "{\\char38}"
+          || Scan.this_string "\\" |-- Scan.succeed "{\\char92}"
+          || Scan.this_string "^" |-- Scan.succeed "{\\char94}"
+          || Scan.this_string "_" |-- Scan.succeed "{\\char95}"
+          || Scan.this_string "{" |-- Scan.succeed "{\\char123}"
+          || Scan.this_string "}" |-- Scan.succeed "{\\char125}"
+          || Scan.this_string "~" |-- Scan.succeed "{\\char126}")
+          -- Scan.repeat (Scan.this_string " ")
+          >> (fn (x, xs) => x ^ replicate_string (length xs) "~")
+        || Scan.one Symbol.not_eof);
+    fun is_newline s = (s = "\n");
+    val cs = explode s |> take_prefix is_newline |> snd
+      |> take_suffix is_newline |> fst;
+    val (texts, []) =  Scan.finite Symbol.stopper parse cs
+  in if null texts
+    then ""
+    else implode ("\\isatypewriter%\n\\noindent%\n\\hspace*{0pt}" :: texts)
+  end
+
 
 (* token output *)