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