src/Pure/Thy/html.ML
author wenzelm
Thu May 27 18:10:37 2010 +0200 (2010-05-27)
changeset 37146 f652333bbf8e
parent 34003 610e41138486
child 37940 4857eab31298
permissions -rw-r--r--
renamed structure PrintMode to Print_Mode, keeping the old name as legacy alias for some time;
     1 (*  Title:      Pure/Thy/html.ML
     2     Author:     Markus Wenzel and Stefan Berghofer, TU Muenchen
     3 
     4 HTML presentation elements.
     5 *)
     6 
     7 signature HTML =
     8 sig
     9   val html_mode: ('a -> 'b) -> 'a -> 'b
    10   type text = string
    11   val plain: string -> text
    12   val name: string -> text
    13   val keyword: string -> text
    14   val command: string -> text
    15   val file_name: string -> text
    16   val file_path: Url.T -> text
    17   val href_name: string -> text -> text
    18   val href_path: Url.T -> text -> text
    19   val href_opt_path: Url.T option -> text -> text
    20   val para: text -> text
    21   val preform: text -> text
    22   val verbatim: string -> text
    23   val with_charset: string -> ('a -> 'b) -> 'a -> 'b
    24   val begin_document: string -> text
    25   val end_document: text
    26   val begin_index: Url.T * string -> Url.T * string -> (Url.T * string) list -> Url.T -> text
    27   val applet_pages: string -> Url.T * string -> (string * string) list
    28   val theory_entry: Url.T * string -> text
    29   val session_entries: (Url.T * string) list -> text
    30   val theory_source: text -> text
    31   val begin_theory: Url.T * string -> string -> (Url.T option * string) list ->
    32     (Url.T * Url.T * bool) list -> text -> text
    33   val ml_file: Url.T -> string -> text
    34 end;
    35 
    36 structure HTML: HTML =
    37 struct
    38 
    39 
    40 (** HTML print modes **)
    41 
    42 (* mode *)
    43 
    44 val htmlN = "HTML";
    45 fun html_mode f x = Print_Mode.with_modes [htmlN] f x;
    46 
    47 
    48 (* common markup *)
    49 
    50 fun span class = ("<span class=" ^ quote (XML.text class) ^ ">", "</span>");
    51 
    52 val _ = Markup.add_mode htmlN (fn (name, _) => span name);
    53 
    54 
    55 (* symbol output *)
    56 
    57 local
    58   val hidden = XML.text #> (span Markup.hiddenN |-> enclose);
    59 
    60   val html_syms = Symtab.make
    61    [("", (0, "")),
    62     ("\n", (0, "<br/>")),
    63     ("'", (1, "&#39;")),
    64     ("\\<spacespace>", (2, "&nbsp;&nbsp;")),
    65     ("\\<exclamdown>", (1, "&iexcl;")),
    66     ("\\<cent>", (1, "&cent;")),
    67     ("\\<pounds>", (1, "&pound;")),
    68     ("\\<currency>", (1, "&curren;")),
    69     ("\\<yen>", (1, "&yen;")),
    70     ("\\<bar>", (1, "&brvbar;")),
    71     ("\\<section>", (1, "&sect;")),
    72     ("\\<dieresis>", (1, "&uml;")),
    73     ("\\<copyright>", (1, "&copy;")),
    74     ("\\<ordfeminine>", (1, "&ordf;")),
    75     ("\\<guillemotleft>", (1, "&laquo;")),
    76     ("\\<not>", (1, "&not;")),
    77     ("\\<hyphen>", (1, "&shy;")),
    78     ("\\<registered>", (1, "&reg;")),
    79     ("\\<inverse>", (1, "&macr;")),
    80     ("\\<degree>", (1, "&deg;")),
    81     ("\\<plusminus>", (1, "&plusmn;")),
    82     ("\\<twosuperior>", (1, "&sup2;")),
    83     ("\\<threesuperior>", (1, "&sup3;")),
    84     ("\\<acute>", (1, "&acute;")),
    85     ("\\<paragraph>", (1, "&para;")),
    86     ("\\<cdot>", (1, "&middot;")),
    87     ("\\<cedilla>", (1, "&cedil;")),
    88     ("\\<onesuperior>", (1, "&sup1;")),
    89     ("\\<ordmasculine>", (1, "&ordm;")),
    90     ("\\<guillemotright>", (1, "&raquo;")),
    91     ("\\<onequarter>", (1, "&frac14;")),
    92     ("\\<onehalf>", (1, "&frac12;")),
    93     ("\\<threequarters>", (1, "&frac34;")),
    94     ("\\<questiondown>", (1, "&iquest;")),
    95     ("\\<times>", (1, "&times;")),
    96     ("\\<div>", (1, "&divide;")),
    97     ("\\<circ>", (1, "o")),
    98     ("\\<Alpha>", (1, "&Alpha;")),
    99     ("\\<Beta>", (1, "&Beta;")),
   100     ("\\<Gamma>", (1, "&Gamma;")),
   101     ("\\<Delta>", (1, "&Delta;")),
   102     ("\\<Epsilon>", (1, "&Epsilon;")),
   103     ("\\<Zeta>", (1, "&Zeta;")),
   104     ("\\<Eta>", (1, "&Eta;")),
   105     ("\\<Theta>", (1, "&Theta;")),
   106     ("\\<Iota>", (1, "&Iota;")),
   107     ("\\<Kappa>", (1, "&Kappa;")),
   108     ("\\<Lambda>", (1, "&Lambda;")),
   109     ("\\<Mu>", (1, "&Mu;")),
   110     ("\\<Nu>", (1, "&Nu;")),
   111     ("\\<Xi>", (1, "&Xi;")),
   112     ("\\<Omicron>", (1, "&Omicron;")),
   113     ("\\<Pi>", (1, "&Pi;")),
   114     ("\\<Rho>", (1, "&Rho;")),
   115     ("\\<Sigma>", (1, "&Sigma;")),
   116     ("\\<Tau>", (1, "&Tau;")),
   117     ("\\<Upsilon>", (1, "&Upsilon;")),
   118     ("\\<Phi>", (1, "&Phi;")),
   119     ("\\<Chi>", (1, "&Chi;")),
   120     ("\\<Psi>", (1, "&Psi;")),
   121     ("\\<Omega>", (1, "&Omega;")),
   122     ("\\<alpha>", (1, "&alpha;")),
   123     ("\\<beta>", (1, "&beta;")),
   124     ("\\<gamma>", (1, "&gamma;")),
   125     ("\\<delta>", (1, "&delta;")),
   126     ("\\<epsilon>", (1, "&epsilon;")),
   127     ("\\<zeta>", (1, "&zeta;")),
   128     ("\\<eta>", (1, "&eta;")),
   129     ("\\<theta>", (1, "&thetasym;")),
   130     ("\\<iota>", (1, "&iota;")),
   131     ("\\<kappa>", (1, "&kappa;")),
   132     ("\\<lambda>", (1, "&lambda;")),
   133     ("\\<mu>", (1, "&mu;")),
   134     ("\\<nu>", (1, "&nu;")),
   135     ("\\<xi>", (1, "&xi;")),
   136     ("\\<omicron>", (1, "&omicron;")),
   137     ("\\<pi>", (1, "&pi;")),
   138     ("\\<rho>", (1, "&rho;")),
   139     ("\\<sigma>", (1, "&sigma;")),
   140     ("\\<tau>", (1, "&tau;")),
   141     ("\\<upsilon>", (1, "&upsilon;")),
   142     ("\\<phi>", (1, "&phi;")),
   143     ("\\<chi>", (1, "&chi;")),
   144     ("\\<psi>", (1, "&psi;")),
   145     ("\\<omega>", (1, "&omega;")),
   146     ("\\<bullet>", (1, "&bull;")),
   147     ("\\<dots>", (1, "&hellip;")),
   148     ("\\<Re>", (1, "&real;")),
   149     ("\\<Im>", (1, "&image;")),
   150     ("\\<wp>", (1, "&weierp;")),
   151     ("\\<forall>", (1, "&forall;")),
   152     ("\\<partial>", (1, "&part;")),
   153     ("\\<exists>", (1, "&exist;")),
   154     ("\\<emptyset>", (1, "&empty;")),
   155     ("\\<nabla>", (1, "&nabla;")),
   156     ("\\<in>", (1, "&isin;")),
   157     ("\\<notin>", (1, "&notin;")),
   158     ("\\<Prod>", (1, "&prod;")),
   159     ("\\<Sum>", (1, "&sum;")),
   160     ("\\<star>", (1, "&lowast;")),
   161     ("\\<propto>", (1, "&prop;")),
   162     ("\\<infinity>", (1, "&infin;")),
   163     ("\\<angle>", (1, "&ang;")),
   164     ("\\<and>", (1, "&and;")),
   165     ("\\<or>", (1, "&or;")),
   166     ("\\<inter>", (1, "&cap;")),
   167     ("\\<union>", (1, "&cup;")),
   168     ("\\<sim>", (1, "&sim;")),
   169     ("\\<cong>", (1, "&cong;")),
   170     ("\\<approx>", (1, "&asymp;")),
   171     ("\\<noteq>", (1, "&ne;")),
   172     ("\\<equiv>", (1, "&equiv;")),
   173     ("\\<le>", (1, "&le;")),
   174     ("\\<ge>", (1, "&ge;")),
   175     ("\\<subset>", (1, "&sub;")),
   176     ("\\<supset>", (1, "&sup;")),
   177     ("\\<subseteq>", (1, "&sube;")),
   178     ("\\<supseteq>", (1, "&supe;")),
   179     ("\\<oplus>", (1, "&oplus;")),
   180     ("\\<otimes>", (1, "&otimes;")),
   181     ("\\<bottom>", (1, "&perp;")),
   182     ("\\<lceil>", (1, "&lceil;")),
   183     ("\\<rceil>", (1, "&rceil;")),
   184     ("\\<lfloor>", (1, "&lfloor;")),
   185     ("\\<rfloor>", (1, "&rfloor;")),
   186     ("\\<langle>", (1, "&lang;")),
   187     ("\\<rangle>", (1, "&rang;")),
   188     ("\\<lozenge>", (1, "&loz;")),
   189     ("\\<spadesuit>", (1, "&spades;")),
   190     ("\\<clubsuit>", (1, "&clubs;")),
   191     ("\\<heartsuit>", (1, "&hearts;")),
   192     ("\\<diamondsuit>", (1, "&diams;")),
   193     ("\\<lbrakk>", (2, "[|")),
   194     ("\\<rbrakk>", (2, "|]")),
   195     ("\\<Longrightarrow>", (3, "==&gt;")),
   196     ("\\<Rightarrow>", (2, "=&gt;")),
   197     ("\\<And>", (2, "!!")),
   198     ("\\<Colon>", (2, "::")),
   199     ("\\<lparr>", (2, "(|")),
   200     ("\\<rparr>", (2, "|)),")),
   201     ("\\<longleftrightarrow>", (3, "&lt;-&gt;")),
   202     ("\\<longrightarrow>", (3, "--&gt;")),
   203     ("\\<rightarrow>", (2, "-&gt;")),
   204     ("\\<^bsub>", (0, hidden "\\<^bsub>" ^ "<sub>")),
   205     ("\\<^esub>", (0, hidden "\\<^esub>" ^ "</sub>")),
   206     ("\\<^bsup>", (0, hidden "\\<^bsup>" ^ "<sup>")),
   207     ("\\<^esup>", (0, hidden "\\<^esup>" ^ "</sup>"))];
   208 
   209   fun output_sym s =
   210     if Symbol.is_raw s then (1, Symbol.decode_raw s)
   211     else
   212       (case Symtab.lookup html_syms s of
   213         SOME x => x
   214       | NONE => (size s, XML.text s));
   215 
   216   fun output_markup (bg, en) s1 s2 =
   217     let val (n, txt) = output_sym s2
   218     in (n, hidden s1 ^ enclose bg en txt) end;
   219 
   220   val output_sub = output_markup ("<sub>", "</sub>");
   221   val output_sup = output_markup ("<sup>", "</sup>");
   222   val output_bold = output_markup (span "bold");
   223   val output_loc = output_markup (span "loc");
   224 
   225   fun output_syms (s1 :: rest) =
   226         let val (s2, ss) = (case rest of [] => ("", []) | s2 :: ss => (s2, ss)) in
   227           if s1 = "\\<^sub>" orelse s1 = "\\<^isub>" then output_sub s1 s2 :: output_syms ss
   228           else if s1 = "\\<^sup>" orelse s1 = "\\<^isup>" then output_sup s1 s2 :: output_syms ss
   229           else if s1 = "\\<^bold>" then output_bold s1 s2 :: output_syms ss
   230           else if s1 = "\\<^loc>" then output_loc s1 s2 :: output_syms ss
   231           else output_sym s1 :: output_syms rest
   232         end
   233     | output_syms [] = [];
   234 in
   235 
   236 fun output_width str =
   237   let val (syms, width) =
   238     fold_map (fn (w, s) => fn width => (s, w + width)) (output_syms (Symbol.explode str)) 0
   239   in (implode syms, width) end;
   240 
   241 val output = #1 o output_width;
   242 
   243 val _ = Output.add_mode htmlN output_width Symbol.encode_raw;
   244 
   245 end;
   246 
   247 
   248 
   249 (** HTML markup **)
   250 
   251 type text = string;
   252 
   253 
   254 (* atoms *)
   255 
   256 val plain = output;
   257 val name = enclose "<span class=\"name\">" "</span>" o output;
   258 val keyword = enclose "<span class=\"keyword\">" "</span>" o output;
   259 val command = enclose "<span class=\"command\">" "</span>" o output;
   260 val file_name = enclose "<span class=\"filename\">" "</span>" o output;
   261 val file_path = file_name o Url.implode;
   262 
   263 
   264 (* misc *)
   265 
   266 fun href_name s txt = "<a href=" ^ quote s ^ ">" ^ txt ^ "</a>";
   267 fun href_path path txt = href_name (Url.implode path) txt;
   268 
   269 fun href_opt_path NONE txt = txt
   270   | href_opt_path (SOME p) txt = href_path p txt;
   271 
   272 fun para txt = "\n<p>" ^ txt ^ "</p>\n";
   273 fun preform txt = "<pre>" ^ txt ^ "</pre>";
   274 val verbatim = preform o output;
   275 
   276 
   277 (* document *)
   278 
   279 val charset = Unsynchronized.ref "ISO-8859-1";
   280 fun with_charset s = setmp_noncritical charset s;   (* FIXME unreliable *)
   281 
   282 fun begin_document title =
   283   let val cs = ! charset in
   284     "<?xml version=\"1.0\" encoding=\"" ^ cs ^ "\" ?>\n\
   285     \<!DOCTYPE html PUBLIC \"-//W3C//DTD XHTML 1.0 Transitional//EN\" \
   286     \\"http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd\">\n\
   287     \<html xmlns=\"http://www.w3.org/1999/xhtml\">\n\
   288     \<head>\n\
   289     \<meta http-equiv=\"Content-Type\" content=\"text/html; charset=" ^ cs ^ "\"/>\n\
   290     \<title>" ^ plain (title ^ " (" ^ Distribution.version ^ ")") ^ "</title>\n\
   291     \<link media=\"all\" rel=\"stylesheet\" type=\"text/css\" href=\"isabelle.css\"/>\n\
   292     \</head>\n\
   293     \\n\
   294     \<body>\n\
   295     \<div class=\"head\">\
   296     \<h1>" ^ plain title ^ "</h1>\n"
   297   end;
   298 
   299 val end_document = "\n</div>\n</body>\n</html>\n";
   300 
   301 fun gen_link how (path, name) = para (href_path path how ^ " to index of " ^ plain name);
   302 val up_link = gen_link "Up";
   303 val back_link = gen_link "Back";
   304 
   305 
   306 (* session index *)
   307 
   308 fun begin_index up (index_path, session) docs graph =
   309   begin_document ("Index of " ^ session) ^ up_link up ^
   310   para ("View " ^ href_path graph "theory dependencies" ^
   311     implode (map (fn (p, name) => "<br/>\nView " ^ href_path p name) docs)) ^
   312   "\n</div>\n<hr/>\n<div class=\"theories\">\n<h2>Theories</h2>\n<ul>\n";
   313 
   314 fun choice chs s = space_implode " " (map (fn (s', lnk) =>
   315   enclose "[" "]" (if s = s' then keyword s' else href_name lnk s')) chs);
   316 
   317 fun applet_pages session back =
   318   let
   319     val sizes =
   320      [("small", "small.html", ("500", "400")),
   321       ("medium", "medium.html", ("650", "520")),
   322       ("large", "large.html", ("800", "640"))];
   323 
   324     fun applet_page (size, name, (width, height)) =
   325       let
   326         val browser_size = "Set browser size: " ^
   327           choice (map (fn (y, z, _) => (y, z)) sizes) size;
   328       in
   329         (name, begin_document ("Theory dependencies of " ^ session) ^
   330           back_link back ^
   331           para browser_size ^
   332           "\n</div>\n<hr/>\n<div class=\"graphbrowser\">\n\
   333           \<applet code=\"GraphBrowser/GraphBrowser.class\" \
   334           \archive=\"GraphBrowser.jar\" \
   335           \width=" ^ quote width ^ " height=" ^ quote height ^ ">\n\
   336           \<param name=\"graphfile\" value=\"" ^ "session.graph" ^ "\"/>\n\
   337           \</applet>\n<hr/>" ^ end_document)
   338       end;
   339   in map applet_page sizes end;
   340 
   341 
   342 fun entry (p, s) = "<li>" ^ href_path p (plain s) ^ "</li>\n";
   343 
   344 val theory_entry = entry;
   345 
   346 fun session_entries [] = "</ul>"
   347   | session_entries es =
   348       "</ul>\n</div>\n<hr/>\n<div class=\"sessions\">\n\
   349       \<h2>Sessions</h2>\n<ul>\n" ^ implode (map entry es) ^ "</ul>";
   350 
   351 
   352 (* theory *)
   353 
   354 val theory_source = enclose
   355   "\n</div>\n<hr/>\n<div class=\"source\">\n<pre>"
   356   "</pre>\n<hr/>\n";
   357 
   358 
   359 local
   360   fun file (href, path, loadit) =
   361     href_path href (if loadit then file_path path else enclose "(" ")" (file_path path));
   362 
   363   fun theory up A =
   364     begin_document ("Theory " ^ A) ^ "\n" ^ up_link up ^
   365     command "theory" ^ " " ^ name A;
   366 
   367   fun imports Bs =
   368     keyword "imports" ^ " " ^ space_implode " " (map (uncurry href_opt_path o apsnd name) Bs);
   369 
   370   fun uses Ps = keyword "uses" ^ " " ^ space_implode " " (map file Ps) ^ "<br/>\n";
   371 in
   372 
   373 fun begin_theory up A Bs Ps body =
   374   theory up A ^ "<br/>\n" ^
   375   imports Bs ^ "<br/>\n" ^
   376   (if null Ps then "" else uses Ps) ^
   377   body;
   378 
   379 end;
   380 
   381 
   382 (* ML file *)
   383 
   384 fun ml_file path str =
   385   begin_document ("File " ^ Url.implode path) ^
   386   "\n</div>\n<hr/><div class=\"mlsource\">\n" ^
   387   verbatim str ^
   388   "\n</div>\n<hr/>\n<div class=\"mlfooter\">" ^
   389   end_document;
   390 
   391 end;