src/Pure/Thy/html.ML
author wenzelm
Tue Feb 11 17:44:29 2014 +0100 (2014-02-11)
changeset 55431 e0f20a44ff9d
parent 55041 368ee97e03ce
child 59448 149d2bc5ddb6
permissions -rw-r--r--
common Command.Chunk for command source and auxiliary files (static Symbol.Index without actual String content);
more informative type Blob, to allow markup reports;
     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 href_name: string -> text -> text
    16   val href_path: Url.T -> text -> text
    17   val href_opt_path: Url.T option -> text -> text
    18   val para: text -> text
    19   val preform: text -> text
    20   val verbatim: string -> text
    21   val begin_document: string -> text
    22   val end_document: text
    23   val begin_session_index: string -> (Url.T * string) list -> Url.T -> text
    24   val applet_pages: string -> Url.T * string -> (string * string) list
    25   val theory_entry: Url.T * string -> text
    26   val theory: string -> (Url.T option * string) list -> text -> text
    27 end;
    28 
    29 structure HTML: HTML =
    30 struct
    31 
    32 
    33 (** HTML print modes **)
    34 
    35 (* mode *)
    36 
    37 val htmlN = "HTML";
    38 fun html_mode f x = Print_Mode.with_modes [htmlN] f x;
    39 
    40 
    41 (* common markup *)
    42 
    43 fun span class = ("<span class=" ^ quote (XML.text class) ^ ">", "</span>");
    44 
    45 val _ = Markup.add_mode htmlN (span o fst);
    46 
    47 
    48 (* symbol output *)
    49 
    50 local
    51   val hidden = span Markup.hiddenN |-> enclose;
    52 
    53   (* FIXME proper unicode -- produced on Scala side *)
    54   val html_syms = Symtab.make
    55    [("", (0, "")),
    56     ("'", (1, "&#39;")),
    57     ("\\<exclamdown>", (1, "&iexcl;")),
    58     ("\\<cent>", (1, "&cent;")),
    59     ("\\<pounds>", (1, "&pound;")),
    60     ("\\<currency>", (1, "&curren;")),
    61     ("\\<yen>", (1, "&yen;")),
    62     ("\\<bar>", (1, "&brvbar;")),
    63     ("\\<section>", (1, "&sect;")),
    64     ("\\<dieresis>", (1, "&uml;")),
    65     ("\\<copyright>", (1, "&copy;")),
    66     ("\\<ordfeminine>", (1, "&ordf;")),
    67     ("\\<guillemotleft>", (1, "&laquo;")),
    68     ("\\<not>", (1, "&not;")),
    69     ("\\<hyphen>", (1, "&shy;")),
    70     ("\\<registered>", (1, "&reg;")),
    71     ("\\<inverse>", (1, "&macr;")),
    72     ("\\<degree>", (1, "&deg;")),
    73     ("\\<plusminus>", (1, "&plusmn;")),
    74     ("\\<acute>", (1, "&acute;")),
    75     ("\\<paragraph>", (1, "&para;")),
    76     ("\\<cdot>", (1, "&middot;")),
    77     ("\\<cedilla>", (1, "&cedil;")),
    78     ("\\<ordmasculine>", (1, "&ordm;")),
    79     ("\\<guillemotright>", (1, "&raquo;")),
    80     ("\\<onequarter>", (1, "&frac14;")),
    81     ("\\<onehalf>", (1, "&frac12;")),
    82     ("\\<threequarters>", (1, "&frac34;")),
    83     ("\\<questiondown>", (1, "&iquest;")),
    84     ("\\<times>", (1, "&times;")),
    85     ("\\<div>", (1, "&divide;")),
    86     ("\\<circ>", (1, "o")),
    87     ("\\<Alpha>", (1, "&Alpha;")),
    88     ("\\<Beta>", (1, "&Beta;")),
    89     ("\\<Gamma>", (1, "&Gamma;")),
    90     ("\\<Delta>", (1, "&Delta;")),
    91     ("\\<Epsilon>", (1, "&Epsilon;")),
    92     ("\\<Zeta>", (1, "&Zeta;")),
    93     ("\\<Eta>", (1, "&Eta;")),
    94     ("\\<Theta>", (1, "&Theta;")),
    95     ("\\<Iota>", (1, "&Iota;")),
    96     ("\\<Kappa>", (1, "&Kappa;")),
    97     ("\\<Lambda>", (1, "&Lambda;")),
    98     ("\\<Mu>", (1, "&Mu;")),
    99     ("\\<Nu>", (1, "&Nu;")),
   100     ("\\<Xi>", (1, "&Xi;")),
   101     ("\\<Omicron>", (1, "&Omicron;")),
   102     ("\\<Pi>", (1, "&Pi;")),
   103     ("\\<Rho>", (1, "&Rho;")),
   104     ("\\<Sigma>", (1, "&Sigma;")),
   105     ("\\<Tau>", (1, "&Tau;")),
   106     ("\\<Upsilon>", (1, "&Upsilon;")),
   107     ("\\<Phi>", (1, "&Phi;")),
   108     ("\\<Chi>", (1, "&Chi;")),
   109     ("\\<Psi>", (1, "&Psi;")),
   110     ("\\<Omega>", (1, "&Omega;")),
   111     ("\\<alpha>", (1, "&alpha;")),
   112     ("\\<beta>", (1, "&beta;")),
   113     ("\\<gamma>", (1, "&gamma;")),
   114     ("\\<delta>", (1, "&delta;")),
   115     ("\\<epsilon>", (1, "&epsilon;")),
   116     ("\\<zeta>", (1, "&zeta;")),
   117     ("\\<eta>", (1, "&eta;")),
   118     ("\\<theta>", (1, "&thetasym;")),
   119     ("\\<iota>", (1, "&iota;")),
   120     ("\\<kappa>", (1, "&kappa;")),
   121     ("\\<lambda>", (1, "&lambda;")),
   122     ("\\<mu>", (1, "&mu;")),
   123     ("\\<nu>", (1, "&nu;")),
   124     ("\\<xi>", (1, "&xi;")),
   125     ("\\<omicron>", (1, "&omicron;")),
   126     ("\\<pi>", (1, "&pi;")),
   127     ("\\<rho>", (1, "&rho;")),
   128     ("\\<sigma>", (1, "&sigma;")),
   129     ("\\<tau>", (1, "&tau;")),
   130     ("\\<upsilon>", (1, "&upsilon;")),
   131     ("\\<phi>", (1, "&phi;")),
   132     ("\\<chi>", (1, "&chi;")),
   133     ("\\<psi>", (1, "&psi;")),
   134     ("\\<omega>", (1, "&omega;")),
   135     ("\\<bullet>", (1, "&bull;")),
   136     ("\\<dots>", (1, "&hellip;")),
   137     ("\\<wp>", (1, "&weierp;")),
   138     ("\\<forall>", (1, "&forall;")),
   139     ("\\<partial>", (1, "&part;")),
   140     ("\\<exists>", (1, "&exist;")),
   141     ("\\<emptyset>", (1, "&empty;")),
   142     ("\\<nabla>", (1, "&nabla;")),
   143     ("\\<in>", (1, "&isin;")),
   144     ("\\<notin>", (1, "&notin;")),
   145     ("\\<Prod>", (1, "&prod;")),
   146     ("\\<Sum>", (1, "&sum;")),
   147     ("\\<star>", (1, "&lowast;")),
   148     ("\\<propto>", (1, "&prop;")),
   149     ("\\<infinity>", (1, "&infin;")),
   150     ("\\<angle>", (1, "&ang;")),
   151     ("\\<and>", (1, "&and;")),
   152     ("\\<or>", (1, "&or;")),
   153     ("\\<inter>", (1, "&cap;")),
   154     ("\\<union>", (1, "&cup;")),
   155     ("\\<sim>", (1, "&sim;")),
   156     ("\\<cong>", (1, "&cong;")),
   157     ("\\<approx>", (1, "&asymp;")),
   158     ("\\<noteq>", (1, "&ne;")),
   159     ("\\<equiv>", (1, "&equiv;")),
   160     ("\\<le>", (1, "&le;")),
   161     ("\\<ge>", (1, "&ge;")),
   162     ("\\<subset>", (1, "&sub;")),
   163     ("\\<supset>", (1, "&sup;")),
   164     ("\\<subseteq>", (1, "&sube;")),
   165     ("\\<supseteq>", (1, "&supe;")),
   166     ("\\<oplus>", (1, "&oplus;")),
   167     ("\\<otimes>", (1, "&otimes;")),
   168     ("\\<bottom>", (1, "&perp;")),
   169     ("\\<lceil>", (1, "&lceil;")),
   170     ("\\<rceil>", (1, "&rceil;")),
   171     ("\\<lfloor>", (1, "&lfloor;")),
   172     ("\\<rfloor>", (1, "&rfloor;")),
   173     ("\\<langle>", (1, "&lang;")),
   174     ("\\<rangle>", (1, "&rang;")),
   175     ("\\<lozenge>", (1, "&loz;")),
   176     ("\\<spadesuit>", (1, "&spades;")),
   177     ("\\<clubsuit>", (1, "&clubs;")),
   178     ("\\<heartsuit>", (1, "&hearts;")),
   179     ("\\<diamondsuit>", (1, "&diams;")),
   180     ("\\<lbrakk>", (2, "[|")),
   181     ("\\<rbrakk>", (2, "|]")),
   182     ("\\<Longrightarrow>", (3, "==&gt;")),
   183     ("\\<Rightarrow>", (2, "=&gt;")),
   184     ("\\<And>", (2, "!!")),
   185     ("\\<Colon>", (2, "::")),
   186     ("\\<lparr>", (2, "(|")),
   187     ("\\<rparr>", (2, "|)),")),
   188     ("\\<longleftrightarrow>", (3, "&lt;-&gt;")),
   189     ("\\<longrightarrow>", (3, "--&gt;")),
   190     ("\\<rightarrow>", (2, "-&gt;")),
   191     ("\\<open>", (1, "&#8249;")),
   192     ("\\<close>", (1, "&#8250;")),
   193     ("\\<newline>", (1, "&#9166;")),
   194     ("\\<^bsub>", (0, hidden "&#8664;" ^ "<sub>")),
   195     ("\\<^esub>", (0, hidden "&#8665;" ^ "</sub>")),
   196     ("\\<^bsup>", (0, hidden "&#8663;" ^ "<sup>")),
   197     ("\\<^esup>", (0, hidden "&#8662;" ^ "</sup>"))];
   198 
   199   fun output_sym s =
   200     if Symbol.is_raw s then (1, Symbol.decode_raw s)
   201     else
   202       (case Symtab.lookup html_syms s of
   203         SOME x => x
   204       | NONE => (size s, XML.text s));
   205 
   206   fun output_markup (bg, en) s1 s2 =
   207     let val (n, txt) = output_sym s2
   208     in (n, hidden s1 ^ enclose bg en txt) end;
   209 
   210   val output_sub = output_markup ("<sub>", "</sub>");
   211   val output_sup = output_markup ("<sup>", "</sup>");
   212   val output_bold = output_markup (span "bold");
   213 
   214   fun output_syms [] (result, width) = (implode (rev result), width)
   215     | output_syms (s1 :: rest) (result, width) =
   216         let
   217           val (s2, ss) = (case rest of [] => ("", []) | s2 :: ss => (s2, ss));
   218           val ((w, s), r) =
   219             if s1 = "\\<^sub>" then (output_sub "&#8681;" s2, ss)
   220             else if s1 = "\\<^sup>" then (output_sup "&#8679;" s2, ss)
   221             else if s1 = "\\<^bold>" then (output_bold "&#10073;" s2, ss)
   222             else (output_sym s1, rest);
   223         in output_syms r (s :: result, width + w) end;
   224 in
   225 
   226 fun output_width str = output_syms (Symbol.explode str) ([], 0);
   227 val output = #1 o output_width;
   228 
   229 val _ = Output.add_mode htmlN output_width Symbol.encode_raw;
   230 
   231 end;
   232 
   233 
   234 
   235 (** HTML markup **)
   236 
   237 type text = string;
   238 
   239 
   240 (* atoms *)
   241 
   242 val plain = output;
   243 val name = enclose "<span class=\"name\">" "</span>" o output;
   244 val keyword = enclose "<span class=\"keyword\">" "</span>" o output;
   245 val command = enclose "<span class=\"command\">" "</span>" o output;
   246 
   247 
   248 (* misc *)
   249 
   250 fun href_name s txt = "<a href=" ^ quote s ^ ">" ^ txt ^ "</a>";
   251 fun href_path path txt = href_name (Url.implode path) txt;
   252 
   253 fun href_opt_path NONE txt = txt
   254   | href_opt_path (SOME p) txt = href_path p txt;
   255 
   256 fun para txt = "\n<p>" ^ txt ^ "</p>\n";
   257 fun preform txt = "<pre>" ^ txt ^ "</pre>";
   258 val verbatim = preform o output;
   259 
   260 
   261 (* document *)
   262 
   263 fun begin_document title =
   264   "<?xml version=\"1.0\" encoding=\"utf-8\" ?>\n\
   265   \<!DOCTYPE html PUBLIC \"-//W3C//DTD XHTML 1.0 Transitional//EN\" \
   266   \\"http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd\">\n\
   267   \<html xmlns=\"http://www.w3.org/1999/xhtml\">\n\
   268   \<head>\n\
   269   \<meta http-equiv=\"Content-Type\" content=\"text/html; charset=utf-8\"/>\n\
   270   \<title>" ^ plain (title ^ " (" ^ Distribution.version ^ ")") ^ "</title>\n\
   271   \<link media=\"all\" rel=\"stylesheet\" type=\"text/css\" href=\"isabelle.css\"/>\n\
   272   \</head>\n\
   273   \\n\
   274   \<body>\n\
   275   \<div class=\"head\">\
   276   \<h1>" ^ plain title ^ "</h1>\n";
   277 
   278 val end_document = "\n</div>\n</body>\n</html>\n";
   279 
   280 
   281 (* session index *)
   282 
   283 fun begin_session_index session docs graph =
   284   begin_document ("Session " ^ plain session) ^
   285   para ("View " ^ href_path graph "theory dependencies" ^
   286     implode (map (fn (p, name) => "<br/>\nView " ^ href_path p name) docs)) ^
   287   "\n</div>\n<div class=\"theories\">\n<h2>Theories</h2>\n<ul>\n";
   288 
   289 fun choice chs s = space_implode " " (map (fn (s', lnk) =>
   290   enclose "[" "]" (if s = s' then keyword s' else href_name lnk s')) chs);
   291 
   292 fun back_link (path, name) = para (href_path path "Back" ^ " to index of " ^ plain name);
   293 
   294 fun applet_pages session back =
   295   let
   296     val sizes =
   297      [("small", "small.html", ("500", "400")),
   298       ("medium", "medium.html", ("650", "520")),
   299       ("large", "large.html", ("800", "640"))];
   300 
   301     fun applet_page (size, name, (width, height)) =
   302       let
   303         val browser_size = "Set browser size: " ^
   304           choice (map (fn (y, z, _) => (y, z)) sizes) size;
   305       in
   306         (name, begin_document ("Theory dependencies of " ^ session) ^
   307           back_link back ^
   308           para browser_size ^
   309           "\n</div>\n<div class=\"graphbrowser\">\n\
   310           \<applet code=\"GraphBrowser/GraphBrowser.class\" \
   311           \archive=\"GraphBrowser.jar\" \
   312           \width=" ^ quote width ^ " height=" ^ quote height ^ ">\n\
   313           \<param name=\"graphfile\" value=\"" ^ "session.graph" ^ "\"/>\n\
   314           \</applet>" ^ end_document)
   315       end;
   316   in map applet_page sizes end;
   317 
   318 
   319 fun theory_entry (p, s) = "<li>" ^ href_path p (plain s) ^ "</li>\n";
   320 
   321 
   322 (* theory *)
   323 
   324 fun theory A Bs txt =
   325   begin_document ("Theory " ^ A) ^ "\n" ^
   326   command "theory" ^ " " ^ name A ^ "<br/>\n" ^
   327   keyword "imports" ^ " " ^ space_implode " " (map (uncurry href_opt_path o apsnd name) Bs) ^
   328   "<br/>\n" ^
   329   enclose "\n</div>\n<div class=\"source\">\n<pre>" "</pre>\n" txt ^
   330   end_document;
   331 
   332 end;