HTML markup elements.
authorwenzelm
Tue Mar 09 12:12:45 1999 +0100 (1999-03-09)
changeset 63243b7111b360b1
parent 6323 e5b3e46d5dbd
child 6325 2822885f5e02
HTML markup elements.
src/Pure/Thy/html.ML
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/Thy/html.ML	Tue Mar 09 12:12:45 1999 +0100
     1.3 @@ -0,0 +1,185 @@
     1.4 +(*  Title:      Pure/Thy/HTML.ML
     1.5 +    ID:         $Id$
     1.6 +    Author:     Markus Wenzel, TU Muenchen
     1.7 +
     1.8 +HTML markup elements.
     1.9 +*)
    1.10 +
    1.11 +signature HTML =
    1.12 +sig
    1.13 +  val output: string -> string
    1.14 +  val output_width: string -> string * real
    1.15 +  type text (* = string *)
    1.16 +  val plain: string -> text
    1.17 +  val name: string -> text
    1.18 +  val keyword: string -> text
    1.19 +  val file_name: string -> text
    1.20 +  val file_path: Path.T -> text
    1.21 +  val para: text -> text
    1.22 +  val href_name: string -> text -> text
    1.23 +  val href_path: Path.T -> text -> text
    1.24 +  val preform: text -> text
    1.25 +  val verbatim: string -> text
    1.26 +  val begin_document: string -> text
    1.27 +  val end_document: text
    1.28 +  val insert_here: text
    1.29 +  val source: (string, 'a) Source.source -> text
    1.30 +  val begin_theory: Path.T * string -> string -> string list -> ((Path.T * Path.T) * bool) list
    1.31 +    -> text -> text
    1.32 +  val end_theory: text
    1.33 +  val ml_file: Path.T -> string -> text
    1.34 +  val conclude_theory: text
    1.35 +  val theorem: string -> thm -> text
    1.36 +  val section: string -> text
    1.37 +  val setup: (theory -> theory) list
    1.38 +end;
    1.39 +
    1.40 +structure HTML: HTML =
    1.41 +struct
    1.42 +
    1.43 +
    1.44 +(** HTML print modes **)
    1.45 +
    1.46 +(* mode *)
    1.47 +
    1.48 +val htmlN = "HTML";
    1.49 +fun html_mode f x = setmp print_mode [htmlN] f x;
    1.50 +
    1.51 +
    1.52 +(* symbol output *)
    1.53 +
    1.54 +val escape = fn "<" => "&lt;" | ">" => "&gt;" | "&" => "&amp;" | c => c;
    1.55 +
    1.56 +val output_chars = implode o map escape;
    1.57 +
    1.58 +fun output s =
    1.59 +  if not (exists_string (equal "<" orf equal ">" orf equal "&") s) then s
    1.60 +  else implode (map escape (explode s));        (*sic!*)
    1.61 +
    1.62 +fun output_width s = (output s, real (size s));
    1.63 +
    1.64 +val _ = Symbol.add_mode htmlN output_width;
    1.65 +
    1.66 +
    1.67 +(* token translations *)
    1.68 +
    1.69 +fun tagit bg en = apfst (enclose bg en) o output_width;
    1.70 +fun color col = tagit ("<font color=" ^ quote col ^ ">") "</font>";
    1.71 +
    1.72 +val html_trans =
    1.73 + [("class", color "red"),
    1.74 +  ("tfree", color "purple"),
    1.75 +  ("tvar",  color "purple"),
    1.76 +  ("free",  color "blue"),
    1.77 +  ("bound", color "green"),
    1.78 +  ("var",   color "blue"),
    1.79 +  ("xnum",  color "yellow"),
    1.80 +  ("xstr",  color "brown")];
    1.81 +
    1.82 +
    1.83 +
    1.84 +(** HTML markup **)
    1.85 +
    1.86 +type text = string;
    1.87 +
    1.88 +
    1.89 +(* atoms *)
    1.90 +
    1.91 +val plain = output;
    1.92 +fun name s = "<i>" ^ output s ^ "</i>";
    1.93 +fun keyword s = "<b>" ^ output s ^ "</b>";
    1.94 +fun file_name s = "<tt>" ^ output s ^ "</tt>";
    1.95 +val file_path = file_name o Path.pack;
    1.96 +
    1.97 +
    1.98 +(* misc *)
    1.99 +
   1.100 +fun para txt = "\n<p>\n" ^ txt ^ "\n</p>\n";
   1.101 +fun href_name s txt = "<a href=" ^ quote s ^ ">" ^ txt ^ "</a>";
   1.102 +fun href_path path txt = href_name (Path.pack path) txt;
   1.103 +fun preform txt = "<pre>" ^ txt ^ "</pre>";
   1.104 +val verbatim = preform o output;
   1.105 +
   1.106 +
   1.107 +(* document *)
   1.108 +
   1.109 +fun begin_document title =
   1.110 +  let val txt = plain title in
   1.111 +    "<html>\n\
   1.112 +    \<head>\n\
   1.113 +    \<title>" ^ txt ^ "</title>\n\
   1.114 +    \</head>\n\
   1.115 +    \\n\
   1.116 +    \<body>\n\
   1.117 +    \<h1>" ^ txt ^ "</h1>\n"
   1.118 +  end;
   1.119 +
   1.120 +val end_document =
   1.121 +  "</body>\n\
   1.122 +  \</html>\n";
   1.123 +
   1.124 +val insert_here = "<!--insert--here-->";
   1.125 +
   1.126 +
   1.127 +(* theory *)
   1.128 +
   1.129 +fun source src =
   1.130 +  "\n<hr>\n<pre>" ^ output_chars (Source.exhaust src) ^ "</pre>\n<hr>\n";
   1.131 +
   1.132 +
   1.133 +local
   1.134 +  fun file ((p, p'), loadit) =
   1.135 +    href_path p' ((if not loadit then enclose "(" ")" else I) (file_path p));
   1.136 +
   1.137 +  fun suffix_last _ [] = []
   1.138 +    | suffix_last s lst = let val (xs, x) = split_last lst in xs @ [x ^ s] end;
   1.139 +
   1.140 +  val plus_names = space_implode " + " o map name;
   1.141 +
   1.142 +  fun theory (back_path, back_name) A =
   1.143 +    begin_document ("Theory " ^ A) ^ "\n" ^
   1.144 +    href_path back_path "Back" ^ " to the index of " ^ plain back_name ^ "\n<p>\n" ^
   1.145 +    keyword "theory" ^ " " ^ name A ^ " = ";
   1.146 +in
   1.147 +
   1.148 +fun begin_theory back A Bs [] body = theory back A ^ plus_names (suffix_last ":" Bs) ^ "\n" ^ body
   1.149 +  | begin_theory back A Bs Ps body =
   1.150 +      theory back A ^ plus_names Bs ^
   1.151 +      "<br>" ^ keyword "files" ^ " " ^ space_implode " + " (map file Ps) ^ ":" ^ "\n" ^ body;
   1.152 +end;
   1.153 +
   1.154 +val end_theory = "";
   1.155 +val conclude_theory = end_document;
   1.156 +
   1.157 +
   1.158 +(* ML file *)
   1.159 +
   1.160 +fun ml_file path str =
   1.161 +  begin_document ("File " ^ Path.pack path) ^
   1.162 +  "\n<hr>\n" ^ verbatim str ^ "\n<hr>\n" ^ end_document;
   1.163 +
   1.164 +
   1.165 +(* theorem *)
   1.166 +
   1.167 +(* FIXME improve freeze_thaw (?) *)
   1.168 +val string_of_thm =
   1.169 +  Pretty.setmp_margin 80 Pretty.string_of o
   1.170 +    Display.pretty_thm_no_quote o #1 o Drule.freeze_thaw;
   1.171 +
   1.172 +fun thm th = preform (prefix_lines "  " (html_mode string_of_thm th));
   1.173 +fun theorem a th = para (keyword "theorem" ^ " " ^ name (a ^ ":") ^ "\n" ^ thm th);
   1.174 +
   1.175 +
   1.176 +(* section *)
   1.177 +
   1.178 +fun section heading = "\n\n<h2>" ^ plain heading ^ "</h2>\n";
   1.179 +
   1.180 +
   1.181 +
   1.182 +(** theory setup **)
   1.183 +
   1.184 +val setup =
   1.185 + [Theory.add_mode_tokentrfuns htmlN html_trans];
   1.186 +
   1.187 +
   1.188 +end;