src/Pure/Thy/html.ML
author kleing
Fri Apr 09 16:31:15 2004 +0200 (2004-04-09)
changeset 14534 7a46bdcd92f2
parent 14083 aed5d25c4a0c
child 14541 0a7743e2f8dd
permissions -rw-r--r--
treat sub/super scripts
wenzelm@6324
     1
(*  Title:      Pure/Thy/HTML.ML
wenzelm@6324
     2
    ID:         $Id$
wenzelm@9415
     3
    Author:     Markus Wenzel and Stefan Berghofer, TU Muenchen
wenzelm@8808
     4
    License:    GPL (GNU GENERAL PUBLIC LICENSE)
wenzelm@6324
     5
wenzelm@9415
     6
HTML presentation elements.
wenzelm@6324
     7
*)
wenzelm@6324
     8
wenzelm@6324
     9
signature HTML =
wenzelm@6324
    10
sig
wenzelm@6324
    11
  val output: string -> string
wenzelm@6324
    12
  val output_width: string -> string * real
wenzelm@6324
    13
  type text (* = string *)
wenzelm@6324
    14
  val plain: string -> text
wenzelm@6324
    15
  val name: string -> text
wenzelm@6324
    16
  val keyword: string -> text
wenzelm@6324
    17
  val file_name: string -> text
berghofe@6649
    18
  val file_path: Url.T -> text
wenzelm@6324
    19
  val href_name: string -> text -> text
berghofe@6649
    20
  val href_path: Url.T -> text -> text
wenzelm@6376
    21
  val href_opt_name: string option -> text -> text
berghofe@6649
    22
  val href_opt_path: Url.T option -> text -> text
wenzelm@6376
    23
  val para: text -> text
wenzelm@6324
    24
  val preform: text -> text
wenzelm@6324
    25
  val verbatim: string -> text
wenzelm@7725
    26
  val begin_index: Url.T * string -> Url.T * string -> Url.T option
wenzelm@7725
    27
    -> Url.T option -> Url.T -> text
wenzelm@6338
    28
  val end_index: text
wenzelm@9415
    29
  val applet_pages: string -> Url.T * string -> (string * string) list
berghofe@6649
    30
  val theory_entry: Url.T * string -> text
berghofe@6649
    31
  val session_entries: (Url.T * string) list -> text
wenzelm@8190
    32
  val verbatim_source: Symbol.symbol list -> text
berghofe@6649
    33
  val begin_theory: Url.T * string -> string -> (Url.T option * string) list ->
wenzelm@7408
    34
    (Url.T option * Url.T * bool option) list -> text -> text
wenzelm@6324
    35
  val end_theory: text
berghofe@6649
    36
  val ml_file: Url.T -> string -> text
wenzelm@13531
    37
  val results: string -> (string * thm list) list -> text
wenzelm@8088
    38
  val chapter: string -> text
wenzelm@6324
    39
  val section: string -> text
wenzelm@7634
    40
  val subsection: string -> text
wenzelm@7634
    41
  val subsubsection: string -> text
wenzelm@6324
    42
  val setup: (theory -> theory) list
wenzelm@6324
    43
end;
wenzelm@6324
    44
wenzelm@6324
    45
structure HTML: HTML =
wenzelm@6324
    46
struct
wenzelm@6324
    47
wenzelm@6324
    48
wenzelm@6324
    49
(** HTML print modes **)
wenzelm@6324
    50
wenzelm@6324
    51
(* mode *)
wenzelm@6324
    52
wenzelm@6324
    53
val htmlN = "HTML";
wenzelm@10573
    54
fun html_mode f x = setmp print_mode (htmlN :: ! print_mode) f x;
wenzelm@6324
    55
wenzelm@6324
    56
wenzelm@6324
    57
(* symbol output *)
wenzelm@6324
    58
wenzelm@6338
    59
local
wenzelm@6338
    60
  val escape = fn "<" => "&lt;" | ">" => "&gt;" | "&" => "&amp;" | c => c;
wenzelm@6324
    61
wenzelm@6338
    62
  val output_sym =
wenzelm@9963
    63
    fn "\\<spacespace>" => (2.0, "&nbsp;&nbsp;")
wenzelm@9963
    64
     | "\\<exclamdown>" => (1.0, "&iexcl;")
wenzelm@9963
    65
     | "\\<cent>" => (1.0, "&cent;")
wenzelm@9963
    66
     | "\\<pounds>" => (1.0, "&pound;")
wenzelm@9963
    67
     | "\\<currency>" => (1.0, "&curren;")
wenzelm@9963
    68
     | "\\<yen>" => (1.0, "&yen;")
wenzelm@9963
    69
     | "\\<bar>" => (1.0, "&brvbar;")
wenzelm@9963
    70
     | "\\<section>" => (1.0, "&sect;")
wenzelm@10837
    71
     | "\\<dieresis>" => (1.0, "&uml;")
wenzelm@9963
    72
     | "\\<copyright>" => (1.0, "&copy;")
wenzelm@9963
    73
     | "\\<ordfeminine>" => (1.0, "&ordf;")
wenzelm@9963
    74
     | "\\<guillemotleft>" => (1.0, "&laquo;")
wenzelm@9963
    75
     | "\\<not>" => (1.0, "&not;")
wenzelm@6338
    76
     | "\\<hyphen>" => (1.0, "&shy;")
wenzelm@9963
    77
     | "\\<registered>" => (1.0, "&reg;")
wenzelm@10831
    78
     | "\\<inverse>" => (1.0, "&macr;")
wenzelm@9963
    79
     | "\\<degree>" => (1.0, "&deg;")
wenzelm@9963
    80
     | "\\<plusminus>" => (1.0, "&plusmn;")
wenzelm@9963
    81
     | "\\<twosuperior>" => (1.0, "&sup2;")
wenzelm@9963
    82
     | "\\<threesuperior>" => (1.0, "&sup3;")
wenzelm@10837
    83
     | "\\<acute>" => (1.0, "&acute;")
wenzelm@9963
    84
     | "\\<mu>" => (1.0, "&micro;")
wenzelm@9963
    85
     | "\\<paragraph>" => (1.0, "&para;")
wenzelm@6338
    86
     | "\\<cdot>" => (1.0, "&middot;")
wenzelm@10837
    87
     | "\\<cedilla>" => (1.0, "&cedil;")
wenzelm@9963
    88
     | "\\<onesuperior>" => (1.0, "&sup1;")
wenzelm@9963
    89
     | "\\<ordmasculine>" => (1.0, "&ordm;")
wenzelm@9963
    90
     | "\\<guillemotright>" => (1.0, "&raquo;")
wenzelm@9963
    91
     | "\\<onequarter>" => (1.0, "&frac14;")
wenzelm@9963
    92
     | "\\<onehalf>" => (1.0, "&frac12;")
wenzelm@9963
    93
     | "\\<threequarters>" => (1.0, "&frac34;")
wenzelm@9963
    94
     | "\\<questiondown>" => (1.0, "&iquest;")
wenzelm@6338
    95
     | "\\<times>" => (1.0, "&times;")
wenzelm@10837
    96
     | "\\<emptyset>" => (1.0, "&Oslash;")
wenzelm@9963
    97
     | "\\<div>" => (1.0, "&divide;")
kleing@14534
    98
     | "\\<^bsub>" => (0.0, "<sub>")
kleing@14534
    99
     | "\\<^esub>" => (0.0, "</sub>")
kleing@14534
   100
     | "\\<^bsup>" => (0.0, "<sup>")
kleing@14534
   101
     | "\\<^esup>" => (0.0, "</sup>")
kleing@14534
   102
(* keep \<^sub> etc, so it does not get destroyed by default case *)
kleing@14534
   103
     | "\\<^sup>" => (0.0, "\\<^sup>")
kleing@14534
   104
     | "\\<^sub>" => (0.0, "\\<^sub>")
kleing@14534
   105
     | "\\<^isup>" => (0.0, "\\<^isup>")
kleing@14534
   106
     | "\\<^isub>" => (0.0, "\\<^isub>")
wenzelm@6338
   107
     | s => (real (size s), implode (map escape (explode s)));
wenzelm@6324
   108
wenzelm@6338
   109
  fun add_sym (width, (w: real, s)) = (width + w, s);
kleing@14534
   110
kleing@14534
   111
  fun script (0, "\\<^sub>") = (1,"<sub>")
kleing@14534
   112
    | script (0, "\\<^isub>") = (1,"<sub>")
kleing@14534
   113
    | script (1, x) = (0, x ^ "</sub>")
kleing@14534
   114
    | script (0, "\\<^sup>") = (2,"<sup>")
kleing@14534
   115
    | script (0, "\\<^isup>") = (2,"<sup>")
kleing@14534
   116
    | script (2, x) = (0, x ^ "</sup>")
kleing@14534
   117
    | script (s, x) = (s,x);
kleing@14534
   118
kleing@14534
   119
  fun scrs (s, []) = (s,[])
kleing@14534
   120
    | scrs (s, x::xs) = let val (s', x') = script (s, x)
kleing@14534
   121
                            val (s'', xs') = scrs (s', xs)
kleing@14534
   122
                        in (s'', x'::xs') end;
kleing@14534
   123
                           
kleing@14534
   124
  fun scripts ss = #2 (scrs (0,ss));
wenzelm@6338
   125
in
wenzelm@6324
   126
wenzelm@6338
   127
fun output_width str =
wenzelm@6338
   128
  if not (exists_string (equal "<" orf equal ">" orf equal "&") str) then (str, real (size str))
wenzelm@6338
   129
  else
wenzelm@6338
   130
    let val (width, syms) = foldl_map add_sym (0.0, map output_sym (Symbol.explode str))
kleing@14534
   131
    in (implode (scripts syms), width) end;
wenzelm@6338
   132
wenzelm@6338
   133
val output = #1 o output_width;
kleing@14534
   134
val output_symbols = scripts o (map (#2 o output_sym))
wenzelm@6338
   135
wenzelm@6338
   136
end;
wenzelm@6338
   137
wenzelm@6324
   138
wenzelm@10954
   139
val _ = Symbol.add_mode htmlN (output_width, Symbol.default_indent);
wenzelm@6324
   140
wenzelm@6324
   141
wenzelm@6324
   142
(* token translations *)
wenzelm@6324
   143
wenzelm@6347
   144
fun color col =
wenzelm@6347
   145
  apfst (enclose ("<font color=" ^ quote col ^ ">") "</font>") o output_width;
wenzelm@6324
   146
wenzelm@6324
   147
val html_trans =
wenzelm@6324
   148
 [("class", color "red"),
wenzelm@6324
   149
  ("tfree", color "purple"),
wenzelm@6324
   150
  ("tvar",  color "purple"),
wenzelm@6324
   151
  ("free",  color "blue"),
wenzelm@6324
   152
  ("bound", color "green"),
wenzelm@6324
   153
  ("var",   color "blue"),
wenzelm@6324
   154
  ("xstr",  color "brown")];
wenzelm@6324
   155
wenzelm@6324
   156
wenzelm@6324
   157
wenzelm@6324
   158
(** HTML markup **)
wenzelm@6324
   159
wenzelm@6324
   160
type text = string;
wenzelm@6324
   161
wenzelm@6324
   162
wenzelm@6324
   163
(* atoms *)
wenzelm@6324
   164
wenzelm@6324
   165
val plain = output;
wenzelm@6324
   166
fun name s = "<i>" ^ output s ^ "</i>";
wenzelm@6324
   167
fun keyword s = "<b>" ^ output s ^ "</b>";
wenzelm@6324
   168
fun file_name s = "<tt>" ^ output s ^ "</tt>";
berghofe@6649
   169
val file_path = file_name o Url.pack;
wenzelm@6324
   170
wenzelm@6324
   171
wenzelm@6324
   172
(* misc *)
wenzelm@6324
   173
wenzelm@6324
   174
fun href_name s txt = "<a href=" ^ quote s ^ ">" ^ txt ^ "</a>";
berghofe@6649
   175
fun href_path path txt = href_name (Url.pack path) txt;
wenzelm@6376
   176
wenzelm@6376
   177
fun href_opt_name None txt = txt
wenzelm@6376
   178
  | href_opt_name (Some s) txt = href_name s txt;
wenzelm@6376
   179
wenzelm@6376
   180
fun href_opt_path None txt = txt
wenzelm@6376
   181
  | href_opt_path (Some p) txt = href_path p txt;
wenzelm@6376
   182
wenzelm@12413
   183
fun para txt = "\n<p>" ^ txt ^ "</p>\n";
wenzelm@6324
   184
fun preform txt = "<pre>" ^ txt ^ "</pre>";
wenzelm@6324
   185
val verbatim = preform o output;
wenzelm@6324
   186
wenzelm@6324
   187
wenzelm@6324
   188
(* document *)
wenzelm@6324
   189
wenzelm@6324
   190
fun begin_document title =
webertj@14083
   191
  "<!DOCTYPE HTML PUBLIC \"-//W3C//DTD HTML 4.01 Transitional//EN\" \"http://www.w3.org/TR/html4/loose.dtd\">\n\
webertj@14083
   192
  \\n\
webertj@14083
   193
  \<html>\n\
wenzelm@6405
   194
  \<head>\n\
webertj@14083
   195
  \<meta http-equiv=\"Content-Type\" content=\"text/html; charset=iso-8859-1\">\n\
wenzelm@6405
   196
  \<title>" ^ plain (title ^ " (" ^ version ^ ")") ^ "</title>\n\
wenzelm@6405
   197
  \</head>\n\
wenzelm@6405
   198
  \\n\
wenzelm@6405
   199
  \<body>\n\
wenzelm@6405
   200
  \<h1>" ^ plain title ^ "</h1>\n"
wenzelm@6324
   201
wenzelm@6405
   202
val end_document = "\n</body>\n</html>\n";
wenzelm@6324
   203
wenzelm@6754
   204
fun gen_link how (path, name) = para (href_path path how ^ " to index of " ^ plain name);
wenzelm@6754
   205
val up_link = gen_link "Up";
wenzelm@6754
   206
val back_link = gen_link "Back";
wenzelm@6338
   207
wenzelm@6338
   208
wenzelm@6338
   209
(* session index *)
wenzelm@6338
   210
wenzelm@7725
   211
fun begin_index up (index_path, session) opt_readme opt_doc graph =
wenzelm@6754
   212
  begin_document ("Index of " ^ session) ^ up_link up ^
wenzelm@6754
   213
  para ("View " ^ href_path graph "theory dependencies" ^
wenzelm@7725
   214
    (case opt_readme of None => "" | Some p => "<br>\nView " ^ href_path p "README") ^
wenzelm@7725
   215
    (case opt_doc of None => "" | Some p => "<br>\nView " ^ href_path p "document")) ^
wenzelm@6405
   216
  "\n<hr>\n\n<h2>Theories</h2>\n<ul>\n";
wenzelm@6338
   217
wenzelm@6338
   218
val end_index = end_document;
wenzelm@6338
   219
berghofe@6649
   220
fun choice chs s = space_implode " " (map (fn (s', lnk) =>
berghofe@6649
   221
  enclose "[" "]" (if s = s' then keyword s' else href_name lnk s')) chs);
berghofe@6649
   222
wenzelm@9415
   223
fun applet_pages session back =
berghofe@6649
   224
  let
wenzelm@9415
   225
    val sizes =
wenzelm@9415
   226
     [("small", "small.html", ("500", "400")),
wenzelm@9415
   227
      ("medium", "medium.html", ("650", "520")),
wenzelm@9415
   228
      ("large", "large.html", ("800", "640"))];
berghofe@6649
   229
wenzelm@9415
   230
    fun applet_page (size, name, (width, height)) =
wenzelm@6754
   231
      let
wenzelm@6754
   232
        val browser_size = "Set browser size: " ^
wenzelm@9415
   233
          choice (map (fn (y, z, _) => (y, z)) sizes) size;
wenzelm@6754
   234
      in
wenzelm@6754
   235
        (name, begin_document ("Theory dependencies of " ^ session) ^
wenzelm@6754
   236
          back_link back ^
wenzelm@9415
   237
          para browser_size ^
wenzelm@6754
   238
          "\n<hr>\n<applet code=\"GraphBrowser/GraphBrowser.class\" \
berghofe@9045
   239
          \width=" ^ width ^ " height=" ^ height ^ ">\n\
wenzelm@9415
   240
          \<param name=\"graphfile\" value=\"" ^ "session.graph" ^ "\">\n\
wenzelm@6754
   241
          \</applet>\n<hr>" ^ end_document)
berghofe@6649
   242
      end;
wenzelm@9415
   243
  in map applet_page sizes end;
berghofe@6649
   244
berghofe@6649
   245
wenzelm@6405
   246
fun entry (p, s) = "<li>" ^ href_path p (plain s) ^ "\n";
wenzelm@6405
   247
wenzelm@6338
   248
val theory_entry = entry;
wenzelm@6338
   249
wenzelm@6405
   250
fun session_entries [] = "</ul>"
wenzelm@6405
   251
  | session_entries es =
wenzelm@6405
   252
      "</ul>\n<hr>\n\n<h2>Sessions</h2>\n<ul>\n" ^ implode (map entry es) ^ "</ul>";
wenzelm@6324
   253
wenzelm@6324
   254
wenzelm@6324
   255
(* theory *)
wenzelm@6324
   256
wenzelm@7725
   257
fun verbatim_source ss = "\n<hr>\n<pre>" ^ implode (output_symbols ss)  ^ "</pre>\n<hr>\n";
wenzelm@6324
   258
wenzelm@6324
   259
wenzelm@6324
   260
local
wenzelm@7408
   261
  fun encl None = enclose "[" "]"
wenzelm@7408
   262
    | encl (Some false) = enclose "(" ")"
wenzelm@7408
   263
    | encl (Some true) = I;
wenzelm@6324
   264
wenzelm@7408
   265
  fun file (opt_ref, path, loadit) = href_opt_path opt_ref (encl loadit (file_path path));
wenzelm@7831
   266
  val files = space_implode " " o map file;
wenzelm@6376
   267
  val parents = space_implode " + " o map (uncurry href_opt_path o apsnd name);
wenzelm@6361
   268
wenzelm@6376
   269
  fun theory up A =
wenzelm@6376
   270
    begin_document ("Theory " ^ A) ^ "\n" ^ up_link up ^
wenzelm@6324
   271
    keyword "theory" ^ " " ^ name A ^ " = ";
wenzelm@6324
   272
in
wenzelm@6324
   273
wenzelm@6376
   274
fun begin_theory up A Bs [] body = theory up A ^ parents Bs ^ ":\n" ^ body
wenzelm@12413
   275
  | begin_theory up A Bs Ps body = theory up A ^ parents Bs ^ "<br>\n" ^ keyword "files" ^
wenzelm@6376
   276
      " " ^ files Ps ^ ":" ^ "\n" ^ body;
wenzelm@6324
   277
end;
wenzelm@6324
   278
wenzelm@6338
   279
val end_theory = end_document;
wenzelm@6324
   280
wenzelm@6324
   281
wenzelm@6324
   282
(* ML file *)
wenzelm@6324
   283
wenzelm@6324
   284
fun ml_file path str =
berghofe@6649
   285
  begin_document ("File " ^ Url.pack path) ^
wenzelm@6324
   286
  "\n<hr>\n" ^ verbatim str ^ "\n<hr>\n" ^ end_document;
wenzelm@6324
   287
wenzelm@6324
   288
wenzelm@7408
   289
(* theorems *)
wenzelm@6324
   290
wenzelm@7572
   291
local
wenzelm@7572
   292
wenzelm@7408
   293
val string_of_thm =
wenzelm@6324
   294
  Pretty.setmp_margin 80 Pretty.string_of o
wenzelm@6324
   295
    Display.pretty_thm_no_quote o #1 o Drule.freeze_thaw;
wenzelm@6324
   296
wenzelm@6324
   297
fun thm th = preform (prefix_lines "  " (html_mode string_of_thm th));
wenzelm@7408
   298
wenzelm@7572
   299
fun thm_name "" = ""
wenzelm@7572
   300
  | thm_name a = " " ^ name (a ^ ":");
wenzelm@7572
   301
wenzelm@7572
   302
in
wenzelm@7572
   303
wenzelm@13531
   304
fun result k (a, ths) = para (cat_lines ((keyword k ^ thm_name a) :: map thm ths));
wenzelm@7572
   305
wenzelm@13531
   306
fun results _ [] = ""
wenzelm@13531
   307
  | results k (res :: ress) = cat_lines (result k res :: map (result "and") ress);
wenzelm@7572
   308
wenzelm@7572
   309
end;
wenzelm@6324
   310
wenzelm@6324
   311
wenzelm@7634
   312
(* sections *)
wenzelm@6324
   313
wenzelm@8088
   314
fun chapter heading = "\n\n<h1>" ^ plain heading ^ "</h1>\n";
wenzelm@6324
   315
fun section heading = "\n\n<h2>" ^ plain heading ^ "</h2>\n";
wenzelm@7634
   316
fun subsection heading = "\n\n<h3>" ^ plain heading ^ "</h3>\n";
wenzelm@7634
   317
fun subsubsection heading = "\n\n<h4>" ^ plain heading ^ "</h4>\n";
wenzelm@6324
   318
wenzelm@6324
   319
wenzelm@6324
   320
wenzelm@6324
   321
(** theory setup **)
wenzelm@6324
   322
wenzelm@6324
   323
val setup =
wenzelm@6324
   324
 [Theory.add_mode_tokentrfuns htmlN html_trans];
wenzelm@6324
   325
wenzelm@6324
   326
wenzelm@6324
   327
end;