1.1 --- a/src/Pure/Thy/html.ML	Wed Sep 01 21:05:48 1999 +0200
     1.2 +++ b/src/Pure/Thy/html.ML	Wed Sep 01 21:06:27 1999 +0200
     1.3 @@ -29,10 +29,11 @@
     1.4    val session_entries: (Url.T * string) list -> text
     1.5    val source: (string, 'a) Source.source -> text
     1.6    val begin_theory: Url.T * string -> string -> (Url.T option * string) list ->
     1.7 -    (Url.T option * Url.T * bool) list -> text -> text
     1.8 +    (Url.T option * Url.T * bool option) list -> text -> text
     1.9    val end_theory: text
    1.10    val ml_file: Url.T -> string -> text
    1.11    val theorem: string -> thm -> text
    1.12 +  val theorems: string -> thm list -> text
    1.13    val section: string -> text
    1.14    val setup: (theory -> theory) list
    1.15  end;
    1.16 @@ -211,9 +212,11 @@
    1.17  
    1.18  
    1.19  local
    1.20 -  fun file (opt_ref, path, loadit) = href_opt_path opt_ref
    1.21 -    ((if not loadit then enclose "(" ")" else I) (file_path path));
    1.22 +  fun encl None = enclose "[" "]"
    1.23 +    | encl (Some false) = enclose "(" ")"
    1.24 +    | encl (Some true) = I;
    1.25  
    1.26 +  fun file (opt_ref, path, loadit) = href_opt_path opt_ref (encl loadit (file_path path));
    1.27    val files = space_implode " + " o map file;
    1.28    val parents = space_implode " + " o map (uncurry href_opt_path o apsnd name);
    1.29  
    1.30 @@ -237,14 +240,17 @@
    1.31    "\n<hr>\n" ^ verbatim str ^ "\n<hr>\n" ^ end_document;
    1.32  
    1.33  
    1.34 -(* theorem *)
    1.35 +(* theorems *)
    1.36  
    1.37 -val string_of_thm =             (* FIXME improve freeze_thaw (?) *)
    1.38 +val string_of_thm =
    1.39    Pretty.setmp_margin 80 Pretty.string_of o
    1.40      Display.pretty_thm_no_quote o #1 o Drule.freeze_thaw;
    1.41  
    1.42  fun thm th = preform (prefix_lines "  " (html_mode string_of_thm th));
    1.43 +
    1.44  fun theorem a th = para (keyword "theorem" ^ " " ^ name (a ^ ":") ^ "\n" ^ thm th);
    1.45 +fun theorems a ths =
    1.46 +  para (cat_lines ((keyword "theorems" ^ " " ^ name (a ^ ":")) :: map thm ths));
    1.47  
    1.48  
    1.49  (* section *)