1.1 --- a/doc-src/antiquote_setup.ML	Wed Mar 04 10:43:39 2009 +0100
     1.2 +++ b/doc-src/antiquote_setup.ML	Wed Mar 04 10:45:52 2009 +0100
     1.3 @@ -1,5 +1,4 @@
     1.4  (*  Title:      Doc/antiquote_setup.ML
     1.5 -    ID:         $Id$
     1.6      Author:     Makarius
     1.7  
     1.8  Auxiliary antiquotations for the Isabelle manuals.
     1.9 @@ -13,13 +12,17 @@
    1.10  
    1.11  (* misc utils *)
    1.12  
    1.13 -val clean_string = translate_string
    1.14 +fun translate f = Symbol.explode #> map f #> implode;
    1.15 +
    1.16 +val clean_string = translate
    1.17    (fn "_" => "\\_"
    1.18 +    | "#" => "\\#"
    1.19      | "<" => "$<$"
    1.20      | ">" => "$>$"
    1.21 -    | "#" => "\\#"
    1.22      | "{" => "\\{"
    1.23 +    | "|" => "$\\mid$"
    1.24      | "}" => "\\}"
    1.25 +    | "\\<dash>" => "-"
    1.26      | c => c);
    1.27  
    1.28  fun clean_name "\\<dots>" = "dots"
    1.29 @@ -28,7 +31,7 @@
    1.30    | clean_name "_" = "underscore"
    1.31    | clean_name "{" = "braceleft"
    1.32    | clean_name "}" = "braceright"
    1.33 -  | clean_name s = s |> translate_string (fn "_" => "-" | c => c);
    1.34 +  | clean_name s = s |> translate (fn "_" => "-" | "\\<dash>" => "-" | c => c);
    1.35  
    1.36  
    1.37  (* verbatim text *)
    1.38 @@ -66,8 +69,9 @@
    1.39      val txt' = if kind = "" then txt else kind ^ " " ^ txt;
    1.40      val _ = writeln (ml (txt1, txt2));
    1.41      val _ = ML_Context.eval_in (SOME ctxt) false Position.none (ml (txt1, txt2));
    1.42 +    val kind' = if kind = "" then "ML" else "ML " ^ kind;
    1.43    in
    1.44 -    "\\indexml" ^ kind ^ enclose "{" "}" (clean_string txt1) ^
    1.45 +    "\\indexdef{}{" ^ kind' ^ "}{" ^ clean_string txt1 ^ "}" ^
    1.46      (txt'
    1.47      |> (if ! O.quotes then quote else I)
    1.48      |> (if ! O.display then enclose "\\begin{verbatim}\n" "\n\\end{verbatim}"
    1.49 @@ -193,6 +197,7 @@
    1.50    entity_antiqs no_check "" "case" @
    1.51    entity_antiqs (K ThyOutput.defined_command) "" "antiquotation" @
    1.52    entity_antiqs (fn _ => fn name => is_some (OS.Process.getEnv name)) "isatt" "setting" @
    1.53 +  entity_antiqs no_check "" "inference" @
    1.54    entity_antiqs no_check "isatt" "executable" @
    1.55    entity_antiqs (K check_tool) "isatt" "tool" @
    1.56    entity_antiqs (K (File.exists o Path.explode)) "isatt" "file" @