1.1 --- a/doc-src/antiquote_setup.ML Thu Jul 19 15:32:58 2007 +0200
1.2 +++ b/doc-src/antiquote_setup.ML Thu Jul 19 15:33:27 2007 +0200
1.3 @@ -52,6 +52,33 @@
1.4
1.5 fun pretty_thy_file name = (ThyLoad.check_thy Path.current name false; Pretty.str name);
1.6
1.7 +
1.8 +(* theorems with names *)
1.9 +
1.10 +fun tweak_line s =
1.11 + if ! O.display then s else Symbol.strip_blanks s;
1.12 +
1.13 +val pretty_text = Pretty.chunks o map Pretty.str o map tweak_line o Library.split_lines;
1.14 +
1.15 +fun output_named_list pretty src ctxt xs =
1.16 + map (apfst (pretty ctxt)) xs (*always pretty in order to exhibit errors!*)
1.17 + |> (if ! O.quotes then map (apfst Pretty.quote) else I)
1.18 + |> (if ! O.display then
1.19 + map (fn (p, name) =>
1.20 + Output.output (Pretty.string_of (Pretty.indent (! O.indent) p)) ^
1.21 + "\\rulename{" ^ Output.output (Pretty.str_of (pretty_text name)) ^ "}")
1.22 + #> space_implode "\\par\\smallskip%\n"
1.23 + #> enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}"
1.24 + else
1.25 + map (fn (p, name) =>
1.26 + Output.output (Pretty.str_of p) ^
1.27 + "\\rulename{" ^ Output.output (Pretty.str_of (pretty_text name)) ^ "}")
1.28 + #> space_implode "\\par\\smallskip%\n"
1.29 + #> enclose "\\isa{" "}");
1.30 +
1.31 +fun pretty_term ctxt = ProofContext.pretty_term ctxt o ProofContext.revert_skolems ctxt;
1.32 +fun pretty_thm ctxt = pretty_term ctxt o Thm.full_prop_of;
1.33 +
1.34 in
1.35
1.36 val _ = O.add_commands
1.37 @@ -62,6 +89,9 @@
1.38 ("index_ML_functor", arguments (index_ml "functor" ml_functor)),
1.39 ("ML_functor", O.args (Scan.lift Args.name) output_verbatim),
1.40 ("verbatim", O.args (Scan.lift Args.name) output_verbatim),
1.41 - ("thy_file", O.args (Scan.lift Args.name) (O.output (K pretty_thy_file)))];
1.42 + ("thy_file", O.args (Scan.lift Args.name) (O.output (K pretty_thy_file))),
1.43 + ("named_thms", O.args (Scan.repeat (Attrib.thm --
1.44 + Scan.lift (Args.$$$ "(" |-- Args.name --| Args.$$$ ")")))
1.45 + (output_named_list pretty_thm))];
1.46
1.47 end;