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