# HG changeset patch
# User wenzelm
# Date 1126973490 -7200
# Node ID 6e9d910c38372c44ffbf3ac5ef955b6bab4d0832
# Parent 4524bf3026d38f7c4ade2a2c6753a78a992a16d6
added with_charset: string -> ('a -> 'b) -> 'a -> 'b;
diff -r 4524bf3026d3 -r 6e9d910c3837 src/Pure/Thy/html.ML
--- a/src/Pure/Thy/html.ML Sat Sep 17 18:11:29 2005 +0200
+++ b/src/Pure/Thy/html.ML Sat Sep 17 18:11:30 2005 +0200
@@ -22,6 +22,7 @@
val para: text -> text
val preform: text -> text
val verbatim: string -> text
+ val with_charset: string -> ('a -> 'b) -> 'a -> 'b
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
@@ -288,13 +289,16 @@
(* document *)
+val charset = ref "iso-8859-1";
+fun with_charset s = setmp charset s;
+
fun begin_document title =
"\n\
\\n\
\\n\
\\n\
- \\n\
+ \\n\
\" ^ plain (title ^ " (" ^ version ^ ")") ^ "\n\
\\n\
\\n\