1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/doc-src/antiquote_setup.ML Wed Nov 15 15:37:34 2006 +0100
1.3 @@ -0,0 +1,60 @@
1.4 +(* Title: antiquote_setup.ML
1.5 + ID: $Id$
1.6 + Author: Makarius
1.7 +
1.8 +Auxiliary antiquotations for Isabelle manuals.
1.9 +*)
1.10 +
1.11 +local
1.12 +
1.13 +structure O = IsarOutput;
1.14 +
1.15 +val str_of_source = space_implode " " o map Args.string_of o #2 o #1 o Args.dest_src;
1.16 +
1.17 +fun ml_val (txt1, "") = "fn _ => (" ^ txt1 ^ ");"
1.18 + | ml_val (txt1, txt2) = "fn _ => (" ^ txt1 ^ ": " ^ txt2 ^ ");";
1.19 +
1.20 +fun ml_type (txt1, "") = "val _ = NONE : (" ^ txt1 ^ ") option;"
1.21 + | ml_type (txt1, txt2) = "val _ = [NONE : (" ^ txt1 ^ ") option, NONE : (" ^ txt2 ^ ") option];";
1.22 +
1.23 +fun ml_structure (txt, _) = "functor DUMMY_FUNCTOR() = struct structure DUMMY = " ^ txt ^ " end;"
1.24 +
1.25 +fun ml_functor _ = "val _ = ();"; (*no check!*)
1.26 +
1.27 +val verbatim = space_implode "\\verb,|," o map (enclose "\\verb|" "|") o space_explode "|";
1.28 +
1.29 +fun index_ml kind ml src ctxt (txt1, txt2) =
1.30 + let
1.31 + val txt = if txt2 = "" then txt1 else
1.32 + if kind = "type"
1.33 + then txt1 ^ " = " ^ txt2
1.34 + else txt1 ^ ": " ^ txt2;
1.35 + val txt' = if kind = "" then txt else kind ^ " " ^ txt;
1.36 + val _ = Context.use_mltext (ml (txt1, txt2)) false (SOME (ProofContext.theory_of ctxt));
1.37 + in
1.38 + "\\indexml" ^ kind ^ enclose "{" "}"
1.39 + (translate_string (fn "_" => "-" | ">" => "$>$" | c => c) txt1) ^
1.40 + ((if ! O.source then str_of_source src else txt')
1.41 + |> (if ! O.quotes then quote else I)
1.42 + |> (if ! O.display then enclose "\\begin{verbatim}\n" "\n\\end{verbatim}"
1.43 + else split_lines #> map verbatim #> space_implode "\\isasep\\isanewline%\n"))
1.44 + end;
1.45 +
1.46 +fun output_verbatim _ _ = split_lines #> map verbatim #> space_implode "\\isasep\\isanewline%\n";
1.47 +
1.48 +fun arguments x = O.args (Scan.lift (Args.name -- Scan.optional (Args.colon |-- Args.name) "")) x;
1.49 +
1.50 +fun pretty_thy_file name = (ThyLoad.check_thy Path.current name false; Pretty.str name);
1.51 +
1.52 +in
1.53 +
1.54 +val _ = O.add_commands
1.55 + [("index_ML", arguments (index_ml "" ml_val)),
1.56 + ("index_ML_type", arguments (index_ml "type" ml_type)),
1.57 + ("index_ML_structure", arguments (index_ml "structure" ml_structure)),
1.58 + ("index_ML_functor", arguments (index_ml "functor" ml_functor)),
1.59 + ("ML_functor", O.args (Scan.lift Args.name) output_verbatim),
1.60 + ("verbatim", O.args (Scan.lift Args.name) output_verbatim),
1.61 + ("thy_file", O.args (Scan.lift Args.name) (O.output (K pretty_thy_file)))];
1.62 +
1.63 +end;