--- 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 *)