# HG changeset patch # User wenzelm # Date 938026671 -7200 # Node ID 6e6dafacbc28bc864592f50b6dc2828a625d945e # Parent 44e9db3150f68650a0bab0ae7b9ebf93d05e40b5 present results; diff -r 44e9db3150f6 -r 6e6dafacbc28 src/Pure/Isar/isar_thy.ML --- 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; diff -r 44e9db3150f6 -r 6e6dafacbc28 src/Pure/Thy/browser_info.ML --- 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)); diff -r 44e9db3150f6 -r 6e6dafacbc28 src/Pure/Thy/html.ML --- 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 *)