1.1 --- a/doc-src/more_antiquote.ML	Fri Oct 31 10:39:04 2008 +0100
     1.2 +++ b/doc-src/more_antiquote.ML	Mon Nov 03 14:15:25 2008 +0100
     1.3 @@ -7,7 +7,7 @@
     1.4  
     1.5  signature MORE_ANTIQUOTE =
     1.6  sig
     1.7 -  val verbatim_lines: string list -> string
     1.8 +  val verbatim: string -> string
     1.9  end;
    1.10  
    1.11  structure More_Antiquote : MORE_ANTIQUOTE =
    1.12 @@ -17,12 +17,34 @@
    1.13  
    1.14  (* printing verbatim lines *)
    1.15  
    1.16 -val verbatim_line = space_implode "\\verb,|," o map (enclose "\\verb|" "|") o space_explode "|";
    1.17 -val verbatim_lines = rev
    1.18 -  #> dropwhile (fn s => s = "")
    1.19 -  #> rev
    1.20 -  #> map verbatim_line #> space_implode "\\newline%\n"
    1.21 -  #> prefix "\\isaverbatim%\n\\noindent%\n"
    1.22 +fun verbatim s =
    1.23 +  let
    1.24 +    val parse = Scan.repeat
    1.25 +      (Scan.this_string "\n" |-- Scan.succeed "\\\\\n\\hspace*{0pt}"
    1.26 +        || (Scan.this_string " " 
    1.27 +          || Scan.this_string ":"
    1.28 +          || Scan.this_string "\"" |-- Scan.succeed "{\\char34}"
    1.29 +          || Scan.this_string "#" |-- Scan.succeed "{\\char35}"
    1.30 +          || Scan.this_string "$" |-- Scan.succeed "{\\char36}"
    1.31 +          || Scan.this_string "%" |-- Scan.succeed "{\\char37}"
    1.32 +          || Scan.this_string "&" |-- Scan.succeed "{\\char38}"
    1.33 +          || Scan.this_string "\\" |-- Scan.succeed "{\\char92}"
    1.34 +          || Scan.this_string "^" |-- Scan.succeed "{\\char94}"
    1.35 +          || Scan.this_string "_" |-- Scan.succeed "{\\char95}"
    1.36 +          || Scan.this_string "{" |-- Scan.succeed "{\\char123}"
    1.37 +          || Scan.this_string "}" |-- Scan.succeed "{\\char125}"
    1.38 +          || Scan.this_string "~" |-- Scan.succeed "{\\char126}")
    1.39 +          -- Scan.repeat (Scan.this_string " ")
    1.40 +          >> (fn (x, xs) => x ^ replicate_string (length xs) "~")
    1.41 +        || Scan.one Symbol.not_eof);
    1.42 +    fun is_newline s = (s = "\n");
    1.43 +    val cs = explode s |> take_prefix is_newline |> snd
    1.44 +      |> take_suffix is_newline |> fst;
    1.45 +    val (texts, []) =  Scan.finite Symbol.stopper parse cs
    1.46 +  in if null texts
    1.47 +    then ""
    1.48 +    else implode ("\\isaverbatim%\n\\noindent%\n\\hspace*{0pt}" :: texts)
    1.49 +  end
    1.50  
    1.51  
    1.52  (* class antiquotation *)
    1.53 @@ -69,8 +91,7 @@
    1.54      Code_Target.code_of (ProofContext.theory_of ctxt)
    1.55        target "Example" (mk_cs (ProofContext.theory_of ctxt))
    1.56          (fn naming => maps (fn f => f (ProofContext.theory_of ctxt) naming) mk_stmtss)
    1.57 -    |> split_lines
    1.58 -    |> verbatim_lines;
    1.59 +    |> verbatim;
    1.60  
    1.61  in
    1.62