1.1 --- a/doc-src/IsarImplementation/style.sty Sat Feb 10 09:26:06 2007 +0100
1.2 +++ b/doc-src/IsarImplementation/style.sty Sat Feb 10 09:26:07 2007 +0100
1.3 @@ -19,6 +19,7 @@
1.4
1.5 %% index
1.6 \newcommand{\indexml}[1]{\index{\emph{#1}|bold}}
1.7 +\newcommand{\indexmlexception}[1]{\index{\emph{#1} (exception)|bold}}
1.8 \newcommand{\indexmltype}[1]{\index{\emph{#1} (type)|bold}}
1.9 \newcommand{\indexmlstructure}[1]{\index{\emph{#1} (structure)|bold}}
1.10 \newcommand{\indexmlfunctor}[1]{\index{\emph{#1} (functor)|bold}}
2.1 --- a/doc-src/antiquote_setup.ML Sat Feb 10 09:26:06 2007 +0100
2.2 +++ b/doc-src/antiquote_setup.ML Sat Feb 10 09:26:07 2007 +0100
2.3 @@ -16,7 +16,10 @@
2.4
2.5 fun ml_type (txt1, "") = "val _ = NONE : (" ^ txt1 ^ ") option;"
2.6 | ml_type (txt1, txt2) = "val _ = [NONE : (" ^ txt1 ^ ") option, NONE : (" ^ txt2 ^ ") option];";
2.7 -
2.8 +
2.9 +fun ml_exc (txt1, "") = "fn _ => (" ^ txt1 ^ ": exn);"
2.10 + | ml_exc (txt1, txt2) = "fn _ => (" ^ txt1 ^ ": " ^ txt2 ^ " -> exn);";
2.11 +
2.12 fun ml_structure (txt, _) = "functor DUMMY_FUNCTOR() = struct structure DUMMY = " ^ txt ^ " end;"
2.13
2.14 fun ml_functor _ = "val _ = ();"; (*no check!*)
2.15 @@ -28,12 +31,15 @@
2.16 val txt = if txt2 = "" then txt1 else
2.17 if kind = "type"
2.18 then txt1 ^ " = " ^ txt2
2.19 - else txt1 ^ ": " ^ txt2;
2.20 + else if kind = "exception"
2.21 + then txt1 ^ " of " ^ txt2
2.22 + else txt1 ^ ": " ^ txt2;
2.23 val txt' = if kind = "" then txt else kind ^ " " ^ txt;
2.24 + val _ = writeln (ml (txt1, txt2));
2.25 val _ = ML_Context.use_mltext (ml (txt1, txt2)) false (SOME (Context.Proof ctxt));
2.26 in
2.27 "\\indexml" ^ kind ^ enclose "{" "}"
2.28 - (translate_string (fn "_" => "-" | ">" => "$>$" | c => c) txt1) ^
2.29 + (translate_string (fn "_" => "-" | ">" => "$>$" | "#" => "\\#" | c => c) txt1) ^
2.30 ((if ! O.source then str_of_source src else txt')
2.31 |> (if ! O.quotes then quote else I)
2.32 |> (if ! O.display then enclose "\\begin{verbatim}\n" "\n\\end{verbatim}"
2.33 @@ -51,6 +57,7 @@
2.34 val _ = O.add_commands
2.35 [("index_ML", arguments (index_ml "" ml_val)),
2.36 ("index_ML_type", arguments (index_ml "type" ml_type)),
2.37 + ("index_ML_exc", arguments (index_ml "exception" ml_exc)),
2.38 ("index_ML_structure", arguments (index_ml "structure" ml_structure)),
2.39 ("index_ML_functor", arguments (index_ml "functor" ml_functor)),
2.40 ("ML_functor", O.args (Scan.lift Args.name) output_verbatim),