# HG changeset patch
# User haftmann
# Date 1226304208 -3600
# Node ID 185110a4b97a6d2d2b557cbd31e1221ba4c19d73
# Parent  47ff45771f2cdaed9ee1aae43721c77d5499832a
clarified verbatim vs. typewriter

diff -r 47ff45771f2c -r 185110a4b97a doc-src/IsarAdvanced/Classes/Thy/document/Classes.tex
--- a/doc-src/IsarAdvanced/Classes/Thy/document/Classes.tex	Mon Nov 10 08:18:58 2008 +0100
+++ b/doc-src/IsarAdvanced/Classes/Thy/document/Classes.tex	Mon Nov 10 09:03:28 2008 +0100
@@ -1114,7 +1114,7 @@
 \isatagquote
 %
 \begin{isamarkuptext}%
-\isaverbatim%
+\isatypewriter%
 \noindent%
 \hspace*{0pt}module Example where {\char123}\\
 \hspace*{0pt}\\
@@ -1201,7 +1201,7 @@
 \isatagquote
 %
 \begin{isamarkuptext}%
-\isaverbatim%
+\isatypewriter%
 \noindent%
 \hspace*{0pt}structure Example = \\
 \hspace*{0pt}struct\\
diff -r 47ff45771f2c -r 185110a4b97a doc-src/IsarAdvanced/Classes/classes.tex
--- a/doc-src/IsarAdvanced/Classes/classes.tex	Mon Nov 10 08:18:58 2008 +0100
+++ b/doc-src/IsarAdvanced/Classes/classes.tex	Mon Nov 10 09:03:28 2008 +0100
@@ -24,7 +24,7 @@
 \newcommand{\qt}[1]{``{#1}''}
 
 % verbatim text
-\newcommand{\isaverbatim}{\fontsize{9pt}{0pt}\tt\renewcommand{\baselinestretch}{1}\setlength{\baselineskip}{9pt}}
+\newcommand{\isatypewriter}{\fontsize{9pt}{0pt}\tt\renewcommand{\baselinestretch}{1}\setlength{\baselineskip}{9pt}}
 
 % invisibility
 \isadroptag{theory}
diff -r 47ff45771f2c -r 185110a4b97a doc-src/IsarAdvanced/Codegen/Thy/document/Adaption.tex
--- a/doc-src/IsarAdvanced/Codegen/Thy/document/Adaption.tex	Mon Nov 10 08:18:58 2008 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/document/Adaption.tex	Mon Nov 10 09:03:28 2008 +0100
@@ -262,7 +262,7 @@
 \isatagquote
 %
 \begin{isamarkuptext}%
-\isaverbatim%
+\isatypewriter%
 \noindent%
 \hspace*{0pt}structure Example = \\
 \hspace*{0pt}struct\\
@@ -345,7 +345,7 @@
 \isatagquote
 %
 \begin{isamarkuptext}%
-\isaverbatim%
+\isatypewriter%
 \noindent%
 \hspace*{0pt}structure Example = \\
 \hspace*{0pt}struct\\
@@ -402,7 +402,7 @@
 \isatagquote
 %
 \begin{isamarkuptext}%
-\isaverbatim%
+\isatypewriter%
 \noindent%
 \hspace*{0pt}structure Example = \\
 \hspace*{0pt}struct\\
diff -r 47ff45771f2c -r 185110a4b97a doc-src/IsarAdvanced/Codegen/Thy/document/Introduction.tex
--- a/doc-src/IsarAdvanced/Codegen/Thy/document/Introduction.tex	Mon Nov 10 08:18:58 2008 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/document/Introduction.tex	Mon Nov 10 09:03:28 2008 +0100
@@ -149,7 +149,7 @@
 \isatagquote
 %
 \begin{isamarkuptext}%
-\isaverbatim%
+\isatypewriter%
 \noindent%
 \hspace*{0pt}structure Example = \\
 \hspace*{0pt}struct\\
@@ -228,7 +228,7 @@
 \isatagquote
 %
 \begin{isamarkuptext}%
-\isaverbatim%
+\isatypewriter%
 \noindent%
 \hspace*{0pt}module Example where {\char123}\\
 \hspace*{0pt}\\
diff -r 47ff45771f2c -r 185110a4b97a doc-src/IsarAdvanced/Codegen/Thy/document/Program.tex
--- a/doc-src/IsarAdvanced/Codegen/Thy/document/Program.tex	Mon Nov 10 08:18:58 2008 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/document/Program.tex	Mon Nov 10 09:03:28 2008 +0100
@@ -85,7 +85,7 @@
 \isatagquote
 %
 \begin{isamarkuptext}%
-\isaverbatim%
+\isatypewriter%
 \noindent%
 \hspace*{0pt}dequeue ::~forall a. Queue a -> (Maybe a, Queue a);\\
 \hspace*{0pt}dequeue (Queue xs (y :~ys)) = (Just y, Queue xs ys);\\
@@ -271,7 +271,7 @@
 \isatagquote
 %
 \begin{isamarkuptext}%
-\isaverbatim%
+\isatypewriter%
 \noindent%
 \hspace*{0pt}module Example where {\char123}\\
 \hspace*{0pt}\\
@@ -336,7 +336,7 @@
 \isatagquote
 %
 \begin{isamarkuptext}%
-\isaverbatim%
+\isatypewriter%
 \noindent%
 \hspace*{0pt}structure Example = \\
 \hspace*{0pt}struct\\
@@ -657,7 +657,7 @@
 \isatagquote
 %
 \begin{isamarkuptext}%
-\isaverbatim%
+\isatypewriter%
 \noindent%
 \hspace*{0pt}structure Example = \\
 \hspace*{0pt}struct\\
@@ -774,7 +774,7 @@
 \isatagquote
 %
 \begin{isamarkuptext}%
-\isaverbatim%
+\isatypewriter%
 \noindent%
 \hspace*{0pt}structure Example = \\
 \hspace*{0pt}struct\\
@@ -910,7 +910,7 @@
 \isatagquote
 %
 \begin{isamarkuptext}%
-\isaverbatim%
+\isatypewriter%
 \noindent%
 \hspace*{0pt}structure Example = \\
 \hspace*{0pt}struct\\
@@ -1031,7 +1031,7 @@
 \isatagquote
 %
 \begin{isamarkuptext}%
-\isaverbatim%
+\isatypewriter%
 \noindent%
 \hspace*{0pt}structure Example = \\
 \hspace*{0pt}struct\\
@@ -1106,7 +1106,7 @@
 \isatagquote
 %
 \begin{isamarkuptext}%
-\isaverbatim%
+\isatypewriter%
 \noindent%
 \hspace*{0pt}strict{\char95}dequeue ::~forall a. Queue a -> (a, Queue a);\\
 \hspace*{0pt}strict{\char95}dequeue (Queue xs (y :~ys)) = (y, Queue xs ys);\\
@@ -1202,7 +1202,7 @@
 \isatagquote
 %
 \begin{isamarkuptext}%
-\isaverbatim%
+\isatypewriter%
 \noindent%
 \hspace*{0pt}empty{\char95}queue ::~forall a. a;\\
 \hspace*{0pt}empty{\char95}queue = error {\char34}empty{\char95}queue{\char34};\\
diff -r 47ff45771f2c -r 185110a4b97a doc-src/IsarAdvanced/Codegen/codegen.tex
--- a/doc-src/IsarAdvanced/Codegen/codegen.tex	Mon Nov 10 08:18:58 2008 +0100
+++ b/doc-src/IsarAdvanced/Codegen/codegen.tex	Mon Nov 10 09:03:28 2008 +0100
@@ -26,7 +26,7 @@
 \newcommand{\qt}[1]{``{#1}''}
 
 % verbatim text
-\newcommand{\isaverbatim}{\fontsize{9pt}{0pt}\tt\renewcommand{\baselinestretch}{1}\setlength{\baselineskip}{9pt}}
+\newcommand{\isatypewriter}{\fontsize{9pt}{0pt}\tt\renewcommand{\baselinestretch}{1}\setlength{\baselineskip}{9pt}}
 
 % invisibility
 \isadroptag{theory}
diff -r 47ff45771f2c -r 185110a4b97a doc-src/more_antiquote.ML
--- a/doc-src/more_antiquote.ML	Mon Nov 10 08:18:58 2008 +0100
+++ b/doc-src/more_antiquote.ML	Mon Nov 10 09:03:28 2008 +0100
@@ -7,7 +7,7 @@
 
 signature MORE_ANTIQUOTE =
 sig
-  val verbatim: string -> string
+  val typewriter: string -> string
 end;
 
 structure More_Antiquote : MORE_ANTIQUOTE =
@@ -15,9 +15,9 @@
 
 structure O = ThyOutput;
 
-(* printing verbatim lines *)
+(* printing typewriter lines *)
 
-fun verbatim s =
+fun typewriter s =
   let
     val parse = Scan.repeat
       (Scan.this_string "\n" |-- Scan.succeed "\\\\\n\\hspace*{0pt}"
@@ -43,7 +43,7 @@
     val (texts, []) =  Scan.finite Symbol.stopper parse cs
   in if null texts
     then ""
-    else implode ("\\isaverbatim%\n\\noindent%\n\\hspace*{0pt}" :: texts)
+    else implode ("\\isatypewriter%\n\\noindent%\n\\hspace*{0pt}" :: texts)
   end
 
 
@@ -91,7 +91,7 @@
     Code_Target.code_of (ProofContext.theory_of ctxt)
       target "Example" (mk_cs (ProofContext.theory_of ctxt))
         (fn naming => maps (fn f => f (ProofContext.theory_of ctxt) naming) mk_stmtss)
-    |> verbatim;
+    |> typewriter;
 
 in