# HG changeset patch # User wenzelm # Date 1291408241 -3600 # Node ID 3f697c636fa1fbfad010aa6fe6783e27430786ea # Parent b8703f63bfb2bc19c83e9e45101d762d2cd25deb eliminated fragile HTML.with_charset -- always use utf-8; diff -r b8703f63bfb2 -r 3f697c636fa1 src/HOL/ex/ROOT.ML --- 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"; diff -r b8703f63bfb2 -r 3f697c636fa1 src/Pure/Thy/html.ML --- 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 - "\n\ - \\n\ - \\n\ - \\n\ - \\n\ - \" ^ plain (title ^ " (" ^ Distribution.version ^ ")") ^ "\n\ - \\n\ - \\n\ - \\n\ - \\n\ - \

\ - \

" ^ plain title ^ "

\n" - end; + "\n\ + \\n\ + \\n\ + \\n\ + \\n\ + \" ^ plain (title ^ " (" ^ Distribution.version ^ ")") ^ "\n\ + \\n\ + \\n\ + \\n\ + \\n\ + \

\ + \

" ^ plain title ^ "

\n"; val end_document = "\n

\n\n\n";