# HG changeset patch
# User berghofe
# Date 1184852007 -7200
# Node ID bfedd1a024fc05d721fb06a6fc6373dc5973a257
# Parent  0b695c401d4d116151b16e9477694f0678c92d54
Added named_thms antiquotation.

diff -r 0b695c401d4d -r bfedd1a024fc doc-src/antiquote_setup.ML
--- a/doc-src/antiquote_setup.ML	Thu Jul 19 15:32:58 2007 +0200
+++ b/doc-src/antiquote_setup.ML	Thu Jul 19 15:33:27 2007 +0200
@@ -52,6 +52,33 @@
 
 fun pretty_thy_file name = (ThyLoad.check_thy Path.current name false; Pretty.str name);
 
+
+(* theorems with names *)
+
+fun tweak_line s =
+  if ! O.display then s else Symbol.strip_blanks s;
+
+val pretty_text = Pretty.chunks o map Pretty.str o map tweak_line o Library.split_lines;
+
+fun output_named_list pretty src ctxt xs =
+  map (apfst (pretty ctxt)) xs        (*always pretty in order to exhibit errors!*)
+  |> (if ! O.quotes then map (apfst Pretty.quote) else I)
+  |> (if ! O.display then
+    map (fn (p, name) =>
+      Output.output (Pretty.string_of (Pretty.indent (! O.indent) p)) ^
+      "\\rulename{" ^ Output.output (Pretty.str_of (pretty_text name)) ^ "}")
+    #> space_implode "\\par\\smallskip%\n"
+    #> enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}"
+  else
+    map (fn (p, name) =>
+      Output.output (Pretty.str_of p) ^
+      "\\rulename{" ^ Output.output (Pretty.str_of (pretty_text name)) ^ "}")
+    #> space_implode "\\par\\smallskip%\n"
+    #> enclose "\\isa{" "}");
+
+fun pretty_term ctxt = ProofContext.pretty_term ctxt o ProofContext.revert_skolems ctxt;
+fun pretty_thm ctxt = pretty_term ctxt o Thm.full_prop_of;
+
 in
 
 val _ = O.add_commands
@@ -62,6 +89,9 @@
   ("index_ML_functor", arguments (index_ml "functor" ml_functor)),
   ("ML_functor", O.args (Scan.lift Args.name) output_verbatim),
   ("verbatim", O.args (Scan.lift Args.name) output_verbatim),
-  ("thy_file", O.args (Scan.lift Args.name) (O.output (K pretty_thy_file)))];
+  ("thy_file", O.args (Scan.lift Args.name) (O.output (K pretty_thy_file))),
+  ("named_thms", O.args (Scan.repeat (Attrib.thm --
+       Scan.lift (Args.$$$ "(" |-- Args.name --| Args.$$$ ")")))
+     (output_named_list pretty_thm))];
 
 end;