1.1 --- a/doc-src/antiquote_setup.ML	Thu Feb 26 20:41:28 2009 +0100
     1.2 +++ b/doc-src/antiquote_setup.ML	Thu Feb 26 20:44:07 2009 +0100
     1.3 @@ -16,10 +16,11 @@
     1.4  
     1.5  val clean_string = translate
     1.6    (fn "_" => "\\_"
     1.7 +    | "#" => "\\#"
     1.8      | "<" => "$<$"
     1.9      | ">" => "$>$"
    1.10 -    | "#" => "\\#"
    1.11      | "{" => "\\{"
    1.12 +    | "|" => "$\\mid$"
    1.13      | "}" => "\\}"
    1.14      | "\\<dash>" => "-"
    1.15      | c => c);
    1.16 @@ -68,8 +69,9 @@
    1.17      val txt' = if kind = "" then txt else kind ^ " " ^ txt;
    1.18      val _ = writeln (ml (txt1, txt2));
    1.19      val _ = ML_Context.eval_in (SOME ctxt) false Position.none (ml (txt1, txt2));
    1.20 +    val kind' = if kind = "" then "ML" else "ML " ^ kind;
    1.21    in
    1.22 -    "\\indexml" ^ kind ^ enclose "{" "}" (clean_string txt1) ^
    1.23 +    "\\indexdef{}{" ^ kind' ^ "}{" ^ clean_string txt1 ^ "}" ^
    1.24      (txt'
    1.25      |> (if ! O.quotes then quote else I)
    1.26      |> (if ! O.display then enclose "\\begin{verbatim}\n" "\n\\end{verbatim}"