src/Pure/Thy/html.ML
author wenzelm
Sun Jul 23 12:08:54 2000 +0200 (2000-07-23)
changeset 9415 daa2296f23ea
parent 9045 a5bfcd4c2a5e
child 9963 6342d9c7fe46
permissions -rw-r--r--
removed all_sessions;
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@7572
    37
  val result: string -> string -> thm -> text
wenzelm@7572
    38
  val results: string -> string -> thm list -> text
wenzelm@6324
    39
  val theorem: string -> thm -> text
wenzelm@7408
    40
  val theorems: string -> thm list -> text
wenzelm@8088
    41
  val chapter: string -> text
wenzelm@6324
    42
  val section: string -> text
wenzelm@7634
    43
  val subsection: string -> text
wenzelm@7634
    44
  val subsubsection: string -> text
wenzelm@6324
    45
  val setup: (theory -> theory) list
wenzelm@6324
    46
end;
wenzelm@6324
    47
wenzelm@6324
    48
structure HTML: HTML =
wenzelm@6324
    49
struct
wenzelm@6324
    50
wenzelm@6324
    51
wenzelm@6324
    52
(** HTML print modes **)
wenzelm@6324
    53
wenzelm@6324
    54
(* mode *)
wenzelm@6324
    55
wenzelm@6324
    56
val htmlN = "HTML";
wenzelm@6324
    57
fun html_mode f x = setmp print_mode [htmlN] f x;
wenzelm@6324
    58
wenzelm@6324
    59
wenzelm@6324
    60
(* symbol output *)
wenzelm@6324
    61
wenzelm@6338
    62
local
wenzelm@6338
    63
  val escape = fn "<" => "&lt;" | ">" => "&gt;" | "&" => "&amp;" | c => c;
wenzelm@6324
    64
wenzelm@6338
    65
  val output_sym =
wenzelm@6338
    66
    fn "\\<not>" => (1.0, "&not;")
wenzelm@6338
    67
     | "\\<hyphen>" => (1.0, "&shy;")
wenzelm@6338
    68
     | "\\<cdot>" => (1.0, "&middot;")
wenzelm@6338
    69
     | "\\<times>" => (1.0, "&times;")
wenzelm@6338
    70
     | "\\<copyright>" => (1.0, "&copy;")
wenzelm@6338
    71
     | "\\<mu>" => (1.0, "&micro;")
wenzelm@6338
    72
     | s => (real (size s), implode (map escape (explode s)));
wenzelm@6324
    73
wenzelm@6338
    74
  fun add_sym (width, (w: real, s)) = (width + w, s);
wenzelm@6338
    75
in
wenzelm@6324
    76
wenzelm@6338
    77
fun output_width str =
wenzelm@6338
    78
  if not (exists_string (equal "<" orf equal ">" orf equal "&") str) then (str, real (size str))
wenzelm@6338
    79
  else
wenzelm@6338
    80
    let val (width, syms) = foldl_map add_sym (0.0, map output_sym (Symbol.explode str))
wenzelm@6338
    81
    in (implode syms, width) end;
wenzelm@6338
    82
wenzelm@6338
    83
val output = #1 o output_width;
wenzelm@6338
    84
val output_symbols = map (#2 o output_sym);
wenzelm@6338
    85
wenzelm@6338
    86
end;
wenzelm@6338
    87
wenzelm@6324
    88
wenzelm@6324
    89
val _ = Symbol.add_mode htmlN output_width;
wenzelm@6324
    90
wenzelm@6324
    91
wenzelm@6324
    92
(* token translations *)
wenzelm@6324
    93
wenzelm@6347
    94
fun color col =
wenzelm@6347
    95
  apfst (enclose ("<font color=" ^ quote col ^ ">") "</font>") o output_width;
wenzelm@6324
    96
wenzelm@6324
    97
val html_trans =
wenzelm@6324
    98
 [("class", color "red"),
wenzelm@6324
    99
  ("tfree", color "purple"),
wenzelm@6324
   100
  ("tvar",  color "purple"),
wenzelm@6324
   101
  ("free",  color "blue"),
wenzelm@6324
   102
  ("bound", color "green"),
wenzelm@6324
   103
  ("var",   color "blue"),
wenzelm@6324
   104
  ("xnum",  color "yellow"),
wenzelm@6324
   105
  ("xstr",  color "brown")];
wenzelm@6324
   106
wenzelm@6324
   107
wenzelm@6324
   108
wenzelm@6324
   109
(** HTML markup **)
wenzelm@6324
   110
wenzelm@6324
   111
type text = string;
wenzelm@6324
   112
wenzelm@6324
   113
wenzelm@6324
   114
(* atoms *)
wenzelm@6324
   115
wenzelm@6324
   116
val plain = output;
wenzelm@6324
   117
fun name s = "<i>" ^ output s ^ "</i>";
wenzelm@6324
   118
fun keyword s = "<b>" ^ output s ^ "</b>";
wenzelm@6324
   119
fun file_name s = "<tt>" ^ output s ^ "</tt>";
berghofe@6649
   120
val file_path = file_name o Url.pack;
wenzelm@6324
   121
wenzelm@6324
   122
wenzelm@6324
   123
(* misc *)
wenzelm@6324
   124
wenzelm@6324
   125
fun href_name s txt = "<a href=" ^ quote s ^ ">" ^ txt ^ "</a>";
berghofe@6649
   126
fun href_path path txt = href_name (Url.pack path) txt;
wenzelm@6376
   127
wenzelm@6376
   128
fun href_opt_name None txt = txt
wenzelm@6376
   129
  | href_opt_name (Some s) txt = href_name s txt;
wenzelm@6376
   130
wenzelm@6376
   131
fun href_opt_path None txt = txt
wenzelm@6376
   132
  | href_opt_path (Some p) txt = href_path p txt;
wenzelm@6376
   133
wenzelm@6376
   134
fun para txt = "\n<p>\n" ^ txt ^ "\n</p>\n";
wenzelm@6324
   135
fun preform txt = "<pre>" ^ txt ^ "</pre>";
wenzelm@6324
   136
val verbatim = preform o output;
wenzelm@6324
   137
wenzelm@6324
   138
wenzelm@6324
   139
(* document *)
wenzelm@6324
   140
wenzelm@6324
   141
fun begin_document title =
wenzelm@6405
   142
  "<html>\n\
wenzelm@6405
   143
  \<head>\n\
wenzelm@6405
   144
  \<title>" ^ plain (title ^ " (" ^ version ^ ")") ^ "</title>\n\
wenzelm@6405
   145
  \</head>\n\
wenzelm@6405
   146
  \\n\
wenzelm@6405
   147
  \<body>\n\
wenzelm@6405
   148
  \<h1>" ^ plain title ^ "</h1>\n"
wenzelm@6324
   149
wenzelm@6405
   150
val end_document = "\n</body>\n</html>\n";
wenzelm@6324
   151
wenzelm@6754
   152
fun gen_link how (path, name) = para (href_path path how ^ " to index of " ^ plain name);
wenzelm@6754
   153
val up_link = gen_link "Up";
wenzelm@6754
   154
val back_link = gen_link "Back";
wenzelm@6338
   155
wenzelm@6338
   156
wenzelm@6338
   157
(* session index *)
wenzelm@6338
   158
wenzelm@7725
   159
fun begin_index up (index_path, session) opt_readme opt_doc graph =
wenzelm@6754
   160
  begin_document ("Index of " ^ session) ^ up_link up ^
wenzelm@6754
   161
  para ("View " ^ href_path graph "theory dependencies" ^
wenzelm@7725
   162
    (case opt_readme of None => "" | Some p => "<br>\nView " ^ href_path p "README") ^
wenzelm@7725
   163
    (case opt_doc of None => "" | Some p => "<br>\nView " ^ href_path p "document")) ^
wenzelm@6405
   164
  "\n<hr>\n\n<h2>Theories</h2>\n<ul>\n";
wenzelm@6338
   165
wenzelm@6338
   166
val end_index = end_document;
wenzelm@6338
   167
berghofe@6649
   168
fun choice chs s = space_implode " " (map (fn (s', lnk) =>
berghofe@6649
   169
  enclose "[" "]" (if s = s' then keyword s' else href_name lnk s')) chs);
berghofe@6649
   170
wenzelm@9415
   171
fun applet_pages session back =
berghofe@6649
   172
  let
wenzelm@9415
   173
    val sizes =
wenzelm@9415
   174
     [("small", "small.html", ("500", "400")),
wenzelm@9415
   175
      ("medium", "medium.html", ("650", "520")),
wenzelm@9415
   176
      ("large", "large.html", ("800", "640"))];
berghofe@6649
   177
wenzelm@9415
   178
    fun applet_page (size, name, (width, height)) =
wenzelm@6754
   179
      let
wenzelm@6754
   180
        val browser_size = "Set browser size: " ^
wenzelm@9415
   181
          choice (map (fn (y, z, _) => (y, z)) sizes) size;
wenzelm@6754
   182
      in
wenzelm@6754
   183
        (name, begin_document ("Theory dependencies of " ^ session) ^
wenzelm@6754
   184
          back_link back ^
wenzelm@9415
   185
          para browser_size ^
wenzelm@6754
   186
          "\n<hr>\n<applet code=\"GraphBrowser/GraphBrowser.class\" \
berghofe@9045
   187
          \width=" ^ width ^ " height=" ^ height ^ ">\n\
wenzelm@9415
   188
          \<param name=\"graphfile\" value=\"" ^ "session.graph" ^ "\">\n\
wenzelm@6754
   189
          \</applet>\n<hr>" ^ end_document)
berghofe@6649
   190
      end;
wenzelm@9415
   191
  in map applet_page sizes end;
berghofe@6649
   192
berghofe@6649
   193
wenzelm@6405
   194
fun entry (p, s) = "<li>" ^ href_path p (plain s) ^ "\n";
wenzelm@6405
   195
wenzelm@6338
   196
val theory_entry = entry;
wenzelm@6338
   197
wenzelm@6405
   198
fun session_entries [] = "</ul>"
wenzelm@6405
   199
  | session_entries es =
wenzelm@6405
   200
      "</ul>\n<hr>\n\n<h2>Sessions</h2>\n<ul>\n" ^ implode (map entry es) ^ "</ul>";
wenzelm@6324
   201
wenzelm@6324
   202
wenzelm@6324
   203
(* theory *)
wenzelm@6324
   204
wenzelm@7725
   205
fun verbatim_source ss = "\n<hr>\n<pre>" ^ implode (output_symbols ss)  ^ "</pre>\n<hr>\n";
wenzelm@6324
   206
wenzelm@6324
   207
wenzelm@6324
   208
local
wenzelm@7408
   209
  fun encl None = enclose "[" "]"
wenzelm@7408
   210
    | encl (Some false) = enclose "(" ")"
wenzelm@7408
   211
    | encl (Some true) = I;
wenzelm@6324
   212
wenzelm@7408
   213
  fun file (opt_ref, path, loadit) = href_opt_path opt_ref (encl loadit (file_path path));
wenzelm@7831
   214
  val files = space_implode " " o map file;
wenzelm@6376
   215
  val parents = space_implode " + " o map (uncurry href_opt_path o apsnd name);
wenzelm@6361
   216
wenzelm@6376
   217
  fun theory up A =
wenzelm@6376
   218
    begin_document ("Theory " ^ A) ^ "\n" ^ up_link up ^
wenzelm@6324
   219
    keyword "theory" ^ " " ^ name A ^ " = ";
wenzelm@6324
   220
in
wenzelm@6324
   221
wenzelm@6376
   222
fun begin_theory up A Bs [] body = theory up A ^ parents Bs ^ ":\n" ^ body
wenzelm@6376
   223
  | begin_theory up A Bs Ps body = theory up A ^ parents Bs ^ "<br>" ^ keyword "files" ^
wenzelm@6376
   224
      " " ^ files Ps ^ ":" ^ "\n" ^ body;
wenzelm@6324
   225
end;
wenzelm@6324
   226
wenzelm@6338
   227
val end_theory = end_document;
wenzelm@6324
   228
wenzelm@6324
   229
wenzelm@6324
   230
(* ML file *)
wenzelm@6324
   231
wenzelm@6324
   232
fun ml_file path str =
berghofe@6649
   233
  begin_document ("File " ^ Url.pack path) ^
wenzelm@6324
   234
  "\n<hr>\n" ^ verbatim str ^ "\n<hr>\n" ^ end_document;
wenzelm@6324
   235
wenzelm@6324
   236
wenzelm@7408
   237
(* theorems *)
wenzelm@6324
   238
wenzelm@7572
   239
local
wenzelm@7572
   240
wenzelm@7408
   241
val string_of_thm =
wenzelm@6324
   242
  Pretty.setmp_margin 80 Pretty.string_of o
wenzelm@6324
   243
    Display.pretty_thm_no_quote o #1 o Drule.freeze_thaw;
wenzelm@6324
   244
wenzelm@6324
   245
fun thm th = preform (prefix_lines "  " (html_mode string_of_thm th));
wenzelm@7408
   246
wenzelm@7572
   247
fun thm_name "" = ""
wenzelm@7572
   248
  | thm_name a = " " ^ name (a ^ ":");
wenzelm@7572
   249
wenzelm@7572
   250
in
wenzelm@7572
   251
wenzelm@7572
   252
fun result k a th = para (keyword k ^ thm_name a ^ "\n" ^ thm th);
wenzelm@7572
   253
fun results k a ths = para (cat_lines ((keyword k ^ thm_name a) :: map thm ths));
wenzelm@7572
   254
wenzelm@7572
   255
val theorem = result "theorem";
wenzelm@7572
   256
val theorems = results "theorems";
wenzelm@7572
   257
wenzelm@7572
   258
end;
wenzelm@6324
   259
wenzelm@6324
   260
wenzelm@7634
   261
(* sections *)
wenzelm@6324
   262
wenzelm@8088
   263
fun chapter heading = "\n\n<h1>" ^ plain heading ^ "</h1>\n";
wenzelm@6324
   264
fun section heading = "\n\n<h2>" ^ plain heading ^ "</h2>\n";
wenzelm@7634
   265
fun subsection heading = "\n\n<h3>" ^ plain heading ^ "</h3>\n";
wenzelm@7634
   266
fun subsubsection heading = "\n\n<h4>" ^ plain heading ^ "</h4>\n";
wenzelm@6324
   267
wenzelm@6324
   268
wenzelm@6324
   269
wenzelm@6324
   270
(** theory setup **)
wenzelm@6324
   271
wenzelm@6324
   272
val setup =
wenzelm@6324
   273
 [Theory.add_mode_tokentrfuns htmlN html_trans];
wenzelm@6324
   274
wenzelm@6324
   275
wenzelm@6324
   276
end;