present results;
authorwenzelm
Wed Sep 22 20:57:51 1999 +0200 (1999-09-22)
changeset 75726e6dafacbc28
parent 7571 44e9db3150f6
child 7573 aa87cf5a15f5
present results;
src/Pure/Isar/isar_thy.ML
src/Pure/Thy/browser_info.ML
src/Pure/Thy/html.ML
     1.1 --- a/src/Pure/Isar/isar_thy.ML	Tue Sep 21 23:06:50 1999 +0200
     1.2 +++ b/src/Pure/Isar/isar_thy.ML	Wed Sep 22 20:57:51 1999 +0200
     1.3 @@ -225,7 +225,11 @@
     1.4    f name (map (attrib x) more_srcs)
     1.5      (map (fn (s, srcs) => (get x s, map (attrib x) srcs)) th_srcs) x;
     1.6  
     1.7 -fun global_have_thmss x = gen_have_thmss PureThy.get_thms Attrib.global_attribute x;
     1.8 +fun global_have_thmss kind f (x as ((name, _), _)) thy =
     1.9 +  let val (thy', thms) = gen_have_thmss PureThy.get_thms Attrib.global_attribute f x thy in
    1.10 +    if kind <> "" then Context.setmp (Some thy') (Present.results kind name) thms else ();
    1.11 +    (thy', thms)
    1.12 +  end;
    1.13  
    1.14  fun local_have_thmss x =
    1.15    gen_have_thmss (ProofContext.get_thms o Proof.context_of)
    1.16 @@ -237,11 +241,11 @@
    1.17  fun have_lemss name atts = PureThy.have_thmss name (atts @ [Drule.tag_lemma]);
    1.18  
    1.19  
    1.20 -fun apply_theorems th_srcs = global_have_thmss PureThy.have_thmss (("", []), th_srcs);
    1.21 +fun apply_theorems th_srcs = global_have_thmss "" PureThy.have_thmss (("", []), th_srcs);
    1.22  fun apply_theorems_i th_srcs = gen_have_thmss_i PureThy.have_thmss (("", []), th_srcs);
    1.23 -val have_theorems = #1 oo (global_have_thmss PureThy.have_thmss o Comment.ignore);
    1.24 +val have_theorems = #1 oo (global_have_thmss "theorems" PureThy.have_thmss o Comment.ignore);
    1.25  val have_theorems_i = #1 oo (gen_have_thmss_i PureThy.have_thmss o Comment.ignore);
    1.26 -val have_lemmas = #1 oo (global_have_thmss have_lemss o Comment.ignore);
    1.27 +val have_lemmas = #1 oo (global_have_thmss "lemmas" have_lemss o Comment.ignore);
    1.28  val have_lemmas_i = #1 oo (gen_have_thmss_i have_lemss o Comment.ignore);
    1.29  val have_facts = ProofHistory.apply o local_have_thmss (Proof.have_thmss []) o Comment.ignore;
    1.30  val have_facts_i = ProofHistory.apply o gen_have_thmss_i (Proof.have_thmss []) o Comment.ignore;
    1.31 @@ -335,12 +339,17 @@
    1.32  
    1.33  (* print result *)
    1.34  
    1.35 +local
    1.36 +
    1.37  fun pretty_result {kind, name, thm} =
    1.38 -  Pretty.block [Pretty.str (kind ^ " " ^ name ^ ":"), Pretty.fbrk, Proof.pretty_thm thm];
    1.39 +  Pretty.block [Pretty.str (kind ^ (if name = "" then "" else " " ^ name ^ ":")),
    1.40 +    Pretty.fbrk, Proof.pretty_thm thm];
    1.41  
    1.42  fun pretty_rule thm =
    1.43    Pretty.block [Pretty.str "trying to solve goal by rule:", Pretty.fbrk, Proof.pretty_thm thm];
    1.44  
    1.45 +in
    1.46 +
    1.47  val print_result = Pretty.writeln o pretty_result;
    1.48  
    1.49  fun cond_print_result_rule int =
    1.50 @@ -349,6 +358,8 @@
    1.51  
    1.52  fun proof'' f = Toplevel.proof' (f o cond_print_result_rule);
    1.53  
    1.54 +end;
    1.55 +
    1.56  
    1.57  (* local endings *)
    1.58  
    1.59 @@ -373,8 +384,8 @@
    1.60    let
    1.61      val state = ProofHistory.current prf;
    1.62      val _ = if Proof.at_bottom state then () else raise Toplevel.UNDEF;
    1.63 -    val (thy, res) = finish state;
    1.64 -  in print_result res; thy end);
    1.65 +    val (thy, res as {kind, name, thm}) = finish state;
    1.66 +  in print_result res; Context.setmp (Some thy) (Present.result kind name) thm; thy end);
    1.67  
    1.68  val global_qed = global_result o Method.global_qed o apsome Comment.ignore_interest;
    1.69  val global_terminal_proof = global_result o Method.global_terminal_proof o ignore_interests;
     2.1 --- a/src/Pure/Thy/browser_info.ML	Tue Sep 21 23:06:50 1999 +0200
     2.2 +++ b/src/Pure/Thy/browser_info.ML	Wed Sep 22 20:57:51 1999 +0200
     2.3 @@ -18,6 +18,8 @@
     2.4    val theory_source: string -> (string, 'a) Source.source -> unit
     2.5    val begin_theory: string -> string list -> (Path.T * bool) list -> theory -> theory
     2.6    val end_theory: string -> unit
     2.7 +  val result: string -> string -> thm -> unit
     2.8 +  val results: string -> string -> thm list -> unit
     2.9    val theorem: string -> thm -> unit
    2.10    val theorems: string -> thm list -> unit
    2.11    val setup: (theory -> theory) list
    2.12 @@ -31,7 +33,8 @@
    2.13  
    2.14  val output_path = Path.variable "ISABELLE_BROWSER_INFO";
    2.15  
    2.16 -fun top_path sess_path offset = Path.append (Path.appends (replicate (offset + length sess_path) Path.parent));
    2.17 +fun top_path sess_path offset =
    2.18 +  Path.append (Path.appends (replicate (offset + length sess_path) Path.parent));
    2.19  
    2.20  val html_ext = Path.ext "html";
    2.21  val html_path = html_ext o Path.basic;
    2.22 @@ -359,8 +362,10 @@
    2.23  
    2.24  fun end_theory _ = ();
    2.25  
    2.26 -fun theorem name thm = with_session () (fn _ => with_context add_html (HTML.theorem name thm));
    2.27 -fun theorems name thms = with_session () (fn _ => with_context add_html (HTML.theorems name thms));
    2.28 +fun result k a thm = with_session () (fn _ => with_context add_html (HTML.result k a thm));
    2.29 +fun results k a thms = with_session () (fn _ => with_context add_html (HTML.results k a thms));
    2.30 +fun theorem a thm = with_session () (fn _ => with_context add_html (HTML.theorem a thm));
    2.31 +fun theorems a thms = with_session () (fn _ => with_context add_html (HTML.theorems a thms));
    2.32  fun section s = with_session () (fn _ => with_context add_html (HTML.section s));
    2.33  
    2.34  
     3.1 --- a/src/Pure/Thy/html.ML	Tue Sep 21 23:06:50 1999 +0200
     3.2 +++ b/src/Pure/Thy/html.ML	Wed Sep 22 20:57:51 1999 +0200
     3.3 @@ -32,6 +32,8 @@
     3.4      (Url.T option * Url.T * bool option) list -> text -> text
     3.5    val end_theory: text
     3.6    val ml_file: Url.T -> string -> text
     3.7 +  val result: string -> string -> thm -> text
     3.8 +  val results: string -> string -> thm list -> text
     3.9    val theorem: string -> thm -> text
    3.10    val theorems: string -> thm list -> text
    3.11    val section: string -> text
    3.12 @@ -242,15 +244,26 @@
    3.13  
    3.14  (* theorems *)
    3.15  
    3.16 +local
    3.17 +
    3.18  val string_of_thm =
    3.19    Pretty.setmp_margin 80 Pretty.string_of o
    3.20      Display.pretty_thm_no_quote o #1 o Drule.freeze_thaw;
    3.21  
    3.22  fun thm th = preform (prefix_lines "  " (html_mode string_of_thm th));
    3.23  
    3.24 -fun theorem a th = para (keyword "theorem" ^ " " ^ name (a ^ ":") ^ "\n" ^ thm th);
    3.25 -fun theorems a ths =
    3.26 -  para (cat_lines ((keyword "theorems" ^ " " ^ name (a ^ ":")) :: map thm ths));
    3.27 +fun thm_name "" = ""
    3.28 +  | thm_name a = " " ^ name (a ^ ":");
    3.29 +
    3.30 +in
    3.31 +
    3.32 +fun result k a th = para (keyword k ^ thm_name a ^ "\n" ^ thm th);
    3.33 +fun results k a ths = para (cat_lines ((keyword k ^ thm_name a) :: map thm ths));
    3.34 +
    3.35 +val theorem = result "theorem";
    3.36 +val theorems = results "theorems";
    3.37 +
    3.38 +end;
    3.39  
    3.40  
    3.41  (* section *)