# HG changeset patch
# User wenzelm
# Date 947068728 -3600
# Node ID 6ae943d080de66049f33409ec762704344d8615a
# Parent 4187ef29d8264fd4d4903a7818cc3dbfbf51922a
chapter;
diff -r 4187ef29d826 -r 6ae943d080de src/Pure/Thy/html.ML
--- a/src/Pure/Thy/html.ML Wed Jan 05 11:37:44 2000 +0100
+++ b/src/Pure/Thy/html.ML Wed Jan 05 11:38:48 2000 +0100
@@ -37,6 +37,7 @@
val results: string -> string -> thm list -> text
val theorem: string -> thm -> text
val theorems: string -> thm list -> text
+ val chapter: string -> text
val section: string -> text
val subsection: string -> text
val subsubsection: string -> text
@@ -271,6 +272,7 @@
(* sections *)
+fun chapter heading = "\n\n
" ^ plain heading ^ "
\n";
fun section heading = "\n\n" ^ plain heading ^ "
\n";
fun subsection heading = "\n\n" ^ plain heading ^ "
\n";
fun subsubsection heading = "\n\n" ^ plain heading ^ "
\n";
diff -r 4187ef29d826 -r 6ae943d080de src/Pure/Thy/present.ML
--- a/src/Pure/Thy/present.ML Wed Jan 05 11:37:44 2000 +0100
+++ b/src/Pure/Thy/present.ML Wed Jan 05 11:38:48 2000 +0100
@@ -27,6 +27,7 @@
val results: string -> string -> thm list -> unit
val theorem: string -> thm -> unit
val theorems: string -> thm list -> unit
+ val chapter: string -> unit
val subsection: string -> unit
val subsubsection: string -> unit
val setup: (theory -> theory) list
@@ -427,6 +428,7 @@
fun results k a thms = with_session () (fn _ => with_context add_html (HTML.results k a thms));
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 chapter s = with_session () (fn _ => with_context add_html (HTML.chapter s));
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));