# HG changeset patch # User kleing # Date 1081806771 -7200 # Node ID 0a7743e2f8dd727d1b353906dcd0705c967ccb36 # Parent 0417e7ed93fdba293b1ca9525612f35b76c9c51a use css use Graphrowser.jar instead of .class files diff -r 0417e7ed93fd -r 0a7743e2f8dd src/Pure/Thy/html.ML --- a/src/Pure/Thy/html.ML Mon Apr 12 23:52:15 2004 +0200 +++ b/src/Pure/Thy/html.ML Mon Apr 12 23:52:51 2004 +0200 @@ -141,17 +141,17 @@ (* token translations *) -fun color col = - apfst (enclose ("") "") o output_width; +fun style stl = + apfst (enclose ("") "") o output_width; val html_trans = - [("class", color "red"), - ("tfree", color "purple"), - ("tvar", color "purple"), - ("free", color "blue"), - ("bound", color "green"), - ("var", color "blue"), - ("xstr", color "brown")]; + [("class", style "tclass"), + ("tfree", style "tfree"), + ("tvar", style "tvar"), + ("free", style "free"), + ("bound", style "bound"), + ("var", style "var"), + ("xstr", style "xstr")]; @@ -163,9 +163,9 @@ (* atoms *) val plain = output; -fun name s = "" ^ output s ^ ""; -fun keyword s = "" ^ output s ^ ""; -fun file_name s = "" ^ output s ^ ""; +fun name s = "" ^ output s ^ ""; +fun keyword s = "" ^ output s ^ ""; +fun file_name s = "" ^ output s ^ ""; val file_path = file_name o Url.pack; @@ -194,12 +194,14 @@ \\n\ \\n\ \" ^ plain (title ^ " (" ^ version ^ ")") ^ "\n\ + \\n\ \\n\ \\n\ \\n\ + \
\ \

" ^ plain title ^ "

\n" -val end_document = "\n\n\n"; +val end_document = "\n
\n\n\n"; fun gen_link how (path, name) = para (href_path path how ^ " to index of " ^ plain name); val up_link = gen_link "Up"; @@ -213,7 +215,7 @@ para ("View " ^ href_path graph "theory dependencies" ^ (case opt_readme of None => "" | Some p => "
\nView " ^ href_path p "README") ^ (case opt_doc of None => "" | Some p => "
\nView " ^ href_path p "document")) ^ - "\n
\n\n

Theories

\n