--- 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