src/Pure/Thy/html.ML
changeset 7572 6e6dafacbc28
parent 7408 1ec1567c1307
child 7634 c326808da921
     1.1 --- a/src/Pure/Thy/html.ML	Tue Sep 21 23:06:50 1999 +0200
     1.2 +++ b/src/Pure/Thy/html.ML	Wed Sep 22 20:57:51 1999 +0200
     1.3 @@ -32,6 +32,8 @@
     1.4      (Url.T option * Url.T * bool option) list -> text -> text
     1.5    val end_theory: text
     1.6    val ml_file: Url.T -> string -> text
     1.7 +  val result: string -> string -> thm -> text
     1.8 +  val results: string -> string -> thm list -> text
     1.9    val theorem: string -> thm -> text
    1.10    val theorems: string -> thm list -> text
    1.11    val section: string -> text
    1.12 @@ -242,15 +244,26 @@
    1.13  
    1.14  (* theorems *)
    1.15  
    1.16 +local
    1.17 +
    1.18  val string_of_thm =
    1.19    Pretty.setmp_margin 80 Pretty.string_of o
    1.20      Display.pretty_thm_no_quote o #1 o Drule.freeze_thaw;
    1.21  
    1.22  fun thm th = preform (prefix_lines "  " (html_mode string_of_thm th));
    1.23  
    1.24 -fun theorem a th = para (keyword "theorem" ^ " " ^ name (a ^ ":") ^ "\n" ^ thm th);
    1.25 -fun theorems a ths =
    1.26 -  para (cat_lines ((keyword "theorems" ^ " " ^ name (a ^ ":")) :: map thm ths));
    1.27 +fun thm_name "" = ""
    1.28 +  | thm_name a = " " ^ name (a ^ ":");
    1.29 +
    1.30 +in
    1.31 +
    1.32 +fun result k a th = para (keyword k ^ thm_name a ^ "\n" ^ thm th);
    1.33 +fun results k a ths = para (cat_lines ((keyword k ^ thm_name a) :: map thm ths));
    1.34 +
    1.35 +val theorem = result "theorem";
    1.36 +val theorems = results "theorems";
    1.37 +
    1.38 +end;
    1.39  
    1.40  
    1.41  (* section *)