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