--- a/doc-src/antiquote_setup.ML Wed Mar 04 10:43:39 2009 +0100
+++ b/doc-src/antiquote_setup.ML Wed Mar 04 10:45:52 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Doc/antiquote_setup.ML
- ID: $Id$
Author: Makarius
Auxiliary antiquotations for the Isabelle manuals.
@@ -13,13 +12,17 @@
(* misc utils *)
-val clean_string = translate_string
+fun translate f = Symbol.explode #> map f #> implode;
+
+val clean_string = translate
(fn "_" => "\\_"
+ | "#" => "\\#"
| "<" => "$<$"
| ">" => "$>$"
- | "#" => "\\#"
| "{" => "\\{"
+ | "|" => "$\\mid$"
| "}" => "\\}"
+ | "\\<dash>" => "-"
| c => c);
fun clean_name "\\<dots>" = "dots"
@@ -28,7 +31,7 @@
| clean_name "_" = "underscore"
| clean_name "{" = "braceleft"
| clean_name "}" = "braceright"
- | clean_name s = s |> translate_string (fn "_" => "-" | c => c);
+ | clean_name s = s |> translate (fn "_" => "-" | "\\<dash>" => "-" | c => c);
(* verbatim text *)
@@ -66,8 +69,9 @@
val txt' = if kind = "" then txt else kind ^ " " ^ txt;
val _ = writeln (ml (txt1, txt2));
val _ = ML_Context.eval_in (SOME ctxt) false Position.none (ml (txt1, txt2));
+ val kind' = if kind = "" then "ML" else "ML " ^ kind;
in
- "\\indexml" ^ kind ^ enclose "{" "}" (clean_string txt1) ^
+ "\\indexdef{}{" ^ kind' ^ "}{" ^ clean_string txt1 ^ "}" ^
(txt'
|> (if ! O.quotes then quote else I)
|> (if ! O.display then enclose "\\begin{verbatim}\n" "\n\\end{verbatim}"
@@ -193,6 +197,7 @@
entity_antiqs no_check "" "case" @
entity_antiqs (K ThyOutput.defined_command) "" "antiquotation" @
entity_antiqs (fn _ => fn name => is_some (OS.Process.getEnv name)) "isatt" "setting" @
+ entity_antiqs no_check "" "inference" @
entity_antiqs no_check "isatt" "executable" @
entity_antiqs (K check_tool) "isatt" "tool" @
entity_antiqs (K (File.exists o Path.explode)) "isatt" "file" @