src/Pure/Thy/html.ML
author wenzelm
Wed, 29 Jun 2011 15:23:36 +0200
changeset 43592 e67d104c0c50
parent 43548 f231a7594e54
child 45666 d83797ef0d2d
permissions -rw-r--r--
HTML: render control symbols more like Isabelle/Scala/jEdit;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
24584
01e83ffa6c54 fixed title
haftmann
parents: 24244
diff changeset
     1
(*  Title:      Pure/Thy/html.ML
9415
daa2296f23ea removed all_sessions;
wenzelm
parents: 9045
diff changeset
     2
    Author:     Markus Wenzel and Stefan Berghofer, TU Muenchen
6324
3b7111b360b1 HTML markup elements.
wenzelm
parents:
diff changeset
     3
9415
daa2296f23ea removed all_sessions;
wenzelm
parents: 9045
diff changeset
     4
HTML presentation elements.
6324
3b7111b360b1 HTML markup elements.
wenzelm
parents:
diff changeset
     5
*)
3b7111b360b1 HTML markup elements.
wenzelm
parents:
diff changeset
     6
3b7111b360b1 HTML markup elements.
wenzelm
parents:
diff changeset
     7
signature HTML =
3b7111b360b1 HTML markup elements.
wenzelm
parents:
diff changeset
     8
sig
23724
6e95ed5f64da export html_mode, begin_document, end_document;
wenzelm
parents: 23703
diff changeset
     9
  val html_mode: ('a -> 'b) -> 'a -> 'b
23622
8ce09f692653 simplified pretty token metric: type int;
wenzelm
parents: 22796
diff changeset
    10
  type text = string
6324
3b7111b360b1 HTML markup elements.
wenzelm
parents:
diff changeset
    11
  val plain: string -> text
3b7111b360b1 HTML markup elements.
wenzelm
parents:
diff changeset
    12
  val name: string -> text
3b7111b360b1 HTML markup elements.
wenzelm
parents:
diff changeset
    13
  val keyword: string -> text
23622
8ce09f692653 simplified pretty token metric: type int;
wenzelm
parents: 22796
diff changeset
    14
  val command: string -> text
6324
3b7111b360b1 HTML markup elements.
wenzelm
parents:
diff changeset
    15
  val file_name: string -> text
6649
2156012be986 Reimplemented graph generator.
berghofe
parents: 6405
diff changeset
    16
  val file_path: Url.T -> text
6324
3b7111b360b1 HTML markup elements.
wenzelm
parents:
diff changeset
    17
  val href_name: string -> text -> text
6649
2156012be986 Reimplemented graph generator.
berghofe
parents: 6405
diff changeset
    18
  val href_path: Url.T -> text -> text
2156012be986 Reimplemented graph generator.
berghofe
parents: 6405
diff changeset
    19
  val href_opt_path: Url.T option -> text -> text
6376
wenzelm
parents: 6361
diff changeset
    20
  val para: text -> text
6324
3b7111b360b1 HTML markup elements.
wenzelm
parents:
diff changeset
    21
  val preform: text -> text
3b7111b360b1 HTML markup elements.
wenzelm
parents:
diff changeset
    22
  val verbatim: string -> text
23724
6e95ed5f64da export html_mode, begin_document, end_document;
wenzelm
parents: 23703
diff changeset
    23
  val begin_document: string -> text
6e95ed5f64da export html_mode, begin_document, end_document;
wenzelm
parents: 23703
diff changeset
    24
  val end_document: text
17080
c0c213a8f39c begin_index: list of docs;
wenzelm
parents: 16267
diff changeset
    25
  val begin_index: Url.T * string -> Url.T * string -> (Url.T * string) list -> Url.T -> text
9415
daa2296f23ea removed all_sessions;
wenzelm
parents: 9045
diff changeset
    26
  val applet_pages: string -> Url.T * string -> (string * string) list
6649
2156012be986 Reimplemented graph generator.
berghofe
parents: 6405
diff changeset
    27
  val theory_entry: Url.T * string -> text
2156012be986 Reimplemented graph generator.
berghofe
parents: 6405
diff changeset
    28
  val session_entries: (Url.T * string) list -> text
27861
911bf8e58c4c removed obsolete verbatim_source, results, chapter, section etc.;
wenzelm
parents: 27832
diff changeset
    29
  val theory_source: text -> text
6649
2156012be986 Reimplemented graph generator.
berghofe
parents: 6405
diff changeset
    30
  val begin_theory: Url.T * string -> string -> (Url.T option * string) list ->
27490
ac1d6e87aa52 removed unused href_opt_name;
wenzelm
parents: 26709
diff changeset
    31
    (Url.T * Url.T * bool) list -> text -> text
37940
4857eab31298 generic external source files -- nothing special about ML here;
wenzelm
parents: 37146
diff changeset
    32
  val external_file: Url.T -> string -> text
6324
3b7111b360b1 HTML markup elements.
wenzelm
parents:
diff changeset
    33
end;
3b7111b360b1 HTML markup elements.
wenzelm
parents:
diff changeset
    34
3b7111b360b1 HTML markup elements.
wenzelm
parents:
diff changeset
    35
structure HTML: HTML =
3b7111b360b1 HTML markup elements.
wenzelm
parents:
diff changeset
    36
struct
3b7111b360b1 HTML markup elements.
wenzelm
parents:
diff changeset
    37
3b7111b360b1 HTML markup elements.
wenzelm
parents:
diff changeset
    38
3b7111b360b1 HTML markup elements.
wenzelm
parents:
diff changeset
    39
(** HTML print modes **)
3b7111b360b1 HTML markup elements.
wenzelm
parents:
diff changeset
    40
3b7111b360b1 HTML markup elements.
wenzelm
parents:
diff changeset
    41
(* mode *)
3b7111b360b1 HTML markup elements.
wenzelm
parents:
diff changeset
    42
3b7111b360b1 HTML markup elements.
wenzelm
parents:
diff changeset
    43
val htmlN = "HTML";
37146
f652333bbf8e renamed structure PrintMode to Print_Mode, keeping the old name as legacy alias for some time;
wenzelm
parents: 34003
diff changeset
    44
fun html_mode f x = Print_Mode.with_modes [htmlN] f x;
6324
3b7111b360b1 HTML markup elements.
wenzelm
parents:
diff changeset
    45
3b7111b360b1 HTML markup elements.
wenzelm
parents:
diff changeset
    46
33985
1d33e85a3fa9 added markup for hidden text;
wenzelm
parents: 33983
diff changeset
    47
(* common markup *)
1d33e85a3fa9 added markup for hidden text;
wenzelm
parents: 33983
diff changeset
    48
1d33e85a3fa9 added markup for hidden text;
wenzelm
parents: 33983
diff changeset
    49
fun span class = ("<span class=" ^ quote (XML.text class) ^ ">", "</span>");
1d33e85a3fa9 added markup for hidden text;
wenzelm
parents: 33983
diff changeset
    50
43548
f231a7594e54 type classes: entity markup instead of old-style token markup;
wenzelm
parents: 43458
diff changeset
    51
fun span_class (name, props) =
f231a7594e54 type classes: entity markup instead of old-style token markup;
wenzelm
parents: 43458
diff changeset
    52
  (case Markup.get_entity_kind (name, props) of
f231a7594e54 type classes: entity markup instead of old-style token markup;
wenzelm
parents: 43458
diff changeset
    53
    SOME kind => Markup.entityN ^ "_" ^ name
f231a7594e54 type classes: entity markup instead of old-style token markup;
wenzelm
parents: 43458
diff changeset
    54
  | NONE => name);
f231a7594e54 type classes: entity markup instead of old-style token markup;
wenzelm
parents: 43458
diff changeset
    55
f231a7594e54 type classes: entity markup instead of old-style token markup;
wenzelm
parents: 43458
diff changeset
    56
val _ = Markup.add_mode htmlN (span o span_class);
33985
1d33e85a3fa9 added markup for hidden text;
wenzelm
parents: 33983
diff changeset
    57
1d33e85a3fa9 added markup for hidden text;
wenzelm
parents: 33983
diff changeset
    58
6324
3b7111b360b1 HTML markup elements.
wenzelm
parents:
diff changeset
    59
(* symbol output *)
3b7111b360b1 HTML markup elements.
wenzelm
parents:
diff changeset
    60
6338
bf0d22535e47 output: some symbol translations;
wenzelm
parents: 6324
diff changeset
    61
local
43592
e67d104c0c50 HTML: render control symbols more like Isabelle/Scala/jEdit;
wenzelm
parents: 43548
diff changeset
    62
  val hidden = span Markup.hiddenN |-> enclose;
33985
1d33e85a3fa9 added markup for hidden text;
wenzelm
parents: 33983
diff changeset
    63
43592
e67d104c0c50 HTML: render control symbols more like Isabelle/Scala/jEdit;
wenzelm
parents: 43548
diff changeset
    64
  (* FIXME proper unicode -- produced on Scala side *)
16196
abff174ba569 html_syms table;
wenzelm
parents: 15801
diff changeset
    65
  val html_syms = Symtab.make
34003
610e41138486 output_syms: permissive treatment of control symbols, cf. Scala version;
wenzelm
parents: 33986
diff changeset
    66
   [("", (0, "")),
610e41138486 output_syms: permissive treatment of control symbols, cf. Scala version;
wenzelm
parents: 33986
diff changeset
    67
    ("\n", (0, "<br/>")),
33986
041dc6d8d344 output linefeed as </br> -- workaround problem with <pre> in Lobo Browser 0.98.4;
wenzelm
parents: 33985
diff changeset
    68
    ("'", (1, "&#39;")),
33983
cfbf1ff6170d output "'" as "&#39;" which is a bit more portable ("&apos;" is defined in XML/XHTML, but not in old-style HTML4);
wenzelm
parents: 33222
diff changeset
    69
    ("\\<spacespace>", (2, "&nbsp;&nbsp;")),
23622
8ce09f692653 simplified pretty token metric: type int;
wenzelm
parents: 22796
diff changeset
    70
    ("\\<exclamdown>", (1, "&iexcl;")),
8ce09f692653 simplified pretty token metric: type int;
wenzelm
parents: 22796
diff changeset
    71
    ("\\<cent>", (1, "&cent;")),
8ce09f692653 simplified pretty token metric: type int;
wenzelm
parents: 22796
diff changeset
    72
    ("\\<pounds>", (1, "&pound;")),
8ce09f692653 simplified pretty token metric: type int;
wenzelm
parents: 22796
diff changeset
    73
    ("\\<currency>", (1, "&curren;")),
8ce09f692653 simplified pretty token metric: type int;
wenzelm
parents: 22796
diff changeset
    74
    ("\\<yen>", (1, "&yen;")),
8ce09f692653 simplified pretty token metric: type int;
wenzelm
parents: 22796
diff changeset
    75
    ("\\<bar>", (1, "&brvbar;")),
8ce09f692653 simplified pretty token metric: type int;
wenzelm
parents: 22796
diff changeset
    76
    ("\\<section>", (1, "&sect;")),
8ce09f692653 simplified pretty token metric: type int;
wenzelm
parents: 22796
diff changeset
    77
    ("\\<dieresis>", (1, "&uml;")),
8ce09f692653 simplified pretty token metric: type int;
wenzelm
parents: 22796
diff changeset
    78
    ("\\<copyright>", (1, "&copy;")),
8ce09f692653 simplified pretty token metric: type int;
wenzelm
parents: 22796
diff changeset
    79
    ("\\<ordfeminine>", (1, "&ordf;")),
8ce09f692653 simplified pretty token metric: type int;
wenzelm
parents: 22796
diff changeset
    80
    ("\\<guillemotleft>", (1, "&laquo;")),
8ce09f692653 simplified pretty token metric: type int;
wenzelm
parents: 22796
diff changeset
    81
    ("\\<not>", (1, "&not;")),
8ce09f692653 simplified pretty token metric: type int;
wenzelm
parents: 22796
diff changeset
    82
    ("\\<hyphen>", (1, "&shy;")),
8ce09f692653 simplified pretty token metric: type int;
wenzelm
parents: 22796
diff changeset
    83
    ("\\<registered>", (1, "&reg;")),
8ce09f692653 simplified pretty token metric: type int;
wenzelm
parents: 22796
diff changeset
    84
    ("\\<inverse>", (1, "&macr;")),
8ce09f692653 simplified pretty token metric: type int;
wenzelm
parents: 22796
diff changeset
    85
    ("\\<degree>", (1, "&deg;")),
8ce09f692653 simplified pretty token metric: type int;
wenzelm
parents: 22796
diff changeset
    86
    ("\\<plusminus>", (1, "&plusmn;")),
8ce09f692653 simplified pretty token metric: type int;
wenzelm
parents: 22796
diff changeset
    87
    ("\\<twosuperior>", (1, "&sup2;")),
8ce09f692653 simplified pretty token metric: type int;
wenzelm
parents: 22796
diff changeset
    88
    ("\\<threesuperior>", (1, "&sup3;")),
8ce09f692653 simplified pretty token metric: type int;
wenzelm
parents: 22796
diff changeset
    89
    ("\\<acute>", (1, "&acute;")),
8ce09f692653 simplified pretty token metric: type int;
wenzelm
parents: 22796
diff changeset
    90
    ("\\<paragraph>", (1, "&para;")),
8ce09f692653 simplified pretty token metric: type int;
wenzelm
parents: 22796
diff changeset
    91
    ("\\<cdot>", (1, "&middot;")),
8ce09f692653 simplified pretty token metric: type int;
wenzelm
parents: 22796
diff changeset
    92
    ("\\<cedilla>", (1, "&cedil;")),
8ce09f692653 simplified pretty token metric: type int;
wenzelm
parents: 22796
diff changeset
    93
    ("\\<onesuperior>", (1, "&sup1;")),
8ce09f692653 simplified pretty token metric: type int;
wenzelm
parents: 22796
diff changeset
    94
    ("\\<ordmasculine>", (1, "&ordm;")),
8ce09f692653 simplified pretty token metric: type int;
wenzelm
parents: 22796
diff changeset
    95
    ("\\<guillemotright>", (1, "&raquo;")),
8ce09f692653 simplified pretty token metric: type int;
wenzelm
parents: 22796
diff changeset
    96
    ("\\<onequarter>", (1, "&frac14;")),
8ce09f692653 simplified pretty token metric: type int;
wenzelm
parents: 22796
diff changeset
    97
    ("\\<onehalf>", (1, "&frac12;")),
8ce09f692653 simplified pretty token metric: type int;
wenzelm
parents: 22796
diff changeset
    98
    ("\\<threequarters>", (1, "&frac34;")),
8ce09f692653 simplified pretty token metric: type int;
wenzelm
parents: 22796
diff changeset
    99
    ("\\<questiondown>", (1, "&iquest;")),
8ce09f692653 simplified pretty token metric: type int;
wenzelm
parents: 22796
diff changeset
   100
    ("\\<times>", (1, "&times;")),
8ce09f692653 simplified pretty token metric: type int;
wenzelm
parents: 22796
diff changeset
   101
    ("\\<div>", (1, "&divide;")),
8ce09f692653 simplified pretty token metric: type int;
wenzelm
parents: 22796
diff changeset
   102
    ("\\<circ>", (1, "o")),
8ce09f692653 simplified pretty token metric: type int;
wenzelm
parents: 22796
diff changeset
   103
    ("\\<Alpha>", (1, "&Alpha;")),
8ce09f692653 simplified pretty token metric: type int;
wenzelm
parents: 22796
diff changeset
   104
    ("\\<Beta>", (1, "&Beta;")),
8ce09f692653 simplified pretty token metric: type int;
wenzelm
parents: 22796
diff changeset
   105
    ("\\<Gamma>", (1, "&Gamma;")),
8ce09f692653 simplified pretty token metric: type int;
wenzelm
parents: 22796
diff changeset
   106
    ("\\<Delta>", (1, "&Delta;")),
8ce09f692653 simplified pretty token metric: type int;
wenzelm
parents: 22796
diff changeset
   107
    ("\\<Epsilon>", (1, "&Epsilon;")),
8ce09f692653 simplified pretty token metric: type int;
wenzelm
parents: 22796
diff changeset
   108
    ("\\<Zeta>", (1, "&Zeta;")),
8ce09f692653 simplified pretty token metric: type int;
wenzelm
parents: 22796
diff changeset
   109
    ("\\<Eta>", (1, "&Eta;")),
8ce09f692653 simplified pretty token metric: type int;
wenzelm
parents: 22796
diff changeset
   110
    ("\\<Theta>", (1, "&Theta;")),
8ce09f692653 simplified pretty token metric: type int;
wenzelm
parents: 22796
diff changeset
   111
    ("\\<Iota>", (1, "&Iota;")),
8ce09f692653 simplified pretty token metric: type int;
wenzelm
parents: 22796
diff changeset
   112
    ("\\<Kappa>", (1, "&Kappa;")),
8ce09f692653 simplified pretty token metric: type int;
wenzelm
parents: 22796
diff changeset
   113
    ("\\<Lambda>", (1, "&Lambda;")),
8ce09f692653 simplified pretty token metric: type int;
wenzelm
parents: 22796
diff changeset
   114
    ("\\<Mu>", (1, "&Mu;")),
8ce09f692653 simplified pretty token metric: type int;
wenzelm
parents: 22796
diff changeset
   115
    ("\\<Nu>", (1, "&Nu;")),
8ce09f692653 simplified pretty token metric: type int;
wenzelm
parents: 22796
diff changeset
   116
    ("\\<Xi>", (1, "&Xi;")),
8ce09f692653 simplified pretty token metric: type int;
wenzelm
parents: 22796
diff changeset
   117
    ("\\<Omicron>", (1, "&Omicron;")),
8ce09f692653 simplified pretty token metric: type int;
wenzelm
parents: 22796
diff changeset
   118
    ("\\<Pi>", (1, "&Pi;")),
8ce09f692653 simplified pretty token metric: type int;
wenzelm
parents: 22796
diff changeset
   119
    ("\\<Rho>", (1, "&Rho;")),
8ce09f692653 simplified pretty token metric: type int;
wenzelm
parents: 22796
diff changeset
   120
    ("\\<Sigma>", (1, "&Sigma;")),
8ce09f692653 simplified pretty token metric: type int;
wenzelm
parents: 22796
diff changeset
   121
    ("\\<Tau>", (1, "&Tau;")),
8ce09f692653 simplified pretty token metric: type int;
wenzelm
parents: 22796
diff changeset
   122
    ("\\<Upsilon>", (1, "&Upsilon;")),
8ce09f692653 simplified pretty token metric: type int;
wenzelm
parents: 22796
diff changeset
   123
    ("\\<Phi>", (1, "&Phi;")),
8ce09f692653 simplified pretty token metric: type int;
wenzelm
parents: 22796
diff changeset
   124
    ("\\<Chi>", (1, "&Chi;")),
8ce09f692653 simplified pretty token metric: type int;
wenzelm
parents: 22796
diff changeset
   125
    ("\\<Psi>", (1, "&Psi;")),
8ce09f692653 simplified pretty token metric: type int;
wenzelm
parents: 22796
diff changeset
   126
    ("\\<Omega>", (1, "&Omega;")),
8ce09f692653 simplified pretty token metric: type int;
wenzelm
parents: 22796
diff changeset
   127
    ("\\<alpha>", (1, "&alpha;")),
8ce09f692653 simplified pretty token metric: type int;
wenzelm
parents: 22796
diff changeset
   128
    ("\\<beta>", (1, "&beta;")),
8ce09f692653 simplified pretty token metric: type int;
wenzelm
parents: 22796
diff changeset
   129
    ("\\<gamma>", (1, "&gamma;")),
8ce09f692653 simplified pretty token metric: type int;
wenzelm
parents: 22796
diff changeset
   130
    ("\\<delta>", (1, "&delta;")),
8ce09f692653 simplified pretty token metric: type int;
wenzelm
parents: 22796
diff changeset
   131
    ("\\<epsilon>", (1, "&epsilon;")),
8ce09f692653 simplified pretty token metric: type int;
wenzelm
parents: 22796
diff changeset
   132
    ("\\<zeta>", (1, "&zeta;")),
8ce09f692653 simplified pretty token metric: type int;
wenzelm
parents: 22796
diff changeset
   133
    ("\\<eta>", (1, "&eta;")),
8ce09f692653 simplified pretty token metric: type int;
wenzelm
parents: 22796
diff changeset
   134
    ("\\<theta>", (1, "&thetasym;")),
8ce09f692653 simplified pretty token metric: type int;
wenzelm
parents: 22796
diff changeset
   135
    ("\\<iota>", (1, "&iota;")),
8ce09f692653 simplified pretty token metric: type int;
wenzelm
parents: 22796
diff changeset
   136
    ("\\<kappa>", (1, "&kappa;")),
8ce09f692653 simplified pretty token metric: type int;
wenzelm
parents: 22796
diff changeset
   137
    ("\\<lambda>", (1, "&lambda;")),
8ce09f692653 simplified pretty token metric: type int;
wenzelm
parents: 22796
diff changeset
   138
    ("\\<mu>", (1, "&mu;")),
8ce09f692653 simplified pretty token metric: type int;
wenzelm
parents: 22796
diff changeset
   139
    ("\\<nu>", (1, "&nu;")),
8ce09f692653 simplified pretty token metric: type int;
wenzelm
parents: 22796
diff changeset
   140
    ("\\<xi>", (1, "&xi;")),
8ce09f692653 simplified pretty token metric: type int;
wenzelm
parents: 22796
diff changeset
   141
    ("\\<omicron>", (1, "&omicron;")),
8ce09f692653 simplified pretty token metric: type int;
wenzelm
parents: 22796
diff changeset
   142
    ("\\<pi>", (1, "&pi;")),
8ce09f692653 simplified pretty token metric: type int;
wenzelm
parents: 22796
diff changeset
   143
    ("\\<rho>", (1, "&rho;")),
8ce09f692653 simplified pretty token metric: type int;
wenzelm
parents: 22796
diff changeset
   144
    ("\\<sigma>", (1, "&sigma;")),
8ce09f692653 simplified pretty token metric: type int;
wenzelm
parents: 22796
diff changeset
   145
    ("\\<tau>", (1, "&tau;")),
8ce09f692653 simplified pretty token metric: type int;
wenzelm
parents: 22796
diff changeset
   146
    ("\\<upsilon>", (1, "&upsilon;")),
8ce09f692653 simplified pretty token metric: type int;
wenzelm
parents: 22796
diff changeset
   147
    ("\\<phi>", (1, "&phi;")),
8ce09f692653 simplified pretty token metric: type int;
wenzelm
parents: 22796
diff changeset
   148
    ("\\<chi>", (1, "&chi;")),
8ce09f692653 simplified pretty token metric: type int;
wenzelm
parents: 22796
diff changeset
   149
    ("\\<psi>", (1, "&psi;")),
8ce09f692653 simplified pretty token metric: type int;
wenzelm
parents: 22796
diff changeset
   150
    ("\\<omega>", (1, "&omega;")),
8ce09f692653 simplified pretty token metric: type int;
wenzelm
parents: 22796
diff changeset
   151
    ("\\<bullet>", (1, "&bull;")),
8ce09f692653 simplified pretty token metric: type int;
wenzelm
parents: 22796
diff changeset
   152
    ("\\<dots>", (1, "&hellip;")),
8ce09f692653 simplified pretty token metric: type int;
wenzelm
parents: 22796
diff changeset
   153
    ("\\<Re>", (1, "&real;")),
8ce09f692653 simplified pretty token metric: type int;
wenzelm
parents: 22796
diff changeset
   154
    ("\\<Im>", (1, "&image;")),
8ce09f692653 simplified pretty token metric: type int;
wenzelm
parents: 22796
diff changeset
   155
    ("\\<wp>", (1, "&weierp;")),
8ce09f692653 simplified pretty token metric: type int;
wenzelm
parents: 22796
diff changeset
   156
    ("\\<forall>", (1, "&forall;")),
8ce09f692653 simplified pretty token metric: type int;
wenzelm
parents: 22796
diff changeset
   157
    ("\\<partial>", (1, "&part;")),
8ce09f692653 simplified pretty token metric: type int;
wenzelm
parents: 22796
diff changeset
   158
    ("\\<exists>", (1, "&exist;")),
8ce09f692653 simplified pretty token metric: type int;
wenzelm
parents: 22796
diff changeset
   159
    ("\\<emptyset>", (1, "&empty;")),
8ce09f692653 simplified pretty token metric: type int;
wenzelm
parents: 22796
diff changeset
   160
    ("\\<nabla>", (1, "&nabla;")),
8ce09f692653 simplified pretty token metric: type int;
wenzelm
parents: 22796
diff changeset
   161
    ("\\<in>", (1, "&isin;")),
8ce09f692653 simplified pretty token metric: type int;
wenzelm
parents: 22796
diff changeset
   162
    ("\\<notin>", (1, "&notin;")),
8ce09f692653 simplified pretty token metric: type int;
wenzelm
parents: 22796
diff changeset
   163
    ("\\<Prod>", (1, "&prod;")),
8ce09f692653 simplified pretty token metric: type int;
wenzelm
parents: 22796
diff changeset
   164
    ("\\<Sum>", (1, "&sum;")),
8ce09f692653 simplified pretty token metric: type int;
wenzelm
parents: 22796
diff changeset
   165
    ("\\<star>", (1, "&lowast;")),
8ce09f692653 simplified pretty token metric: type int;
wenzelm
parents: 22796
diff changeset
   166
    ("\\<propto>", (1, "&prop;")),
8ce09f692653 simplified pretty token metric: type int;
wenzelm
parents: 22796
diff changeset
   167
    ("\\<infinity>", (1, "&infin;")),
8ce09f692653 simplified pretty token metric: type int;
wenzelm
parents: 22796
diff changeset
   168
    ("\\<angle>", (1, "&ang;")),
8ce09f692653 simplified pretty token metric: type int;
wenzelm
parents: 22796
diff changeset
   169
    ("\\<and>", (1, "&and;")),
8ce09f692653 simplified pretty token metric: type int;
wenzelm
parents: 22796
diff changeset
   170
    ("\\<or>", (1, "&or;")),
8ce09f692653 simplified pretty token metric: type int;
wenzelm
parents: 22796
diff changeset
   171
    ("\\<inter>", (1, "&cap;")),
8ce09f692653 simplified pretty token metric: type int;
wenzelm
parents: 22796
diff changeset
   172
    ("\\<union>", (1, "&cup;")),
8ce09f692653 simplified pretty token metric: type int;
wenzelm
parents: 22796
diff changeset
   173
    ("\\<sim>", (1, "&sim;")),
8ce09f692653 simplified pretty token metric: type int;
wenzelm
parents: 22796
diff changeset
   174
    ("\\<cong>", (1, "&cong;")),
8ce09f692653 simplified pretty token metric: type int;
wenzelm
parents: 22796
diff changeset
   175
    ("\\<approx>", (1, "&asymp;")),
8ce09f692653 simplified pretty token metric: type int;
wenzelm
parents: 22796
diff changeset
   176
    ("\\<noteq>", (1, "&ne;")),
8ce09f692653 simplified pretty token metric: type int;
wenzelm
parents: 22796
diff changeset
   177
    ("\\<equiv>", (1, "&equiv;")),
8ce09f692653 simplified pretty token metric: type int;
wenzelm
parents: 22796
diff changeset
   178
    ("\\<le>", (1, "&le;")),
8ce09f692653 simplified pretty token metric: type int;
wenzelm
parents: 22796
diff changeset
   179
    ("\\<ge>", (1, "&ge;")),
8ce09f692653 simplified pretty token metric: type int;
wenzelm
parents: 22796
diff changeset
   180
    ("\\<subset>", (1, "&sub;")),
8ce09f692653 simplified pretty token metric: type int;
wenzelm
parents: 22796
diff changeset
   181
    ("\\<supset>", (1, "&sup;")),
8ce09f692653 simplified pretty token metric: type int;
wenzelm
parents: 22796
diff changeset
   182
    ("\\<subseteq>", (1, "&sube;")),
8ce09f692653 simplified pretty token metric: type int;
wenzelm
parents: 22796
diff changeset
   183
    ("\\<supseteq>", (1, "&supe;")),
8ce09f692653 simplified pretty token metric: type int;
wenzelm
parents: 22796
diff changeset
   184
    ("\\<oplus>", (1, "&oplus;")),
8ce09f692653 simplified pretty token metric: type int;
wenzelm
parents: 22796
diff changeset
   185
    ("\\<otimes>", (1, "&otimes;")),
8ce09f692653 simplified pretty token metric: type int;
wenzelm
parents: 22796
diff changeset
   186
    ("\\<bottom>", (1, "&perp;")),
8ce09f692653 simplified pretty token metric: type int;
wenzelm
parents: 22796
diff changeset
   187
    ("\\<lceil>", (1, "&lceil;")),
8ce09f692653 simplified pretty token metric: type int;
wenzelm
parents: 22796
diff changeset
   188
    ("\\<rceil>", (1, "&rceil;")),
8ce09f692653 simplified pretty token metric: type int;
wenzelm
parents: 22796
diff changeset
   189
    ("\\<lfloor>", (1, "&lfloor;")),
8ce09f692653 simplified pretty token metric: type int;
wenzelm
parents: 22796
diff changeset
   190
    ("\\<rfloor>", (1, "&rfloor;")),
8ce09f692653 simplified pretty token metric: type int;
wenzelm
parents: 22796
diff changeset
   191
    ("\\<langle>", (1, "&lang;")),
8ce09f692653 simplified pretty token metric: type int;
wenzelm
parents: 22796
diff changeset
   192
    ("\\<rangle>", (1, "&rang;")),
8ce09f692653 simplified pretty token metric: type int;
wenzelm
parents: 22796
diff changeset
   193
    ("\\<lozenge>", (1, "&loz;")),
8ce09f692653 simplified pretty token metric: type int;
wenzelm
parents: 22796
diff changeset
   194
    ("\\<spadesuit>", (1, "&spades;")),
8ce09f692653 simplified pretty token metric: type int;
wenzelm
parents: 22796
diff changeset
   195
    ("\\<clubsuit>", (1, "&clubs;")),
8ce09f692653 simplified pretty token metric: type int;
wenzelm
parents: 22796
diff changeset
   196
    ("\\<heartsuit>", (1, "&hearts;")),
8ce09f692653 simplified pretty token metric: type int;
wenzelm
parents: 22796
diff changeset
   197
    ("\\<diamondsuit>", (1, "&diams;")),
8ce09f692653 simplified pretty token metric: type int;
wenzelm
parents: 22796
diff changeset
   198
    ("\\<lbrakk>", (2, "[|")),
8ce09f692653 simplified pretty token metric: type int;
wenzelm
parents: 22796
diff changeset
   199
    ("\\<rbrakk>", (2, "|]")),
8ce09f692653 simplified pretty token metric: type int;
wenzelm
parents: 22796
diff changeset
   200
    ("\\<Longrightarrow>", (3, "==&gt;")),
8ce09f692653 simplified pretty token metric: type int;
wenzelm
parents: 22796
diff changeset
   201
    ("\\<Rightarrow>", (2, "=&gt;")),
8ce09f692653 simplified pretty token metric: type int;
wenzelm
parents: 22796
diff changeset
   202
    ("\\<And>", (2, "!!")),
8ce09f692653 simplified pretty token metric: type int;
wenzelm
parents: 22796
diff changeset
   203
    ("\\<Colon>", (2, "::")),
8ce09f692653 simplified pretty token metric: type int;
wenzelm
parents: 22796
diff changeset
   204
    ("\\<lparr>", (2, "(|")),
8ce09f692653 simplified pretty token metric: type int;
wenzelm
parents: 22796
diff changeset
   205
    ("\\<rparr>", (2, "|)),")),
8ce09f692653 simplified pretty token metric: type int;
wenzelm
parents: 22796
diff changeset
   206
    ("\\<longleftrightarrow>", (3, "&lt;-&gt;")),
8ce09f692653 simplified pretty token metric: type int;
wenzelm
parents: 22796
diff changeset
   207
    ("\\<longrightarrow>", (3, "--&gt;")),
8ce09f692653 simplified pretty token metric: type int;
wenzelm
parents: 22796
diff changeset
   208
    ("\\<rightarrow>", (2, "-&gt;")),
43592
e67d104c0c50 HTML: render control symbols more like Isabelle/Scala/jEdit;
wenzelm
parents: 43548
diff changeset
   209
    ("\\<^bsub>", (0, hidden "&#8664;" ^ "<sub>")),
e67d104c0c50 HTML: render control symbols more like Isabelle/Scala/jEdit;
wenzelm
parents: 43548
diff changeset
   210
    ("\\<^esub>", (0, hidden "&#8665;" ^ "</sub>")),
e67d104c0c50 HTML: render control symbols more like Isabelle/Scala/jEdit;
wenzelm
parents: 43548
diff changeset
   211
    ("\\<^bsup>", (0, hidden "&#8663;" ^ "<sup>")),
e67d104c0c50 HTML: render control symbols more like Isabelle/Scala/jEdit;
wenzelm
parents: 43548
diff changeset
   212
    ("\\<^esup>", (0, hidden "&#8662;" ^ "</sup>"))];
17178
18a98ecc6821 output \<^loc> as 'loc' span;
wenzelm
parents: 17116
diff changeset
   213
16196
abff174ba569 html_syms table;
wenzelm
parents: 15801
diff changeset
   214
  fun output_sym s =
23622
8ce09f692653 simplified pretty token metric: type int;
wenzelm
parents: 22796
diff changeset
   215
    if Symbol.is_raw s then (1, Symbol.decode_raw s)
20742
2233f6afc491 reverted to 1.58;
wenzelm
parents: 20576
diff changeset
   216
    else
33983
cfbf1ff6170d output "'" as "&#39;" which is a bit more portable ("&apos;" is defined in XML/XHTML, but not in old-style HTML4);
wenzelm
parents: 33222
diff changeset
   217
      (case Symtab.lookup html_syms s of
cfbf1ff6170d output "'" as "&#39;" which is a bit more portable ("&apos;" is defined in XML/XHTML, but not in old-style HTML4);
wenzelm
parents: 33222
diff changeset
   218
        SOME x => x
26709
f963ea18a579 replaced token translations by common markup;
wenzelm
parents: 26463
diff changeset
   219
      | NONE => (size s, XML.text s));
6324
3b7111b360b1 HTML markup elements.
wenzelm
parents:
diff changeset
   220
33985
1d33e85a3fa9 added markup for hidden text;
wenzelm
parents: 33983
diff changeset
   221
  fun output_markup (bg, en) s1 s2 =
1d33e85a3fa9 added markup for hidden text;
wenzelm
parents: 33983
diff changeset
   222
    let val (n, txt) = output_sym s2
1d33e85a3fa9 added markup for hidden text;
wenzelm
parents: 33983
diff changeset
   223
    in (n, hidden s1 ^ enclose bg en txt) end;
14534
7a46bdcd92f2 treat sub/super scripts
kleing
parents: 14083
diff changeset
   224
33985
1d33e85a3fa9 added markup for hidden text;
wenzelm
parents: 33983
diff changeset
   225
  val output_sub = output_markup ("<sub>", "</sub>");
1d33e85a3fa9 added markup for hidden text;
wenzelm
parents: 33983
diff changeset
   226
  val output_sup = output_markup ("<sup>", "</sup>");
1d33e85a3fa9 added markup for hidden text;
wenzelm
parents: 33983
diff changeset
   227
  val output_bold = output_markup (span "bold");
1d33e85a3fa9 added markup for hidden text;
wenzelm
parents: 33983
diff changeset
   228
41482
f4c07fdd1d48 more scalable HTML.output_width;
wenzelm
parents: 40946
diff changeset
   229
  fun output_syms [] (result, width) = (implode (rev result), width)
f4c07fdd1d48 more scalable HTML.output_width;
wenzelm
parents: 40946
diff changeset
   230
    | output_syms (s1 :: rest) (result, width) =
f4c07fdd1d48 more scalable HTML.output_width;
wenzelm
parents: 40946
diff changeset
   231
        let
f4c07fdd1d48 more scalable HTML.output_width;
wenzelm
parents: 40946
diff changeset
   232
          val (s2, ss) = (case rest of [] => ("", []) | s2 :: ss => (s2, ss));
f4c07fdd1d48 more scalable HTML.output_width;
wenzelm
parents: 40946
diff changeset
   233
          val ((w, s), r) =
43592
e67d104c0c50 HTML: render control symbols more like Isabelle/Scala/jEdit;
wenzelm
parents: 43548
diff changeset
   234
            if s1 = "\\<^sub>" then (output_sub "&#8681;" s2, ss)
e67d104c0c50 HTML: render control symbols more like Isabelle/Scala/jEdit;
wenzelm
parents: 43548
diff changeset
   235
            else if s1 = "\\<^isub>" then (output_sub "&#8675;" s2, ss)
e67d104c0c50 HTML: render control symbols more like Isabelle/Scala/jEdit;
wenzelm
parents: 43548
diff changeset
   236
            else if s1 = "\\<^sup>" then (output_sup "&#8679;" s2, ss)
e67d104c0c50 HTML: render control symbols more like Isabelle/Scala/jEdit;
wenzelm
parents: 43548
diff changeset
   237
            else if s1 = "\\<^isup>" then (output_sup "&#8673;" s2, ss)
e67d104c0c50 HTML: render control symbols more like Isabelle/Scala/jEdit;
wenzelm
parents: 43548
diff changeset
   238
            else if s1 = "\\<^bold>" then (output_bold "&#10073;" s2, ss)
41482
f4c07fdd1d48 more scalable HTML.output_width;
wenzelm
parents: 40946
diff changeset
   239
            else (output_sym s1, rest);
f4c07fdd1d48 more scalable HTML.output_width;
wenzelm
parents: 40946
diff changeset
   240
        in output_syms r (s :: result, width + w) end;
6338
bf0d22535e47 output: some symbol translations;
wenzelm
parents: 6324
diff changeset
   241
in
6324
3b7111b360b1 HTML markup elements.
wenzelm
parents:
diff changeset
   242
41482
f4c07fdd1d48 more scalable HTML.output_width;
wenzelm
parents: 40946
diff changeset
   243
fun output_width str = output_syms (Symbol.explode str) ([], 0);
6338
bf0d22535e47 output: some symbol translations;
wenzelm
parents: 6324
diff changeset
   244
val output = #1 o output_width;
bf0d22535e47 output: some symbol translations;
wenzelm
parents: 6324
diff changeset
   245
26709
f963ea18a579 replaced token translations by common markup;
wenzelm
parents: 26463
diff changeset
   246
val _ = Output.add_mode htmlN output_width Symbol.encode_raw;
f963ea18a579 replaced token translations by common markup;
wenzelm
parents: 26463
diff changeset
   247
6338
bf0d22535e47 output: some symbol translations;
wenzelm
parents: 6324
diff changeset
   248
end;
bf0d22535e47 output: some symbol translations;
wenzelm
parents: 6324
diff changeset
   249
6324
3b7111b360b1 HTML markup elements.
wenzelm
parents:
diff changeset
   250
3b7111b360b1 HTML markup elements.
wenzelm
parents:
diff changeset
   251
3b7111b360b1 HTML markup elements.
wenzelm
parents:
diff changeset
   252
(** HTML markup **)
3b7111b360b1 HTML markup elements.
wenzelm
parents:
diff changeset
   253
3b7111b360b1 HTML markup elements.
wenzelm
parents:
diff changeset
   254
type text = string;
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
(* atoms *)
3b7111b360b1 HTML markup elements.
wenzelm
parents:
diff changeset
   258
3b7111b360b1 HTML markup elements.
wenzelm
parents:
diff changeset
   259
val plain = output;
19265
cae36e16f3c0 Output.add_mode: keyword component;
wenzelm
parents: 18708
diff changeset
   260
val name = enclose "<span class=\"name\">" "</span>" o output;
cae36e16f3c0 Output.add_mode: keyword component;
wenzelm
parents: 18708
diff changeset
   261
val keyword = enclose "<span class=\"keyword\">" "</span>" o output;
23622
8ce09f692653 simplified pretty token metric: type int;
wenzelm
parents: 22796
diff changeset
   262
val command = enclose "<span class=\"command\">" "</span>" o output;
19265
cae36e16f3c0 Output.add_mode: keyword component;
wenzelm
parents: 18708
diff changeset
   263
val file_name = enclose "<span class=\"filename\">" "</span>" o output;
21858
05f57309170c avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents: 20742
diff changeset
   264
val file_path = file_name o Url.implode;
6324
3b7111b360b1 HTML markup elements.
wenzelm
parents:
diff changeset
   265
3b7111b360b1 HTML markup elements.
wenzelm
parents:
diff changeset
   266
3b7111b360b1 HTML markup elements.
wenzelm
parents:
diff changeset
   267
(* misc *)
3b7111b360b1 HTML markup elements.
wenzelm
parents:
diff changeset
   268
28840
wenzelm
parents: 27896
diff changeset
   269
fun href_name s txt = "<a href=" ^ quote s ^ ">" ^ txt ^ "</a>";
21858
05f57309170c avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents: 20742
diff changeset
   270
fun href_path path txt = href_name (Url.implode path) txt;
6376
wenzelm
parents: 6361
diff changeset
   271
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15336
diff changeset
   272
fun href_opt_path NONE txt = txt
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15336
diff changeset
   273
  | href_opt_path (SOME p) txt = href_path p txt;
6376
wenzelm
parents: 6361
diff changeset
   274
12413
f879fcc9412d tuned line breaks in HTML source;
wenzelm
parents: 12151
diff changeset
   275
fun para txt = "\n<p>" ^ txt ^ "</p>\n";
27830
68de2a2780b3 <pre>: removed xml:space, is already default;
wenzelm
parents: 27829
diff changeset
   276
fun preform txt = "<pre>" ^ txt ^ "</pre>";
6324
3b7111b360b1 HTML markup elements.
wenzelm
parents:
diff changeset
   277
val verbatim = preform o output;
3b7111b360b1 HTML markup elements.
wenzelm
parents:
diff changeset
   278
3b7111b360b1 HTML markup elements.
wenzelm
parents:
diff changeset
   279
3b7111b360b1 HTML markup elements.
wenzelm
parents:
diff changeset
   280
(* document *)
3b7111b360b1 HTML markup elements.
wenzelm
parents:
diff changeset
   281
3b7111b360b1 HTML markup elements.
wenzelm
parents:
diff changeset
   282
fun begin_document title =
40946
3f697c636fa1 eliminated fragile HTML.with_charset -- always use utf-8;
wenzelm
parents: 39616
diff changeset
   283
  "<?xml version=\"1.0\" encoding=\"utf-8\" ?>\n\
3f697c636fa1 eliminated fragile HTML.with_charset -- always use utf-8;
wenzelm
parents: 39616
diff changeset
   284
  \<!DOCTYPE html PUBLIC \"-//W3C//DTD XHTML 1.0 Transitional//EN\" \
3f697c636fa1 eliminated fragile HTML.with_charset -- always use utf-8;
wenzelm
parents: 39616
diff changeset
   285
  \\"http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd\">\n\
3f697c636fa1 eliminated fragile HTML.with_charset -- always use utf-8;
wenzelm
parents: 39616
diff changeset
   286
  \<html xmlns=\"http://www.w3.org/1999/xhtml\">\n\
3f697c636fa1 eliminated fragile HTML.with_charset -- always use utf-8;
wenzelm
parents: 39616
diff changeset
   287
  \<head>\n\
3f697c636fa1 eliminated fragile HTML.with_charset -- always use utf-8;
wenzelm
parents: 39616
diff changeset
   288
  \<meta http-equiv=\"Content-Type\" content=\"text/html; charset=utf-8\"/>\n\
3f697c636fa1 eliminated fragile HTML.with_charset -- always use utf-8;
wenzelm
parents: 39616
diff changeset
   289
  \<title>" ^ plain (title ^ " (" ^ Distribution.version ^ ")") ^ "</title>\n\
3f697c636fa1 eliminated fragile HTML.with_charset -- always use utf-8;
wenzelm
parents: 39616
diff changeset
   290
  \<link media=\"all\" rel=\"stylesheet\" type=\"text/css\" href=\"isabelle.css\"/>\n\
3f697c636fa1 eliminated fragile HTML.with_charset -- always use utf-8;
wenzelm
parents: 39616
diff changeset
   291
  \</head>\n\
3f697c636fa1 eliminated fragile HTML.with_charset -- always use utf-8;
wenzelm
parents: 39616
diff changeset
   292
  \\n\
3f697c636fa1 eliminated fragile HTML.with_charset -- always use utf-8;
wenzelm
parents: 39616
diff changeset
   293
  \<body>\n\
3f697c636fa1 eliminated fragile HTML.with_charset -- always use utf-8;
wenzelm
parents: 39616
diff changeset
   294
  \<div class=\"head\">\
3f697c636fa1 eliminated fragile HTML.with_charset -- always use utf-8;
wenzelm
parents: 39616
diff changeset
   295
  \<h1>" ^ plain title ^ "</h1>\n";
6324
3b7111b360b1 HTML markup elements.
wenzelm
parents:
diff changeset
   296
14541
0a7743e2f8dd use css
kleing
parents: 14534
diff changeset
   297
val end_document = "\n</div>\n</body>\n</html>\n";
6324
3b7111b360b1 HTML markup elements.
wenzelm
parents:
diff changeset
   298
6754
c23c542a32e5 tuned markup;
wenzelm
parents: 6649
diff changeset
   299
fun gen_link how (path, name) = para (href_path path how ^ " to index of " ^ plain name);
c23c542a32e5 tuned markup;
wenzelm
parents: 6649
diff changeset
   300
val up_link = gen_link "Up";
c23c542a32e5 tuned markup;
wenzelm
parents: 6649
diff changeset
   301
val back_link = gen_link "Back";
6338
bf0d22535e47 output: some symbol translations;
wenzelm
parents: 6324
diff changeset
   302
bf0d22535e47 output: some symbol translations;
wenzelm
parents: 6324
diff changeset
   303
bf0d22535e47 output: some symbol translations;
wenzelm
parents: 6324
diff changeset
   304
(* session index *)
bf0d22535e47 output: some symbol translations;
wenzelm
parents: 6324
diff changeset
   305
17080
c0c213a8f39c begin_index: list of docs;
wenzelm
parents: 16267
diff changeset
   306
fun begin_index up (index_path, session) docs graph =
6754
c23c542a32e5 tuned markup;
wenzelm
parents: 6649
diff changeset
   307
  begin_document ("Index of " ^ session) ^ up_link up ^
c23c542a32e5 tuned markup;
wenzelm
parents: 6649
diff changeset
   308
  para ("View " ^ href_path graph "theory dependencies" ^
27829
c073006e0137 produce XHTML 1.0 Transitional;
wenzelm
parents: 27490
diff changeset
   309
    implode (map (fn (p, name) => "<br/>\nView " ^ href_path p name) docs)) ^
37941
1d812ff95a14 refrain from generating <hr/> and from "hiding" it in isabelle.css -- the latter might be used in other situations as well;
wenzelm
parents: 37940
diff changeset
   310
  "\n</div>\n<div class=\"theories\">\n<h2>Theories</h2>\n<ul>\n";
6338
bf0d22535e47 output: some symbol translations;
wenzelm
parents: 6324
diff changeset
   311
6649
2156012be986 Reimplemented graph generator.
berghofe
parents: 6405
diff changeset
   312
fun choice chs s = space_implode " " (map (fn (s', lnk) =>
2156012be986 Reimplemented graph generator.
berghofe
parents: 6405
diff changeset
   313
  enclose "[" "]" (if s = s' then keyword s' else href_name lnk s')) chs);
2156012be986 Reimplemented graph generator.
berghofe
parents: 6405
diff changeset
   314
9415
daa2296f23ea removed all_sessions;
wenzelm
parents: 9045
diff changeset
   315
fun applet_pages session back =
6649
2156012be986 Reimplemented graph generator.
berghofe
parents: 6405
diff changeset
   316
  let
9415
daa2296f23ea removed all_sessions;
wenzelm
parents: 9045
diff changeset
   317
    val sizes =
daa2296f23ea removed all_sessions;
wenzelm
parents: 9045
diff changeset
   318
     [("small", "small.html", ("500", "400")),
daa2296f23ea removed all_sessions;
wenzelm
parents: 9045
diff changeset
   319
      ("medium", "medium.html", ("650", "520")),
daa2296f23ea removed all_sessions;
wenzelm
parents: 9045
diff changeset
   320
      ("large", "large.html", ("800", "640"))];
6649
2156012be986 Reimplemented graph generator.
berghofe
parents: 6405
diff changeset
   321
9415
daa2296f23ea removed all_sessions;
wenzelm
parents: 9045
diff changeset
   322
    fun applet_page (size, name, (width, height)) =
6754
c23c542a32e5 tuned markup;
wenzelm
parents: 6649
diff changeset
   323
      let
c23c542a32e5 tuned markup;
wenzelm
parents: 6649
diff changeset
   324
        val browser_size = "Set browser size: " ^
9415
daa2296f23ea removed all_sessions;
wenzelm
parents: 9045
diff changeset
   325
          choice (map (fn (y, z, _) => (y, z)) sizes) size;
6754
c23c542a32e5 tuned markup;
wenzelm
parents: 6649
diff changeset
   326
      in
c23c542a32e5 tuned markup;
wenzelm
parents: 6649
diff changeset
   327
        (name, begin_document ("Theory dependencies of " ^ session) ^
c23c542a32e5 tuned markup;
wenzelm
parents: 6649
diff changeset
   328
          back_link back ^
9415
daa2296f23ea removed all_sessions;
wenzelm
parents: 9045
diff changeset
   329
          para browser_size ^
37941
1d812ff95a14 refrain from generating <hr/> and from "hiding" it in isabelle.css -- the latter might be used in other situations as well;
wenzelm
parents: 37940
diff changeset
   330
          "\n</div>\n<div class=\"graphbrowser\">\n\
17080
c0c213a8f39c begin_index: list of docs;
wenzelm
parents: 16267
diff changeset
   331
          \<applet code=\"GraphBrowser/GraphBrowser.class\" \
14541
0a7743e2f8dd use css
kleing
parents: 14534
diff changeset
   332
          \archive=\"GraphBrowser.jar\" \
27832
992c6d984925 <applet>: more XHTML 1.0 Transitional conformance;
wenzelm
parents: 27830
diff changeset
   333
          \width=" ^ quote width ^ " height=" ^ quote height ^ ">\n\
992c6d984925 <applet>: more XHTML 1.0 Transitional conformance;
wenzelm
parents: 27830
diff changeset
   334
          \<param name=\"graphfile\" value=\"" ^ "session.graph" ^ "\"/>\n\
37941
1d812ff95a14 refrain from generating <hr/> and from "hiding" it in isabelle.css -- the latter might be used in other situations as well;
wenzelm
parents: 37940
diff changeset
   335
          \</applet>" ^ end_document)
6649
2156012be986 Reimplemented graph generator.
berghofe
parents: 6405
diff changeset
   336
      end;
9415
daa2296f23ea removed all_sessions;
wenzelm
parents: 9045
diff changeset
   337
  in map applet_page sizes end;
6649
2156012be986 Reimplemented graph generator.
berghofe
parents: 6405
diff changeset
   338
2156012be986 Reimplemented graph generator.
berghofe
parents: 6405
diff changeset
   339
27829
c073006e0137 produce XHTML 1.0 Transitional;
wenzelm
parents: 27490
diff changeset
   340
fun entry (p, s) = "<li>" ^ href_path p (plain s) ^ "</li>\n";
6405
wenzelm
parents: 6376
diff changeset
   341
6338
bf0d22535e47 output: some symbol translations;
wenzelm
parents: 6324
diff changeset
   342
val theory_entry = entry;
bf0d22535e47 output: some symbol translations;
wenzelm
parents: 6324
diff changeset
   343
6405
wenzelm
parents: 6376
diff changeset
   344
fun session_entries [] = "</ul>"
wenzelm
parents: 6376
diff changeset
   345
  | session_entries es =
37941
1d812ff95a14 refrain from generating <hr/> and from "hiding" it in isabelle.css -- the latter might be used in other situations as well;
wenzelm
parents: 37940
diff changeset
   346
      "</ul>\n</div>\n<div class=\"sessions\">\n\
17080
c0c213a8f39c begin_index: list of docs;
wenzelm
parents: 16267
diff changeset
   347
      \<h2>Sessions</h2>\n<ul>\n" ^ implode (map entry es) ^ "</ul>";
6324
3b7111b360b1 HTML markup elements.
wenzelm
parents:
diff changeset
   348
3b7111b360b1 HTML markup elements.
wenzelm
parents:
diff changeset
   349
3b7111b360b1 HTML markup elements.
wenzelm
parents:
diff changeset
   350
(* theory *)
3b7111b360b1 HTML markup elements.
wenzelm
parents:
diff changeset
   351
27861
911bf8e58c4c removed obsolete verbatim_source, results, chapter, section etc.;
wenzelm
parents: 27832
diff changeset
   352
val theory_source = enclose
37941
1d812ff95a14 refrain from generating <hr/> and from "hiding" it in isabelle.css -- the latter might be used in other situations as well;
wenzelm
parents: 37940
diff changeset
   353
  "\n</div>\n<div class=\"source\">\n<pre>"
1d812ff95a14 refrain from generating <hr/> and from "hiding" it in isabelle.css -- the latter might be used in other situations as well;
wenzelm
parents: 37940
diff changeset
   354
  "</pre>\n";
6324
3b7111b360b1 HTML markup elements.
wenzelm
parents:
diff changeset
   355
3b7111b360b1 HTML markup elements.
wenzelm
parents:
diff changeset
   356
3b7111b360b1 HTML markup elements.
wenzelm
parents:
diff changeset
   357
local
27490
ac1d6e87aa52 removed unused href_opt_name;
wenzelm
parents: 26709
diff changeset
   358
  fun file (href, path, loadit) =
ac1d6e87aa52 removed unused href_opt_name;
wenzelm
parents: 26709
diff changeset
   359
    href_path href (if loadit then file_path path else enclose "(" ")" (file_path path));
6361
3a45ad4a95eb theory: include parent links;
wenzelm
parents: 6347
diff changeset
   360
6376
wenzelm
parents: 6361
diff changeset
   361
  fun theory up A =
wenzelm
parents: 6361
diff changeset
   362
    begin_document ("Theory " ^ A) ^ "\n" ^ up_link up ^
23622
8ce09f692653 simplified pretty token metric: type int;
wenzelm
parents: 22796
diff changeset
   363
    command "theory" ^ " " ^ name A;
16267
0773b17922d8 present new-style theory header, with 'imports' and 'uses';
wenzelm
parents: 16196
diff changeset
   364
0773b17922d8 present new-style theory header, with 'imports' and 'uses';
wenzelm
parents: 16196
diff changeset
   365
  fun imports Bs =
0773b17922d8 present new-style theory header, with 'imports' and 'uses';
wenzelm
parents: 16196
diff changeset
   366
    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
   367
27829
c073006e0137 produce XHTML 1.0 Transitional;
wenzelm
parents: 27490
diff changeset
   368
  fun uses Ps = keyword "uses" ^ " " ^ space_implode " " (map file Ps) ^ "<br/>\n";
6324
3b7111b360b1 HTML markup elements.
wenzelm
parents:
diff changeset
   369
in
3b7111b360b1 HTML markup elements.
wenzelm
parents:
diff changeset
   370
16267
0773b17922d8 present new-style theory header, with 'imports' and 'uses';
wenzelm
parents: 16196
diff changeset
   371
fun begin_theory up A Bs Ps body =
27829
c073006e0137 produce XHTML 1.0 Transitional;
wenzelm
parents: 27490
diff changeset
   372
  theory up A ^ "<br/>\n" ^
c073006e0137 produce XHTML 1.0 Transitional;
wenzelm
parents: 27490
diff changeset
   373
  imports Bs ^ "<br/>\n" ^
16267
0773b17922d8 present new-style theory header, with 'imports' and 'uses';
wenzelm
parents: 16196
diff changeset
   374
  (if null Ps then "" else uses Ps) ^
0773b17922d8 present new-style theory header, with 'imports' and 'uses';
wenzelm
parents: 16196
diff changeset
   375
  body;
0773b17922d8 present new-style theory header, with 'imports' and 'uses';
wenzelm
parents: 16196
diff changeset
   376
6324
3b7111b360b1 HTML markup elements.
wenzelm
parents:
diff changeset
   377
end;
3b7111b360b1 HTML markup elements.
wenzelm
parents:
diff changeset
   378
3b7111b360b1 HTML markup elements.
wenzelm
parents:
diff changeset
   379
37940
4857eab31298 generic external source files -- nothing special about ML here;
wenzelm
parents: 37146
diff changeset
   380
(* external file *)
6324
3b7111b360b1 HTML markup elements.
wenzelm
parents:
diff changeset
   381
37940
4857eab31298 generic external source files -- nothing special about ML here;
wenzelm
parents: 37146
diff changeset
   382
fun external_file path str =
21858
05f57309170c avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents: 20742
diff changeset
   383
  begin_document ("File " ^ Url.implode path) ^
37941
1d812ff95a14 refrain from generating <hr/> and from "hiding" it in isabelle.css -- the latter might be used in other situations as well;
wenzelm
parents: 37940
diff changeset
   384
  "\n</div><div class=\"external_source\">\n" ^
14571
b88d5f9e02e1 fixed width;
wenzelm
parents: 14565
diff changeset
   385
  verbatim str ^
37941
1d812ff95a14 refrain from generating <hr/> and from "hiding" it in isabelle.css -- the latter might be used in other situations as well;
wenzelm
parents: 37940
diff changeset
   386
  "\n</div>\n<div class=\"external_footer\">" ^
14541
0a7743e2f8dd use css
kleing
parents: 14534
diff changeset
   387
  end_document;
6324
3b7111b360b1 HTML markup elements.
wenzelm
parents:
diff changeset
   388
7572
6e6dafacbc28 present results;
wenzelm
parents: 7408
diff changeset
   389
end;