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