1.1 --- a/doc-src/antiquote_setup.ML Sat Feb 10 09:26:06 2007 +0100
1.2 +++ b/doc-src/antiquote_setup.ML Sat Feb 10 09:26:07 2007 +0100
1.3 @@ -16,7 +16,10 @@
1.4
1.5 fun ml_type (txt1, "") = "val _ = NONE : (" ^ txt1 ^ ") option;"
1.6 | ml_type (txt1, txt2) = "val _ = [NONE : (" ^ txt1 ^ ") option, NONE : (" ^ txt2 ^ ") option];";
1.7 -
1.8 +
1.9 +fun ml_exc (txt1, "") = "fn _ => (" ^ txt1 ^ ": exn);"
1.10 + | ml_exc (txt1, txt2) = "fn _ => (" ^ txt1 ^ ": " ^ txt2 ^ " -> exn);";
1.11 +
1.12 fun ml_structure (txt, _) = "functor DUMMY_FUNCTOR() = struct structure DUMMY = " ^ txt ^ " end;"
1.13
1.14 fun ml_functor _ = "val _ = ();"; (*no check!*)
1.15 @@ -28,12 +31,15 @@
1.16 val txt = if txt2 = "" then txt1 else
1.17 if kind = "type"
1.18 then txt1 ^ " = " ^ txt2
1.19 - else txt1 ^ ": " ^ txt2;
1.20 + else if kind = "exception"
1.21 + then txt1 ^ " of " ^ txt2
1.22 + else txt1 ^ ": " ^ txt2;
1.23 val txt' = if kind = "" then txt else kind ^ " " ^ txt;
1.24 + val _ = writeln (ml (txt1, txt2));
1.25 val _ = ML_Context.use_mltext (ml (txt1, txt2)) false (SOME (Context.Proof ctxt));
1.26 in
1.27 "\\indexml" ^ kind ^ enclose "{" "}"
1.28 - (translate_string (fn "_" => "-" | ">" => "$>$" | c => c) txt1) ^
1.29 + (translate_string (fn "_" => "-" | ">" => "$>$" | "#" => "\\#" | c => c) txt1) ^
1.30 ((if ! O.source then str_of_source src else txt')
1.31 |> (if ! O.quotes then quote else I)
1.32 |> (if ! O.display then enclose "\\begin{verbatim}\n" "\n\\end{verbatim}"
1.33 @@ -51,6 +57,7 @@
1.34 val _ = O.add_commands
1.35 [("index_ML", arguments (index_ml "" ml_val)),
1.36 ("index_ML_type", arguments (index_ml "type" ml_type)),
1.37 + ("index_ML_exc", arguments (index_ml "exception" ml_exc)),
1.38 ("index_ML_structure", arguments (index_ml "structure" ml_structure)),
1.39 ("index_ML_functor", arguments (index_ml "functor" ml_functor)),
1.40 ("ML_functor", O.args (Scan.lift Args.name) output_verbatim),