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