# HG changeset patch
# User clasohm
# Date 826028338 -3600
# Node ID 31ad553d018b85315e0a7741072268ab696e9a58
# Parent  3f51f0945a3efaadb0213134c08c19f7241a8e85
added function "section" for HTML section headings

diff -r 3f51f0945a3e -r 31ad553d018b src/Pure/Thy/thy_read.ML
--- a/src/Pure/Thy/thy_read.ML	Tue Mar 05 11:38:41 1996 +0100
+++ b/src/Pure/Thy/thy_read.ML	Tue Mar 05 13:18:58 1996 +0100
@@ -98,6 +98,7 @@
   val make_html     : bool ref
   val init_html     : unit -> unit
   val finish_html   : unit -> unit
+  val section       : string -> unit
 end;
 
 
@@ -1008,6 +1009,17 @@
 
 (** Store theorems **)
 
+(*Makes HTML title for list of theorems; as this list may be empty and we
+  don't want a title in that case, mk_theorems_title is only invoked when
+  something is added to the list*)
+fun mk_theorems_title out =
+  if not (!cur_has_title) then
+    (cur_has_title := true;
+     output (out, "<HR><H2>Theorems proved in <A HREF = \"" ^
+                  (!cur_thyname) ^ ".ML\">" ^ (!cur_thyname) ^
+                  ".ML</A>:</H2>\n"))
+  else ();
+
 (*Store a theorem in the thy_info of its theory,
   and in the theory's HTML file*)
 fun store_thm (name, thm) =
@@ -1033,12 +1045,7 @@
             | escape (c::s)   = c ^ escape s;
       in case !cur_htmlfile of
              Some out =>
-               (if not (!cur_has_title) then
-                  (cur_has_title := true;
-                   output (out, "<HR><H2>Theorems proved in <A HREF = \"" ^
-                                (!cur_thyname) ^ ".ML\">" ^ (!cur_thyname) ^
-                                ".ML</A>:</H2>\n"))
-                else ();
+               (mk_theorems_title out;
                 output (out, "<EM>" ^ name ^ "</EM>\n<PRE>" ^
                              escape (explode (string_of_thm (freeze thm))) ^
                              "</PRE><P>\n")
@@ -1258,6 +1265,13 @@
         else link_directory ()
   end;
 
+(*Append section heading to HTML file*)
+fun section s =
+  case !cur_htmlfile of
+      Some out => (mk_theorems_title out;
+                   output (out, "<H3>" ^ s ^ "</H3>\n"))
+    | None => ();
+
 
 (*** Print theory ***)