src/Pure/Thy/html.ML
author kleing
Wed Apr 14 14:13:05 2004 +0200 (2004-04-14)
changeset 14565 c6dc17aab88a
parent 14558 726f6761c562
child 14571 b88d5f9e02e1
permissions -rw-r--r--
use more symbols in HTML output
     1 (*  Title:      Pure/Thy/HTML.ML
     2     ID:         $Id$
     3     Author:     Markus Wenzel and Stefan Berghofer, TU Muenchen
     4     License:    GPL (GNU GENERAL PUBLIC LICENSE)
     5 
     6 HTML presentation elements.
     7 *)
     8 
     9 signature HTML =
    10 sig
    11   val output: string -> string
    12   val output_width: string -> string * real
    13   type text (* = string *)
    14   val plain: string -> text
    15   val name: string -> text
    16   val keyword: string -> text
    17   val file_name: string -> text
    18   val file_path: Url.T -> text
    19   val href_name: string -> text -> text
    20   val href_path: Url.T -> text -> text
    21   val href_opt_name: string option -> text -> text
    22   val href_opt_path: Url.T option -> text -> text
    23   val para: text -> text
    24   val preform: text -> text
    25   val verbatim: string -> text
    26   val begin_index: Url.T * string -> Url.T * string -> Url.T option
    27     -> Url.T option -> Url.T -> text
    28   val end_index: text
    29   val applet_pages: string -> Url.T * string -> (string * string) list
    30   val theory_entry: Url.T * string -> text
    31   val session_entries: (Url.T * string) list -> text
    32   val verbatim_source: Symbol.symbol list -> text
    33   val begin_theory: Url.T * string -> string -> (Url.T option * string) list ->
    34     (Url.T option * Url.T * bool option) list -> text -> text
    35   val end_theory: text
    36   val ml_file: Url.T -> string -> text
    37   val results: string -> (string * thm list) list -> text
    38   val chapter: string -> text
    39   val section: string -> text
    40   val subsection: string -> text
    41   val subsubsection: string -> text
    42   val setup: (theory -> theory) list
    43 end;
    44 
    45 structure HTML: HTML =
    46 struct
    47 
    48 
    49 (** HTML print modes **)
    50 
    51 (* mode *)
    52 
    53 val htmlN = "HTML";
    54 fun html_mode f x = setmp print_mode (htmlN :: ! print_mode) f x;
    55 
    56 
    57 (* symbol output *)
    58 
    59 local
    60   val escape = fn "<" => "&lt;" | ">" => "&gt;" | "&" => "&amp;" | c => c;
    61 
    62   val output_sym =
    63     fn "\\<spacespace>" => (2.0, "&nbsp;&nbsp;")
    64      | "\\<exclamdown>" => (1.0, "&iexcl;")
    65      | "\\<cent>" => (1.0, "&cent;")
    66      | "\\<pounds>" => (1.0, "&pound;")
    67      | "\\<currency>" => (1.0, "&curren;")
    68      | "\\<yen>" => (1.0, "&yen;")
    69      | "\\<bar>" => (1.0, "&brvbar;")
    70      | "\\<section>" => (1.0, "&sect;")
    71      | "\\<dieresis>" => (1.0, "&uml;")
    72      | "\\<copyright>" => (1.0, "&copy;")
    73      | "\\<ordfeminine>" => (1.0, "&ordf;")
    74      | "\\<guillemotleft>" => (1.0, "&laquo;")
    75      | "\\<not>" => (1.0, "&not;")
    76      | "\\<hyphen>" => (1.0, "&shy;")
    77      | "\\<registered>" => (1.0, "&reg;")
    78      | "\\<inverse>" => (1.0, "&macr;")
    79      | "\\<degree>" => (1.0, "&deg;")
    80      | "\\<plusminus>" => (1.0, "&plusmn;")
    81      | "\\<twosuperior>" => (1.0, "&sup2;")
    82      | "\\<threesuperior>" => (1.0, "&sup3;")
    83      | "\\<acute>" => (1.0, "&acute;")
    84      | "\\<mu>" => (1.0, "&micro;")
    85      | "\\<paragraph>" => (1.0, "&para;")
    86      | "\\<cdot>" => (1.0, "&middot;")
    87      | "\\<cedilla>" => (1.0, "&cedil;")
    88      | "\\<onesuperior>" => (1.0, "&sup1;")
    89      | "\\<ordmasculine>" => (1.0, "&ordm;")
    90      | "\\<guillemotright>" => (1.0, "&raquo;")
    91      | "\\<onequarter>" => (1.0, "&frac14;")
    92      | "\\<onehalf>" => (1.0, "&frac12;")
    93      | "\\<threequarters>" => (1.0, "&frac34;")
    94      | "\\<questiondown>" => (1.0, "&iquest;")
    95      | "\\<times>" => (1.0, "&times;")
    96      | "\\<emptyset>" => (1.0, "&Oslash;")
    97      | "\\<div>" => (1.0, "&divide;")
    98      | "\\<circ>" => (1.0, "&circ;")    
    99      | "\\<Alpha>" => (1.0, "&Alpha;")
   100      | "\\<Beta>" => (1.0, "&Beta;")
   101      | "\\<Gamma>" => (1.0, "&Gamma;")
   102      | "\\<Delta>" => (1.0, "&Delta;")
   103      | "\\<Epsilon>" => (1.0, "&Epsilon;")
   104      | "\\<Zeta>" => (1.0, "&Zeta;")
   105      | "\\<Eta>" => (1.0, "&Eta;")
   106      | "\\<Theta>" => (1.0, "&Theta;")
   107      | "\\<Iota>" => (1.0, "&Iota;")
   108      | "\\<Kappa>" => (1.0, "&Kappa;")
   109      | "\\<Lambda>" => (1.0, "&Lambda;")
   110      | "\\<Mu>" => (1.0, "&Mu;")
   111      | "\\<Nu>" => (1.0, "&Nu;")
   112      | "\\<Xi>" => (1.0, "&Xi;")
   113      | "\\<Omicron>" => (1.0, "&Omicron;")
   114      | "\\<Pi>" => (1.0, "&Pi;")
   115      | "\\<Rho>" => (1.0, "&Rho;")
   116      | "\\<Sigma>" => (1.0, "&Sigma;")
   117      | "\\<Tau>" => (1.0, "&Tau;")
   118      | "\\<Upsilon>" => (1.0, "&Upsilon;")
   119      | "\\<Phi>" => (1.0, "&Phi;")
   120      | "\\<Chi>" => (1.0, "&Chi;")
   121      | "\\<Psi>" => (1.0, "&Psi;")
   122      | "\\<Omega>" => (1.0, "&Omega;")
   123      | "\\<alpha>" => (1.0, "&alpha;")
   124      | "\\<beta>" => (1.0, "&beta;")
   125      | "\\<gamma>" => (1.0, "&gamma;")
   126      | "\\<delta>" => (1.0, "&delta;")
   127      | "\\<epsilon>" => (1.0, "&epsilon;")
   128      | "\\<zeta>" => (1.0, "&zeta;")
   129      | "\\<eta>" => (1.0, "&eta;")
   130      | "\\<theta>" => (1.0, "&thetasym;")
   131      | "\\<iota>" => (1.0, "&iota;")
   132      | "\\<kappa>" => (1.0, "&kappa;")
   133      | "\\<lambda>" => (1.0, "&lambda;")
   134      | "\\<mu>" => (1.0, "&mu;")
   135      | "\\<nu>" => (1.0, "&nu;")
   136      | "\\<xi>" => (1.0, "&xi;")
   137      | "\\<omicron>" => (1.0, "&omicron;")
   138      | "\\<pi>" => (1.0, "&pi;")
   139      | "\\<rho>" => (1.0, "&rho;")
   140      | "\\<sigma>" => (1.0, "&sigma;")
   141      | "\\<tau>" => (1.0, "&tau;")
   142      | "\\<upsilon>" => (1.0, "&upsilon;")
   143      | "\\<phi>" => (1.0, "&phi;")
   144      | "\\<chi>" => (1.0, "&chi;")
   145      | "\\<psi>" => (1.0, "&psi;")
   146      | "\\<omega>" => (1.0, "&omega;")
   147      | "\\<buller>" => (1.0, "&bull;")
   148      | "\\<dots>" => (1.0, "&hellip;")
   149      | "\\<Re>" => (1.0, "&real;")
   150      | "\\<Im>" => (1.0, "&image;")
   151      | "\\<wp>" => (1.0, "&weierp;")
   152      | "\\<forall>" => (1.0, "&forall;")
   153      | "\\<partial>" => (1.0, "&part;")
   154      | "\\<exists>" => (1.0, "&exist;")
   155      | "\\<emptyset>" => (1.0, "&empty;")
   156      | "\\<nabla>" => (1.0, "&nabla;")
   157      | "\\<in>" => (1.0, "&isin;")
   158      | "\\<notin>" => (1.0, "&notin;")
   159      | "\\<Prod>" => (1.0, "&prod;")
   160      | "\\<Sum>" => (1.0, "&sum;")
   161      | "\\<star>" => (1.0, "&lowast;")
   162      | "\\<propto>" => (1.0, "&prop;")
   163      | "\\<infinity>" => (1.0, "&infin;")
   164      | "\\<angle>" => (1.0, "&ang;")
   165      | "\\<and>" => (1.0, "&and;")     
   166      | "\\<or>" => (1.0, "&or;")
   167      | "\\<inter>" => (1.0, "&cap;")
   168      | "\\<union>" => (1.0, "&cup;")
   169      | "\\<sim>" => (1.0, "&sim;")
   170      | "\\<cong>" => (1.0, "&cong;")
   171      | "\\<approx>" => (1.0, "&asymp;")
   172      | "\\<noteq>" => (1.0, "&ne;")
   173      | "\\<equiv>" => (1.0, "&equiv;")
   174      | "\\<le>" => (1.0, "&le;")
   175      | "\\<ge>" => (1.0, "&ge;")
   176      | "\\<subset>" => (1.0, "&sub;")
   177      | "\\<supset>" => (1.0, "&sup;")
   178      | "\\<subseteq>" => (1.0, "&sube;")
   179      | "\\<supseteq>" => (1.0, "&supe;")
   180      | "\\<oplus>" => (1.0, "&oplus;")
   181      | "\\<otimes>" => (1.0, "&otimes;")
   182      | "\\<bottom>" => (1.0, "&perp;")
   183      | "\\<lceil>" => (1.0, "&lceil;")
   184      | "\\<rceil>" => (1.0, "&rceil;")
   185      | "\\<lfloor>" => (1.0, "&lfloor;")
   186      | "\\<rfloor>" => (1.0, "&rfloor;")
   187      | "\\<langle>" => (1.0, "&lang;")
   188      | "\\<rangle>" => (1.0, "&rang;")
   189      | "\\<lozenge>" => (1.0, "&loz;")
   190      | "\\<spadesuit>" => (1.0, "&spades;")
   191      | "\\<clubsuit>" => (1.0, "&clubs;")
   192      | "\\<heartsuit>" => (1.0, "&hearts;")
   193      | "\\<diamondsuit>" => (1.0, "&diams;")
   194 
   195      | "\\<lbrakk>" => (2.0, "[|")
   196      | "\\<rbrakk>" => (2.0, "|]")
   197      | "\\<Longrightarrow>" => (3.0, "==&gt;")
   198      | "\\<Rightarrow>" => (3.0, "=&gt;")
   199      | "\\<And>" => (2.0, "!!")
   200      | "\\<Colon>" => (2.0, "::")
   201      | "\\<lparr>" => (2.0, "(|")
   202      | "\\<rparr>" => (2.0, "|)")
   203      | "\\<longleftrightarrow>" => (3.0, "&lt;-&gt;")
   204      | "\\<longrightarrow>" => (3.0, "--&gt;")
   205      | "\\<rightarrow>" => (2.0, "-&gt;")
   206      | "\\<rightleftharpoons>" => (2.0, "==")
   207      | "\\<rightharpoonup>" => (2.0, "=&gt;")
   208      | "\\<leftharpoondown>" => (2.0, "&lt;=")
   209 
   210      | "\\<^bsub>" => (0.0, "<sub>")
   211      | "\\<^esub>" => (0.0, "</sub>")
   212      | "\\<^bsup>" => (0.0, "<sup>")
   213      | "\\<^esup>" => (0.0, "</sup>")
   214 (* keep \<^sub> etc, so they are not destroyed by default case *)
   215      | "\\<^sup>" => (0.0, "\\<^sup>")
   216      | "\\<^sub>" => (0.0, "\\<^sub>")
   217      | "\\<^isup>" => (0.0, "\\<^isup>")
   218      | "\\<^isub>" => (0.0, "\\<^isub>")
   219      | s => (real (size s), implode (map escape (explode s)));
   220 
   221   fun add_sym (width, (w: real, s)) = (width + w, s);
   222 
   223   fun script (0, "\\<^sub>") = (1,"<sub>")
   224     | script (0, "\\<^isub>") = (1,"<sub>")
   225     | script (1, x) = (0, x ^ "</sub>")
   226     | script (0, "\\<^sup>") = (2,"<sup>")
   227     | script (0, "\\<^isup>") = (2,"<sup>")
   228     | script (2, x) = (0, x ^ "</sup>")
   229     | script (s, x) = (s,x);
   230 
   231   fun scrs (s, []) = (s,[])
   232     | scrs (s, x::xs) = let val (s', x') = script (s, x)
   233                             val (s'', xs') = scrs (s', xs)
   234                         in (s'', x'::xs') end;
   235                            
   236   fun scripts ss = #2 (scrs (0,ss));
   237 in
   238 
   239 fun output_width str =
   240   if not (exists_string (equal "<" orf equal ">" orf equal "&") str) then (str, real (size str))
   241   else
   242     let val (width, syms) = foldl_map add_sym (0.0, map output_sym (Symbol.explode str))
   243     in (implode (scripts syms), width) end;
   244 
   245 val output = #1 o output_width;
   246 val output_symbols = scripts o (map (#2 o output_sym))
   247 
   248 end;
   249 
   250 
   251 val _ = Symbol.add_mode htmlN (output_width, Symbol.default_indent);
   252 
   253 
   254 (* token translations *)
   255 
   256 fun style stl =
   257   apfst (enclose ("<span class=" ^ quote stl ^ ">") "</span>") o output_width;
   258 
   259 val html_trans =
   260  [("class", style "tclass"),
   261   ("tfree", style "tfree"),
   262   ("tvar",  style "tvar"),
   263   ("free",  style "free"),
   264   ("bound", style "bound"),
   265   ("var",   style "var"),
   266   ("xstr",  style "xstr")];
   267 
   268 
   269 
   270 (** HTML markup **)
   271 
   272 type text = string;
   273 
   274 
   275 (* atoms *)
   276 
   277 val plain = output;
   278 fun name s = "<span class=\"name\">" ^ output s ^ "</span>";
   279 fun keyword s = "<span class=\"keyword\">" ^ output s ^ "</span>";
   280 fun file_name s = "<span class=\"filename\">" ^ output s ^ "</span>";
   281 val file_path = file_name o Url.pack;
   282 
   283 
   284 (* misc *)
   285 
   286 fun href_name s txt = "<a href=" ^ quote s ^ ">" ^ txt ^ "</a>";
   287 fun href_path path txt = href_name (Url.pack path) txt;
   288 
   289 fun href_opt_name None txt = txt
   290   | href_opt_name (Some s) txt = href_name s txt;
   291 
   292 fun href_opt_path None txt = txt
   293   | href_opt_path (Some p) txt = href_path p txt;
   294 
   295 fun para txt = "\n<p>" ^ txt ^ "</p>\n";
   296 fun preform txt = "<pre>" ^ txt ^ "</pre>";
   297 val verbatim = preform o output;
   298 
   299 
   300 (* document *)
   301 
   302 fun begin_document title =
   303   "<!DOCTYPE HTML PUBLIC \"-//W3C//DTD HTML 4.01 Transitional//EN\" \"http://www.w3.org/TR/html4/loose.dtd\">\n\
   304   \\n\
   305   \<html>\n\
   306   \<head>\n\
   307   \<meta http-equiv=\"Content-Type\" content=\"text/html; charset=iso-8859-1\">\n\
   308   \<title>" ^ plain (title ^ " (" ^ version ^ ")") ^ "</title>\n\
   309   \<link rel=\"stylesheet\" type=\"text/css\" href=\"isabelle.css\">\n\
   310   \</head>\n\
   311   \\n\
   312   \<body>\n\
   313   \<div class=\"head\">\
   314   \<h1>" ^ plain title ^ "</h1>\n"
   315 
   316 val end_document = "\n</div>\n</body>\n</html>\n";
   317 
   318 fun gen_link how (path, name) = para (href_path path how ^ " to index of " ^ plain name);
   319 val up_link = gen_link "Up";
   320 val back_link = gen_link "Back";
   321 
   322 
   323 (* session index *)
   324 
   325 fun begin_index up (index_path, session) opt_readme opt_doc graph =
   326   begin_document ("Index of " ^ session) ^ up_link up ^
   327   para ("View " ^ href_path graph "theory dependencies" ^
   328     (case opt_readme of None => "" | Some p => "<br>\nView " ^ href_path p "README") ^
   329     (case opt_doc of None => "" | Some p => "<br>\nView " ^ href_path p "document")) ^
   330   "\n</div>\n<hr>\n<div class=\"theories\">\n<h2>Theories</h2>\n<ul>\n";
   331 
   332 val end_index = end_document;
   333 
   334 fun choice chs s = space_implode " " (map (fn (s', lnk) =>
   335   enclose "[" "]" (if s = s' then keyword s' else href_name lnk s')) chs);
   336 
   337 fun applet_pages session back =
   338   let
   339     val sizes =
   340      [("small", "small.html", ("500", "400")),
   341       ("medium", "medium.html", ("650", "520")),
   342       ("large", "large.html", ("800", "640"))];
   343 
   344     fun applet_page (size, name, (width, height)) =
   345       let
   346         val browser_size = "Set browser size: " ^
   347           choice (map (fn (y, z, _) => (y, z)) sizes) size;
   348       in
   349         (name, begin_document ("Theory dependencies of " ^ session) ^
   350           back_link back ^
   351           para browser_size ^
   352           "\n</div>\n<hr>\n<div class=\"graphbrowser\">\n<applet code=\"GraphBrowser/GraphBrowser.class\" \
   353           \archive=\"GraphBrowser.jar\" \
   354           \width=" ^ width ^ " height=" ^ height ^ ">\n\
   355           \<param name=\"graphfile\" value=\"" ^ "session.graph" ^ "\">\n\
   356           \</applet>\n<hr>" ^ end_document)
   357       end;
   358   in map applet_page sizes end;
   359 
   360 
   361 fun entry (p, s) = "<li>" ^ href_path p (plain s) ^ "\n";
   362 
   363 val theory_entry = entry;
   364 
   365 fun session_entries [] = "</ul>"
   366   | session_entries es =
   367       "</ul>\n</div>\n<hr>\n<div class=\"sessions\">\n<h2>Sessions</h2>\n<ul>\n" ^ implode (map entry es) ^ "</ul>";
   368 
   369 
   370 (* theory *)
   371 
   372 fun verbatim_source ss = "\n</div>\n<hr>\n<div class=\"source\">\n<pre>" ^ 
   373                          implode (output_symbols ss)  ^ 
   374                          "</pre>\n</div>\n<hr>\n<div class=\"theorems\">\n";
   375 
   376 
   377 local
   378   fun encl None = enclose "[" "]"
   379     | encl (Some false) = enclose "(" ")"
   380     | encl (Some true) = I;
   381 
   382   fun file (opt_ref, path, loadit) = href_opt_path opt_ref (encl loadit (file_path path));
   383   val files = space_implode " " o map file;
   384   val parents = space_implode " + " o map (uncurry href_opt_path o apsnd name);
   385 
   386   fun theory up A =
   387     begin_document ("Theory " ^ A) ^ "\n" ^ up_link up ^
   388     keyword "theory" ^ " " ^ name A ^ " = ";
   389 in
   390 
   391 fun begin_theory up A Bs [] body = theory up A ^ parents Bs ^ ":\n" ^ body
   392   | begin_theory up A Bs Ps body = theory up A ^ parents Bs ^ "<br>\n" ^ keyword "files" ^
   393       " " ^ files Ps ^ ":" ^ "\n" ^ body;
   394 end;
   395 
   396 val end_theory = end_document;
   397 
   398 
   399 (* ML file *)
   400 
   401 fun ml_file path str =
   402   begin_document ("File " ^ Url.pack path) ^
   403   "\n</div>\n<hr><div class=\"mlsource\">\n" ^ 
   404   verbatim str ^ 
   405   "\n</div>\n<hr>\n<div class=\"mlfooter\">\n" ^ 
   406   end_document;
   407 
   408 
   409 (* theorems *)
   410 
   411 local
   412 
   413 val string_of_thm =
   414   Pretty.setmp_margin 80 Pretty.string_of o
   415     Display.pretty_thm_no_quote o #1 o Drule.freeze_thaw;
   416 
   417 fun thm th = preform (prefix_lines "  " (html_mode string_of_thm th));
   418 
   419 fun thm_name "" = ""
   420   | thm_name a = " " ^ name (a ^ ":");
   421 
   422 in
   423 
   424 fun result k (a, ths) = para (cat_lines ((keyword k ^ thm_name a) :: map thm ths));
   425 
   426 fun results _ [] = ""
   427   | results k (res :: ress) = cat_lines (result k res :: map (result "and") ress);
   428 
   429 end;
   430 
   431 
   432 (* sections *)
   433 
   434 fun chapter heading = "\n\n<h1>" ^ plain heading ^ "</h1>\n";
   435 fun section heading = "\n\n<h2>" ^ plain heading ^ "</h2>\n";
   436 fun subsection heading = "\n\n<h3>" ^ plain heading ^ "</h3>\n";
   437 fun subsubsection heading = "\n\n<h4>" ^ plain heading ^ "</h4>\n";
   438 
   439 
   440 (** theory setup **)
   441 
   442 val setup =
   443  [Theory.add_mode_tokentrfuns htmlN html_trans];
   444 
   445 
   446 end;