wneuper/isa: src/Pure/Thy/html.ML@c6dc17aab88a

     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)

     6 HTML presentation elements.

     7 *)

     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;

    45 structure HTML: HTML =

    46 struct

    49 (** HTML print modes **)

    51 (* mode *)

    53 val htmlN = "HTML";

    54 fun html_mode f x = setmp print_mode (htmlN :: ! print_mode) f x;

    57 (* symbol output *)

    59 local

    60   val escape = fn "<" => "&lt;" | ">" => "&gt;" | "&" => "&amp;" | c => c;

    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;")

   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;=")

   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)));

   221   fun add_sym (width, (w: real, s)) = (width + w, s);

   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);

   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;

   236   fun scripts ss = #2 (scrs (0,ss));

   237 in

   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;

   245 val output = #1 o output_width;

   246 val output_symbols = scripts o (map (#2 o output_sym))

   248 end;

   251 val _ = Symbol.add_mode htmlN (output_width, Symbol.default_indent);

   254 (* token translations *)

   256 fun style stl =

   257   apfst (enclose ("<span class=" ^ quote stl ^ ">") "</span>") o output_width;

   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")];

   270 (** HTML markup **)

   272 type text = string;

   275 (* atoms *)

   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;

   284 (* misc *)

   286 fun href_name s txt = "<a href=" ^ quote s ^ ">" ^ txt ^ "</a>";

   287 fun href_path path txt = href_name (Url.pack path) txt;

   289 fun href_opt_name None txt = txt

   290   | href_opt_name (Some s) txt = href_name s txt;

   292 fun href_opt_path None txt = txt

   293   | href_opt_path (Some p) txt = href_path p txt;

   295 fun para txt = "\n<p>" ^ txt ^ "</p>\n";

   296 fun preform txt = "<pre>" ^ txt ^ "</pre>";

   297 val verbatim = preform o output;

   300 (* document *)

   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"

   316 val end_document = "\n</div>\n</body>\n</html>\n";

   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";

   323 (* session index *)

   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";

   332 val end_index = end_document;

   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);

   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"))];

   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;

   361 fun entry (p, s) = "<li>" ^ href_path p (plain s) ^ "\n";

   363 val theory_entry = entry;

   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>";

   370 (* theory *)

   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";

   377 local

   378   fun encl None = enclose "[" "]"

   379     | encl (Some false) = enclose "(" ")"

   380     | encl (Some true) = I;

   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);

   386   fun theory up A =

   387     begin_document ("Theory " ^ A) ^ "\n" ^ up_link up ^

   388     keyword "theory" ^ " " ^ name A ^ " = ";

   389 in

   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;

   396 val end_theory = end_document;

   399 (* ML file *)

   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;

   409 (* theorems *)

   411 local

   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;

   417 fun thm th = preform (prefix_lines "  " (html_mode string_of_thm th));

   419 fun thm_name "" = ""

   420   | thm_name a = " " ^ name (a ^ ":");

   422 in

   424 fun result k (a, ths) = para (cat_lines ((keyword k ^ thm_name a) :: map thm ths));

   426 fun results _ [] = ""

   427   | results k (res :: ress) = cat_lines (result k res :: map (result "and") ress);

   429 end;

   432 (* sections *)

   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";

   440 (** theory setup **)

   442 val setup =

   443  [Theory.add_mode_tokentrfuns htmlN html_trans];

   446 end;

author	kleing
	Wed, 14 Apr 2004 14:13:05 +0200
changeset 14565	c6dc17aab88a
parent 14558	726f6761c562
child 14571	b88d5f9e02e1
permissions	-rw-r--r--