--- a/src/HOL/ex/ROOT.ML Fri Dec 03 20:38:58 2010 +0100
+++ b/src/HOL/ex/ROOT.ML Fri Dec 03 21:30:41 2010 +0100
@@ -8,7 +8,10 @@
"Efficient_Nat_examples",
"FuncSet",
"Eval_Examples",
- "Normalization_by_Evaluation"
+ "Normalization_by_Evaluation",
+ "Hebrew",
+ "Chinese",
+ "Serbian"
];
use_thys [
@@ -71,9 +74,6 @@
"Birthday_Paradoxon"
];
-HTML.with_charset "utf-8" (no_document use_thys)
- ["Hebrew", "Chinese", "Serbian"];
-
use_thy "SVC_Oracle";
if getenv "SVC_HOME" = "" then ()
else use_thy "svc_test";
--- a/src/Pure/Thy/html.ML Fri Dec 03 20:38:58 2010 +0100
+++ b/src/Pure/Thy/html.ML Fri Dec 03 21:30:41 2010 +0100
@@ -20,7 +20,6 @@
val para: text -> text
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
@@ -276,25 +275,20 @@
(* document *)
-val charset = Unsynchronized.ref "ISO-8859-1";
-fun with_charset s = Unsynchronized.setmp charset s; (* FIXME unreliable *)
-
fun begin_document title =
- let val cs = ! charset in
- "<?xml version=\"1.0\" encoding=\"" ^ cs ^ "\" ?>\n\
- \<!DOCTYPE html PUBLIC \"-//W3C//DTD XHTML 1.0 Transitional//EN\" \
- \\"http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd\">\n\
- \<html xmlns=\"http://www.w3.org/1999/xhtml\">\n\
- \<head>\n\
- \<meta http-equiv=\"Content-Type\" content=\"text/html; charset=" ^ cs ^ "\"/>\n\
- \<title>" ^ plain (title ^ " (" ^ Distribution.version ^ ")") ^ "</title>\n\
- \<link media=\"all\" rel=\"stylesheet\" type=\"text/css\" href=\"isabelle.css\"/>\n\
- \</head>\n\
- \\n\
- \<body>\n\
- \<div class=\"head\">\
- \<h1>" ^ plain title ^ "</h1>\n"
- end;
+ "<?xml version=\"1.0\" encoding=\"utf-8\" ?>\n\
+ \<!DOCTYPE html PUBLIC \"-//W3C//DTD XHTML 1.0 Transitional//EN\" \
+ \\"http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd\">\n\
+ \<html xmlns=\"http://www.w3.org/1999/xhtml\">\n\
+ \<head>\n\
+ \<meta http-equiv=\"Content-Type\" content=\"text/html; charset=utf-8\"/>\n\
+ \<title>" ^ plain (title ^ " (" ^ Distribution.version ^ ")") ^ "</title>\n\
+ \<link media=\"all\" rel=\"stylesheet\" type=\"text/css\" href=\"isabelle.css\"/>\n\
+ \</head>\n\
+ \\n\
+ \<body>\n\
+ \<div class=\"head\">\
+ \<h1>" ^ plain title ^ "</h1>\n";
val end_document = "\n</div>\n</body>\n</html>\n";