# HG changeset patch # User wenzelm # Date 1218472671 -7200 # Node ID c073006e0137b149d9fb7cefd94e9204a9527140 # Parent edafacb690a3639a425b6be40e84de1e98e7b180 produce XHTML 1.0 Transitional; tuned charset name; renamed Markup.class to Markup.tclass, to avoid potential conflicts with spacial meaning in markup languages (e.g. HTML); diff -r edafacb690a3 -r c073006e0137 src/Pure/Thy/html.ML --- a/src/Pure/Thy/html.ML Mon Aug 11 18:37:49 2008 +0200 +++ b/src/Pure/Thy/html.ML Mon Aug 11 18:37:51 2008 +0200 @@ -241,8 +241,7 @@ fun span s = ("", ""); -val _ = Markup.add_mode htmlN (fn (name, props) => - if name = Markup.classN then span "tclass" else span name); +val _ = Markup.add_mode htmlN (fn (name, _) => span name); @@ -270,29 +269,31 @@ | href_opt_path (SOME p) txt = href_path p txt; fun para txt = "\n

" ^ txt ^ "

\n"; -fun preform txt = "
" ^ txt ^ "
"; +fun preform txt = "
" ^ txt ^ "
"; val verbatim = preform o output; (* document *) -val charset = ref "iso-8859-1"; +val charset = ref "ISO-8859-1"; fun with_charset s = setmp_noncritical charset s; fun begin_document title = - "\n\ - \\n\ - \\n\ - \\n\ - \\n\ - \" ^ plain (title ^ " (" ^ Distribution.version ^ ")") ^ "\n\ - \\n\ - \\n\ - \\n\ - \\n\ - \
\ - \

" ^ plain title ^ "

\n" + let val cs = ! charset in + "\n\ + \\n\ + \\n\ + \\n\ + \\n\ + \" ^ plain (title ^ " (" ^ Distribution.version ^ ")") ^ "\n\ + \\n\ + \\n\ + \\n\ + \\n\ + \
\ + \

" ^ plain title ^ "

\n" + end; val end_document = "\n
\n\n\n"; @@ -306,8 +307,8 @@ fun begin_index up (index_path, session) docs graph = begin_document ("Index of " ^ session) ^ up_link up ^ para ("View " ^ href_path graph "theory dependencies" ^ - implode (map (fn (p, name) => "
\nView " ^ href_path p name) docs)) ^ - "\n
\n
\n
\n

Theories

\n
\n
\n
\n

Theories

\n
\n
\n
\n\ + "\n
\n
\n
\n\ \\n\ \\n\ - \\n
" ^ end_document) + \\n
" ^ end_document) end; in map applet_page sizes end; -fun entry (p, s) = "
  • " ^ href_path p (plain s) ^ "\n"; +fun entry (p, s) = "
  • " ^ href_path p (plain s) ^ "
    • \n"; val theory_entry = entry; fun session_entries [] = "" | session_entries es = - "\n
    \n
    \n
    \n\ + "\n
    \n
    \n
    \n\ \

    Sessions

    \n"; (* theory *) fun verbatim_source ss = - "\n
    \n
    \n
    \n
    " ^
+  "\n
    \n
    \n
    \n
    " ^
   implode (output_symbols ss) ^
-  "
    \n
    \n
    \n
    \n"; + "\n
    \n
    \n
    \n"; local @@ -368,14 +369,14 @@ fun imports Bs = keyword "imports" ^ " " ^ space_implode " " (map (uncurry href_opt_path o apsnd name) Bs); - fun uses Ps = keyword "uses" ^ " " ^ space_implode " " (map file Ps) ^ "
    \n"; + fun uses Ps = keyword "uses" ^ " " ^ space_implode " " (map file Ps) ^ "
    \n"; in fun begin_theory up A Bs Ps body = - theory up A ^ "
    \n" ^ - imports Bs ^ "
    \n" ^ + theory up A ^ "
    \n" ^ + imports Bs ^ "
    \n" ^ (if null Ps then "" else uses Ps) ^ - keyword "begin" ^ "
    \n" ^ + keyword "begin" ^ "
    \n" ^ body; end; @@ -387,9 +388,9 @@ fun ml_file path str = begin_document ("File " ^ Url.implode path) ^ - "\n
    \n
    \n" ^ + "\n
    \n
    \n" ^ verbatim str ^ - "\n
    \n
    \n
    \n" ^ + "\n
    \n
    \n
    \n" ^ end_document;