src/Pure/Thy/html.ML
author wenzelm
Tue Mar 09 12:12:45 1999 +0100 (1999-03-09)
changeset 6324 3b7111b360b1
child 6338 bf0d22535e47
permissions -rw-r--r--
HTML markup elements.
wenzelm@6324
     1
(*  Title:      Pure/Thy/HTML.ML
wenzelm@6324
     2
    ID:         $Id$
wenzelm@6324
     3
    Author:     Markus Wenzel, TU Muenchen
wenzelm@6324
     4
wenzelm@6324
     5
HTML markup 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
wenzelm@6324
    17
  val file_path: Path.T -> text
wenzelm@6324
    18
  val para: text -> text
wenzelm@6324
    19
  val href_name: string -> text -> text
wenzelm@6324
    20
  val href_path: Path.T -> text -> text
wenzelm@6324
    21
  val preform: text -> text
wenzelm@6324
    22
  val verbatim: string -> text
wenzelm@6324
    23
  val begin_document: string -> text
wenzelm@6324
    24
  val end_document: text
wenzelm@6324
    25
  val insert_here: text
wenzelm@6324
    26
  val source: (string, 'a) Source.source -> text
wenzelm@6324
    27
  val begin_theory: Path.T * string -> string -> string list -> ((Path.T * Path.T) * bool) list
wenzelm@6324
    28
    -> text -> text
wenzelm@6324
    29
  val end_theory: text
wenzelm@6324
    30
  val ml_file: Path.T -> string -> text
wenzelm@6324
    31
  val conclude_theory: text
wenzelm@6324
    32
  val theorem: string -> thm -> text
wenzelm@6324
    33
  val section: string -> text
wenzelm@6324
    34
  val setup: (theory -> theory) list
wenzelm@6324
    35
end;
wenzelm@6324
    36
wenzelm@6324
    37
structure HTML: HTML =
wenzelm@6324
    38
struct
wenzelm@6324
    39
wenzelm@6324
    40
wenzelm@6324
    41
(** HTML print modes **)
wenzelm@6324
    42
wenzelm@6324
    43
(* mode *)
wenzelm@6324
    44
wenzelm@6324
    45
val htmlN = "HTML";
wenzelm@6324
    46
fun html_mode f x = setmp print_mode [htmlN] f x;
wenzelm@6324
    47
wenzelm@6324
    48
wenzelm@6324
    49
(* symbol output *)
wenzelm@6324
    50
wenzelm@6324
    51
val escape = fn "<" => "&lt;" | ">" => "&gt;" | "&" => "&amp;" | c => c;
wenzelm@6324
    52
wenzelm@6324
    53
val output_chars = implode o map escape;
wenzelm@6324
    54
wenzelm@6324
    55
fun output s =
wenzelm@6324
    56
  if not (exists_string (equal "<" orf equal ">" orf equal "&") s) then s
wenzelm@6324
    57
  else implode (map escape (explode s));        (*sic!*)
wenzelm@6324
    58
wenzelm@6324
    59
fun output_width s = (output s, real (size s));
wenzelm@6324
    60
wenzelm@6324
    61
val _ = Symbol.add_mode htmlN output_width;
wenzelm@6324
    62
wenzelm@6324
    63
wenzelm@6324
    64
(* token translations *)
wenzelm@6324
    65
wenzelm@6324
    66
fun tagit bg en = apfst (enclose bg en) o output_width;
wenzelm@6324
    67
fun color col = tagit ("<font color=" ^ quote col ^ ">") "</font>";
wenzelm@6324
    68
wenzelm@6324
    69
val html_trans =
wenzelm@6324
    70
 [("class", color "red"),
wenzelm@6324
    71
  ("tfree", color "purple"),
wenzelm@6324
    72
  ("tvar",  color "purple"),
wenzelm@6324
    73
  ("free",  color "blue"),
wenzelm@6324
    74
  ("bound", color "green"),
wenzelm@6324
    75
  ("var",   color "blue"),
wenzelm@6324
    76
  ("xnum",  color "yellow"),
wenzelm@6324
    77
  ("xstr",  color "brown")];
wenzelm@6324
    78
wenzelm@6324
    79
wenzelm@6324
    80
wenzelm@6324
    81
(** HTML markup **)
wenzelm@6324
    82
wenzelm@6324
    83
type text = string;
wenzelm@6324
    84
wenzelm@6324
    85
wenzelm@6324
    86
(* atoms *)
wenzelm@6324
    87
wenzelm@6324
    88
val plain = output;
wenzelm@6324
    89
fun name s = "<i>" ^ output s ^ "</i>";
wenzelm@6324
    90
fun keyword s = "<b>" ^ output s ^ "</b>";
wenzelm@6324
    91
fun file_name s = "<tt>" ^ output s ^ "</tt>";
wenzelm@6324
    92
val file_path = file_name o Path.pack;
wenzelm@6324
    93
wenzelm@6324
    94
wenzelm@6324
    95
(* misc *)
wenzelm@6324
    96
wenzelm@6324
    97
fun para txt = "\n<p>\n" ^ txt ^ "\n</p>\n";
wenzelm@6324
    98
fun href_name s txt = "<a href=" ^ quote s ^ ">" ^ txt ^ "</a>";
wenzelm@6324
    99
fun href_path path txt = href_name (Path.pack path) txt;
wenzelm@6324
   100
fun preform txt = "<pre>" ^ txt ^ "</pre>";
wenzelm@6324
   101
val verbatim = preform o output;
wenzelm@6324
   102
wenzelm@6324
   103
wenzelm@6324
   104
(* document *)
wenzelm@6324
   105
wenzelm@6324
   106
fun begin_document title =
wenzelm@6324
   107
  let val txt = plain title in
wenzelm@6324
   108
    "<html>\n\
wenzelm@6324
   109
    \<head>\n\
wenzelm@6324
   110
    \<title>" ^ txt ^ "</title>\n\
wenzelm@6324
   111
    \</head>\n\
wenzelm@6324
   112
    \\n\
wenzelm@6324
   113
    \<body>\n\
wenzelm@6324
   114
    \<h1>" ^ txt ^ "</h1>\n"
wenzelm@6324
   115
  end;
wenzelm@6324
   116
wenzelm@6324
   117
val end_document =
wenzelm@6324
   118
  "</body>\n\
wenzelm@6324
   119
  \</html>\n";
wenzelm@6324
   120
wenzelm@6324
   121
val insert_here = "<!--insert--here-->";
wenzelm@6324
   122
wenzelm@6324
   123
wenzelm@6324
   124
(* theory *)
wenzelm@6324
   125
wenzelm@6324
   126
fun source src =
wenzelm@6324
   127
  "\n<hr>\n<pre>" ^ output_chars (Source.exhaust src) ^ "</pre>\n<hr>\n";
wenzelm@6324
   128
wenzelm@6324
   129
wenzelm@6324
   130
local
wenzelm@6324
   131
  fun file ((p, p'), loadit) =
wenzelm@6324
   132
    href_path p' ((if not loadit then enclose "(" ")" else I) (file_path p));
wenzelm@6324
   133
wenzelm@6324
   134
  fun suffix_last _ [] = []
wenzelm@6324
   135
    | suffix_last s lst = let val (xs, x) = split_last lst in xs @ [x ^ s] end;
wenzelm@6324
   136
wenzelm@6324
   137
  val plus_names = space_implode " + " o map name;
wenzelm@6324
   138
wenzelm@6324
   139
  fun theory (back_path, back_name) A =
wenzelm@6324
   140
    begin_document ("Theory " ^ A) ^ "\n" ^
wenzelm@6324
   141
    href_path back_path "Back" ^ " to the index of " ^ plain back_name ^ "\n<p>\n" ^
wenzelm@6324
   142
    keyword "theory" ^ " " ^ name A ^ " = ";
wenzelm@6324
   143
in
wenzelm@6324
   144
wenzelm@6324
   145
fun begin_theory back A Bs [] body = theory back A ^ plus_names (suffix_last ":" Bs) ^ "\n" ^ body
wenzelm@6324
   146
  | begin_theory back A Bs Ps body =
wenzelm@6324
   147
      theory back A ^ plus_names Bs ^
wenzelm@6324
   148
      "<br>" ^ keyword "files" ^ " " ^ space_implode " + " (map file Ps) ^ ":" ^ "\n" ^ body;
wenzelm@6324
   149
end;
wenzelm@6324
   150
wenzelm@6324
   151
val end_theory = "";
wenzelm@6324
   152
val conclude_theory = end_document;
wenzelm@6324
   153
wenzelm@6324
   154
wenzelm@6324
   155
(* ML file *)
wenzelm@6324
   156
wenzelm@6324
   157
fun ml_file path str =
wenzelm@6324
   158
  begin_document ("File " ^ Path.pack path) ^
wenzelm@6324
   159
  "\n<hr>\n" ^ verbatim str ^ "\n<hr>\n" ^ end_document;
wenzelm@6324
   160
wenzelm@6324
   161
wenzelm@6324
   162
(* theorem *)
wenzelm@6324
   163
wenzelm@6324
   164
(* FIXME improve freeze_thaw (?) *)
wenzelm@6324
   165
val string_of_thm =
wenzelm@6324
   166
  Pretty.setmp_margin 80 Pretty.string_of o
wenzelm@6324
   167
    Display.pretty_thm_no_quote o #1 o Drule.freeze_thaw;
wenzelm@6324
   168
wenzelm@6324
   169
fun thm th = preform (prefix_lines "  " (html_mode string_of_thm th));
wenzelm@6324
   170
fun theorem a th = para (keyword "theorem" ^ " " ^ name (a ^ ":") ^ "\n" ^ thm th);
wenzelm@6324
   171
wenzelm@6324
   172
wenzelm@6324
   173
(* section *)
wenzelm@6324
   174
wenzelm@6324
   175
fun section heading = "\n\n<h2>" ^ plain heading ^ "</h2>\n";
wenzelm@6324
   176
wenzelm@6324
   177
wenzelm@6324
   178
wenzelm@6324
   179
(** theory setup **)
wenzelm@6324
   180
wenzelm@6324
   181
val setup =
wenzelm@6324
   182
 [Theory.add_mode_tokentrfuns htmlN html_trans];
wenzelm@6324
   183
wenzelm@6324
   184
wenzelm@6324
   185
end;