present results;

--- a/src/Pure/Isar/isar_thy.ML	Tue Sep 21 23:06:50 1999 +0200
+++ b/src/Pure/Isar/isar_thy.ML	Wed Sep 22 20:57:51 1999 +0200
@@ -225,7 +225,11 @@
   f name (map (attrib x) more_srcs)
     (map (fn (s, srcs) => (get x s, map (attrib x) srcs)) th_srcs) x;
 
-fun global_have_thmss x = gen_have_thmss PureThy.get_thms Attrib.global_attribute x;
+fun global_have_thmss kind f (x as ((name, _), _)) thy =
+  let val (thy', thms) = gen_have_thmss PureThy.get_thms Attrib.global_attribute f x thy in
+    if kind <> "" then Context.setmp (Some thy') (Present.results kind name) thms else ();
+    (thy', thms)
+  end;
 
 fun local_have_thmss x =
   gen_have_thmss (ProofContext.get_thms o Proof.context_of)
@@ -237,11 +241,11 @@
 fun have_lemss name atts = PureThy.have_thmss name (atts @ [Drule.tag_lemma]);
 
 
-fun apply_theorems th_srcs = global_have_thmss PureThy.have_thmss (("", []), th_srcs);
+fun apply_theorems th_srcs = global_have_thmss "" PureThy.have_thmss (("", []), th_srcs);
 fun apply_theorems_i th_srcs = gen_have_thmss_i PureThy.have_thmss (("", []), th_srcs);
-val have_theorems = #1 oo (global_have_thmss PureThy.have_thmss o Comment.ignore);
+val have_theorems = #1 oo (global_have_thmss "theorems" PureThy.have_thmss o Comment.ignore);
 val have_theorems_i = #1 oo (gen_have_thmss_i PureThy.have_thmss o Comment.ignore);
-val have_lemmas = #1 oo (global_have_thmss have_lemss o Comment.ignore);
+val have_lemmas = #1 oo (global_have_thmss "lemmas" have_lemss o Comment.ignore);
 val have_lemmas_i = #1 oo (gen_have_thmss_i have_lemss o Comment.ignore);
 val have_facts = ProofHistory.apply o local_have_thmss (Proof.have_thmss []) o Comment.ignore;
 val have_facts_i = ProofHistory.apply o gen_have_thmss_i (Proof.have_thmss []) o Comment.ignore;
@@ -335,12 +339,17 @@
 
 (* print result *)
 
+local
+
 fun pretty_result {kind, name, thm} =
-  Pretty.block [Pretty.str (kind ^ " " ^ name ^ ":"), Pretty.fbrk, Proof.pretty_thm thm];
+  Pretty.block [Pretty.str (kind ^ (if name = "" then "" else " " ^ name ^ ":")),
+    Pretty.fbrk, Proof.pretty_thm thm];
 
 fun pretty_rule thm =
   Pretty.block [Pretty.str "trying to solve goal by rule:", Pretty.fbrk, Proof.pretty_thm thm];
 
+in
+
 val print_result = Pretty.writeln o pretty_result;
 
 fun cond_print_result_rule int =
@@ -349,6 +358,8 @@
 
 fun proof'' f = Toplevel.proof' (f o cond_print_result_rule);
 
+end;
+
 
 (* local endings *)
 
@@ -373,8 +384,8 @@
   let
     val state = ProofHistory.current prf;
     val _ = if Proof.at_bottom state then () else raise Toplevel.UNDEF;
-    val (thy, res) = finish state;
-  in print_result res; thy end);
+    val (thy, res as {kind, name, thm}) = finish state;
+  in print_result res; Context.setmp (Some thy) (Present.result kind name) thm; thy end);
 
 val global_qed = global_result o Method.global_qed o apsome Comment.ignore_interest;
 val global_terminal_proof = global_result o Method.global_terminal_proof o ignore_interests;

--- a/src/Pure/Thy/browser_info.ML	Tue Sep 21 23:06:50 1999 +0200
+++ b/src/Pure/Thy/browser_info.ML	Wed Sep 22 20:57:51 1999 +0200
@@ -18,6 +18,8 @@
   val theory_source: string -> (string, 'a) Source.source -> unit
   val begin_theory: string -> string list -> (Path.T * bool) list -> theory -> theory
   val end_theory: string -> unit
+  val result: string -> string -> thm -> unit
+  val results: string -> string -> thm list -> unit
   val theorem: string -> thm -> unit
   val theorems: string -> thm list -> unit
   val setup: (theory -> theory) list
@@ -31,7 +33,8 @@
 
 val output_path = Path.variable "ISABELLE_BROWSER_INFO";
 
-fun top_path sess_path offset = Path.append (Path.appends (replicate (offset + length sess_path) Path.parent));
+fun top_path sess_path offset =
+  Path.append (Path.appends (replicate (offset + length sess_path) Path.parent));
 
 val html_ext = Path.ext "html";
 val html_path = html_ext o Path.basic;
@@ -359,8 +362,10 @@
 
 fun end_theory _ = ();
 
-fun theorem name thm = with_session () (fn _ => with_context add_html (HTML.theorem name thm));
-fun theorems name thms = with_session () (fn _ => with_context add_html (HTML.theorems name thms));
+fun result k a thm = with_session () (fn _ => with_context add_html (HTML.result k a thm));
+fun results k a thms = with_session () (fn _ => with_context add_html (HTML.results k a thms));
+fun theorem a thm = with_session () (fn _ => with_context add_html (HTML.theorem a thm));
+fun theorems a thms = with_session () (fn _ => with_context add_html (HTML.theorems a thms));
 fun section s = with_session () (fn _ => with_context add_html (HTML.section s));
 
 

--- a/src/Pure/Thy/html.ML	Tue Sep 21 23:06:50 1999 +0200
+++ b/src/Pure/Thy/html.ML	Wed Sep 22 20:57:51 1999 +0200
@@ -32,6 +32,8 @@
     (Url.T option * Url.T * bool option) list -> text -> text
   val end_theory: text
   val ml_file: Url.T -> string -> text
+  val result: string -> string -> thm -> text
+  val results: string -> string -> thm list -> text
   val theorem: string -> thm -> text
   val theorems: string -> thm list -> text
   val section: string -> text
@@ -242,15 +244,26 @@
 
 (* theorems *)
 
+local
+
 val string_of_thm =
   Pretty.setmp_margin 80 Pretty.string_of o
     Display.pretty_thm_no_quote o #1 o Drule.freeze_thaw;
 
 fun thm th = preform (prefix_lines "  " (html_mode string_of_thm th));
 
-fun theorem a th = para (keyword "theorem" ^ " " ^ name (a ^ ":") ^ "\n" ^ thm th);
-fun theorems a ths =
-  para (cat_lines ((keyword "theorems" ^ " " ^ name (a ^ ":")) :: map thm ths));
+fun thm_name "" = ""
+  | thm_name a = " " ^ name (a ^ ":");
+
+in
+
+fun result k a th = para (keyword k ^ thm_name a ^ "\n" ^ thm th);
+fun results k a ths = para (cat_lines ((keyword k ^ thm_name a) :: map thm ths));
+
+val theorem = result "theorem";
+val theorems = results "theorems";
+
+end;
 
 
 (* section *)