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;