# HG changeset patch
# User wenzelm
# Date 1184102991 -7200
# Node ID 6e95ed5f64da1497def54e83052450f08cf503cd
# Parent  4fff46d5faaa2f242e52f3c3bfd957570b451f7c
export html_mode, begin_document, end_document;

diff -r 4fff46d5faaa -r 6e95ed5f64da src/Pure/Thy/html.ML
--- a/src/Pure/Thy/html.ML	Tue Jul 10 23:29:49 2007 +0200
+++ b/src/Pure/Thy/html.ML	Tue Jul 10 23:29:51 2007 +0200
@@ -7,6 +7,7 @@
 
 signature HTML =
 sig
+  val html_mode: ('a -> 'b) -> 'a -> 'b
   type text = string
   val plain: string -> text
   val name: string -> text
@@ -22,6 +23,8 @@
   val preform: text -> text
   val verbatim: string -> text
   val with_charset: string -> ('a -> 'b) -> 'a -> 'b
+  val begin_document: string -> text
+  val end_document: text
   val begin_index: Url.T * string -> Url.T * string -> (Url.T * string) list -> Url.T -> text
   val end_index: text
   val applet_pages: string -> Url.T * string -> (string * string) list