# HG changeset patch
# User wenzelm
# Date 938605789 -7200
# Node ID c326808da921555ec84e5fa5d3eb2ef4db36dcc3
# Parent  838077e40a460480b196eee0b9fc04455cfcf848
more sections;

diff -r 838077e40a46 -r c326808da921 src/Pure/Thy/browser_info.ML
--- a/src/Pure/Thy/browser_info.ML	Wed Sep 29 13:49:27 1999 +0200
+++ b/src/Pure/Thy/browser_info.ML	Wed Sep 29 13:49:49 1999 +0200
@@ -22,6 +22,8 @@
   val results: string -> string -> thm list -> unit
   val theorem: string -> thm -> unit
   val theorems: string -> thm list -> unit
+  val subsection: string -> unit
+  val subsubsection: string -> unit
   val setup: (theory -> theory) list
 end;
 
@@ -367,6 +369,8 @@
 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));
+fun subsection s = with_session () (fn _ => with_context add_html (HTML.subsection s));
+fun subsubsection s = with_session () (fn _ => with_context add_html (HTML.subsubsection s));
 
 
 
diff -r 838077e40a46 -r c326808da921 src/Pure/Thy/html.ML
--- a/src/Pure/Thy/html.ML	Wed Sep 29 13:49:27 1999 +0200
+++ b/src/Pure/Thy/html.ML	Wed Sep 29 13:49:49 1999 +0200
@@ -37,6 +37,8 @@
   val theorem: string -> thm -> text
   val theorems: string -> thm list -> text
   val section: string -> text
+  val subsection: string -> text
+  val subsubsection: string -> text
   val setup: (theory -> theory) list
 end;
 
@@ -266,9 +268,11 @@
 end;
 
 
-(* section *)
+(* sections *)
 
 fun section heading = "\n\n<h2>" ^ plain heading ^ "</h2>\n";
+fun subsection heading = "\n\n<h3>" ^ plain heading ^ "</h3>\n";
+fun subsubsection heading = "\n\n<h4>" ^ plain heading ^ "</h4>\n";