src/Pure/Thy/html.ML
author wenzelm
Mon, 16 Nov 2020 22:23:04 +0100
changeset 72622 830222403681
parent 69804 9efccbad7d42
child 72636 09ee9eb7a3d3
permissions -rw-r--r--
HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
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
72622
830222403681 HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents: 69804
diff changeset
     2
    Author:     Makarius
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
61381
ddca85598c65 more explicit HTML.symbols;
wenzelm
parents: 61379
diff changeset
     9
  type symbols
ddca85598c65 more explicit HTML.symbols;
wenzelm
parents: 61379
diff changeset
    10
  val make_symbols: (string * int) list -> symbols
ddca85598c65 more explicit HTML.symbols;
wenzelm
parents: 61379
diff changeset
    11
  val no_symbols: symbols
ddca85598c65 more explicit HTML.symbols;
wenzelm
parents: 61379
diff changeset
    12
  val present_span: symbols -> Keyword.keywords -> Command_Span.span -> Output.output
23622
8ce09f692653 simplified pretty token metric: type int;
wenzelm
parents: 22796
diff changeset
    13
  type text = string
72622
830222403681 HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents: 69804
diff changeset
    14
  val name: symbols -> string -> text
830222403681 HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents: 69804
diff changeset
    15
  val keyword: symbols -> string -> text
830222403681 HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents: 69804
diff changeset
    16
  val command: symbols -> string -> text
830222403681 HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents: 69804
diff changeset
    17
  val href_name: string -> string -> string
830222403681 HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents: 69804
diff changeset
    18
  val href_path: Url.T -> string -> string
830222403681 HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents: 69804
diff changeset
    19
  val href_opt_path: Url.T option -> string -> string
61381
ddca85598c65 more explicit HTML.symbols;
wenzelm
parents: 61379
diff changeset
    20
  val begin_document: symbols -> string -> text
23724
6e95ed5f64da export html_mode, begin_document, end_document;
wenzelm
parents: 23703
diff changeset
    21
  val end_document: text
6324
3b7111b360b1 HTML markup elements.
wenzelm
parents:
diff changeset
    22
end;
3b7111b360b1 HTML markup elements.
wenzelm
parents:
diff changeset
    23
3b7111b360b1 HTML markup elements.
wenzelm
parents:
diff changeset
    24
structure HTML: HTML =
3b7111b360b1 HTML markup elements.
wenzelm
parents:
diff changeset
    25
struct
3b7111b360b1 HTML markup elements.
wenzelm
parents:
diff changeset
    26
3b7111b360b1 HTML markup elements.
wenzelm
parents:
diff changeset
    27
33985
1d33e85a3fa9 added markup for hidden text;
wenzelm
parents: 33983
diff changeset
    28
(* common markup *)
1d33e85a3fa9 added markup for hidden text;
wenzelm
parents: 33983
diff changeset
    29
67306
897344e33c26 less redundant;
wenzelm
parents: 66044
diff changeset
    30
fun span "" = ("<span>", "</span>")
897344e33c26 less redundant;
wenzelm
parents: 66044
diff changeset
    31
  | span class = ("<span class=" ^ quote (XML.text class) ^ ">", "</span>");
897344e33c26 less redundant;
wenzelm
parents: 66044
diff changeset
    32
66044
bd7516709051 more HTML rendering as in Isabelle/jEdit;
wenzelm
parents: 63934
diff changeset
    33
val enclose_span = uncurry enclose o span;
33985
1d33e85a3fa9 added markup for hidden text;
wenzelm
parents: 33983
diff changeset
    34
66044
bd7516709051 more HTML rendering as in Isabelle/jEdit;
wenzelm
parents: 63934
diff changeset
    35
val hidden = enclose_span Markup.hiddenN;
33985
1d33e85a3fa9 added markup for hidden text;
wenzelm
parents: 33983
diff changeset
    36
1d33e85a3fa9 added markup for hidden text;
wenzelm
parents: 33983
diff changeset
    37
6324
3b7111b360b1 HTML markup elements.
wenzelm
parents:
diff changeset
    38
(* symbol output *)
3b7111b360b1 HTML markup elements.
wenzelm
parents:
diff changeset
    39
61381
ddca85598c65 more explicit HTML.symbols;
wenzelm
parents: 61379
diff changeset
    40
abstype symbols = Symbols of string Symtab.table
ddca85598c65 more explicit HTML.symbols;
wenzelm
parents: 61379
diff changeset
    41
with
ddca85598c65 more explicit HTML.symbols;
wenzelm
parents: 61379
diff changeset
    42
ddca85598c65 more explicit HTML.symbols;
wenzelm
parents: 61379
diff changeset
    43
fun make_symbols codes =
ddca85598c65 more explicit HTML.symbols;
wenzelm
parents: 61379
diff changeset
    44
  let
ddca85598c65 more explicit HTML.symbols;
wenzelm
parents: 61379
diff changeset
    45
    val mapping =
63806
c54a53ef1873 clarified modules;
wenzelm
parents: 62529
diff changeset
    46
      map (apsnd (fn c => "&#" ^ Value.print_int c ^ ";")) codes @
61381
ddca85598c65 more explicit HTML.symbols;
wenzelm
parents: 61379
diff changeset
    47
       [("'", "&#39;"),
62529
8b7bdfc09f3b clarified treatment of fragments of Isabelle symbols during bootstrap;
wenzelm
parents: 61381
diff changeset
    48
        ("\<^bsub>", hidden "&#8664;" ^ "<sub>"),
8b7bdfc09f3b clarified treatment of fragments of Isabelle symbols during bootstrap;
wenzelm
parents: 61381
diff changeset
    49
        ("\<^esub>", hidden "&#8665;" ^ "</sub>"),
8b7bdfc09f3b clarified treatment of fragments of Isabelle symbols during bootstrap;
wenzelm
parents: 61381
diff changeset
    50
        ("\<^bsup>", hidden "&#8663;" ^ "<sup>"),
8b7bdfc09f3b clarified treatment of fragments of Isabelle symbols during bootstrap;
wenzelm
parents: 61381
diff changeset
    51
        ("\<^esup>", hidden "&#8662;" ^ "</sup>")];
61381
ddca85598c65 more explicit HTML.symbols;
wenzelm
parents: 61379
diff changeset
    52
  in Symbols (fold Symtab.update mapping Symtab.empty) end;
ddca85598c65 more explicit HTML.symbols;
wenzelm
parents: 61379
diff changeset
    53
ddca85598c65 more explicit HTML.symbols;
wenzelm
parents: 61379
diff changeset
    54
val no_symbols = make_symbols [];
ddca85598c65 more explicit HTML.symbols;
wenzelm
parents: 61379
diff changeset
    55
ddca85598c65 more explicit HTML.symbols;
wenzelm
parents: 61379
diff changeset
    56
fun output_sym (Symbols tab) s =
63934
397b25cee74c \<^raw> output is intended for LaTeX;
wenzelm
parents: 63806
diff changeset
    57
  (case Symtab.lookup tab s of
397b25cee74c \<^raw> output is intended for LaTeX;
wenzelm
parents: 63806
diff changeset
    58
    SOME x => x
397b25cee74c \<^raw> output is intended for LaTeX;
wenzelm
parents: 63806
diff changeset
    59
  | NONE => XML.text s);
61381
ddca85598c65 more explicit HTML.symbols;
wenzelm
parents: 61379
diff changeset
    60
ddca85598c65 more explicit HTML.symbols;
wenzelm
parents: 61379
diff changeset
    61
end;
ddca85598c65 more explicit HTML.symbols;
wenzelm
parents: 61379
diff changeset
    62
6338
bf0d22535e47 output: some symbol translations;
wenzelm
parents: 6324
diff changeset
    63
local
61376
93224745477f output HTML text according to Isabelle/Scala Symbol.Interpretation;
wenzelm
parents: 61374
diff changeset
    64
61381
ddca85598c65 more explicit HTML.symbols;
wenzelm
parents: 61379
diff changeset
    65
fun output_markup (bg, en) symbols s1 s2 =
ddca85598c65 more explicit HTML.symbols;
wenzelm
parents: 61379
diff changeset
    66
  hidden s1 ^ enclose bg en (output_sym symbols s2);
61376
93224745477f output HTML text according to Isabelle/Scala Symbol.Interpretation;
wenzelm
parents: 61374
diff changeset
    67
93224745477f output HTML text according to Isabelle/Scala Symbol.Interpretation;
wenzelm
parents: 61374
diff changeset
    68
val output_sub = output_markup ("<sub>", "</sub>");
93224745477f output HTML text according to Isabelle/Scala Symbol.Interpretation;
wenzelm
parents: 61374
diff changeset
    69
val output_sup = output_markup ("<sup>", "</sup>");
93224745477f output HTML text according to Isabelle/Scala Symbol.Interpretation;
wenzelm
parents: 61374
diff changeset
    70
val output_bold = output_markup (span "bold");
17178
18a98ecc6821 output \<^loc> as 'loc' span;
wenzelm
parents: 17116
diff changeset
    71
61381
ddca85598c65 more explicit HTML.symbols;
wenzelm
parents: 61379
diff changeset
    72
fun output_syms _ [] result = implode (rev result)
ddca85598c65 more explicit HTML.symbols;
wenzelm
parents: 61379
diff changeset
    73
  | output_syms symbols (s1 :: rest) result =
61376
93224745477f output HTML text according to Isabelle/Scala Symbol.Interpretation;
wenzelm
parents: 61374
diff changeset
    74
      let
93224745477f output HTML text according to Isabelle/Scala Symbol.Interpretation;
wenzelm
parents: 61374
diff changeset
    75
        val (s2, ss) = (case rest of [] => ("", []) | s2 :: ss => (s2, ss));
61381
ddca85598c65 more explicit HTML.symbols;
wenzelm
parents: 61379
diff changeset
    76
        val (s, r) =
62529
8b7bdfc09f3b clarified treatment of fragments of Isabelle symbols during bootstrap;
wenzelm
parents: 61381
diff changeset
    77
          if s1 = "\<^sub>" then (output_sub symbols "&#8681;" s2, ss)
8b7bdfc09f3b clarified treatment of fragments of Isabelle symbols during bootstrap;
wenzelm
parents: 61381
diff changeset
    78
          else if s1 = "\<^sup>" then (output_sup symbols "&#8679;" s2, ss)
8b7bdfc09f3b clarified treatment of fragments of Isabelle symbols during bootstrap;
wenzelm
parents: 61381
diff changeset
    79
          else if s1 = "\<^bold>" then (output_bold symbols "&#10073;" s2, ss)
61381
ddca85598c65 more explicit HTML.symbols;
wenzelm
parents: 61379
diff changeset
    80
          else (output_sym symbols s1, rest);
ddca85598c65 more explicit HTML.symbols;
wenzelm
parents: 61379
diff changeset
    81
      in output_syms symbols r (s :: result) end;
14534
7a46bdcd92f2 treat sub/super scripts
kleing
parents: 14083
diff changeset
    82
6338
bf0d22535e47 output: some symbol translations;
wenzelm
parents: 6324
diff changeset
    83
in
6324
3b7111b360b1 HTML markup elements.
wenzelm
parents:
diff changeset
    84
61381
ddca85598c65 more explicit HTML.symbols;
wenzelm
parents: 61379
diff changeset
    85
fun output symbols str = output_syms symbols (Symbol.explode str) [];
61376
93224745477f output HTML text according to Isabelle/Scala Symbol.Interpretation;
wenzelm
parents: 61374
diff changeset
    86
6338
bf0d22535e47 output: some symbol translations;
wenzelm
parents: 6324
diff changeset
    87
end;
bf0d22535e47 output: some symbol translations;
wenzelm
parents: 6324
diff changeset
    88
6324
3b7111b360b1 HTML markup elements.
wenzelm
parents:
diff changeset
    89
61379
c57820ceead3 more direct HTML presentation, without print mode;
wenzelm
parents: 61376
diff changeset
    90
(* presentation *)
c57820ceead3 more direct HTML presentation, without print mode;
wenzelm
parents: 61376
diff changeset
    91
61381
ddca85598c65 more explicit HTML.symbols;
wenzelm
parents: 61379
diff changeset
    92
fun present_span symbols keywords =
ddca85598c65 more explicit HTML.symbols;
wenzelm
parents: 61379
diff changeset
    93
  let
66044
bd7516709051 more HTML rendering as in Isabelle/jEdit;
wenzelm
parents: 63934
diff changeset
    94
    fun present_markup (name, props) =
bd7516709051 more HTML rendering as in Isabelle/jEdit;
wenzelm
parents: 63934
diff changeset
    95
      (case Properties.get props Markup.kindN of
bd7516709051 more HTML rendering as in Isabelle/jEdit;
wenzelm
parents: 63934
diff changeset
    96
        SOME kind =>
bd7516709051 more HTML rendering as in Isabelle/jEdit;
wenzelm
parents: 63934
diff changeset
    97
          if kind = Markup.commandN orelse kind = Markup.keywordN then enclose_span kind else I
bd7516709051 more HTML rendering as in Isabelle/jEdit;
wenzelm
parents: 63934
diff changeset
    98
      | NONE => I) #> enclose_span name;
61381
ddca85598c65 more explicit HTML.symbols;
wenzelm
parents: 61379
diff changeset
    99
    fun present_token tok =
66044
bd7516709051 more HTML rendering as in Isabelle/jEdit;
wenzelm
parents: 63934
diff changeset
   100
      fold_rev present_markup (Token.markups keywords tok)
bd7516709051 more HTML rendering as in Isabelle/jEdit;
wenzelm
parents: 63934
diff changeset
   101
        (output symbols (Token.unparse tok));
61381
ddca85598c65 more explicit HTML.symbols;
wenzelm
parents: 61379
diff changeset
   102
  in implode o map present_token o Command_Span.content end;
61379
c57820ceead3 more direct HTML presentation, without print mode;
wenzelm
parents: 61376
diff changeset
   103
c57820ceead3 more direct HTML presentation, without print mode;
wenzelm
parents: 61376
diff changeset
   104
6324
3b7111b360b1 HTML markup elements.
wenzelm
parents:
diff changeset
   105
3b7111b360b1 HTML markup elements.
wenzelm
parents:
diff changeset
   106
(** HTML markup **)
3b7111b360b1 HTML markup elements.
wenzelm
parents:
diff changeset
   107
3b7111b360b1 HTML markup elements.
wenzelm
parents:
diff changeset
   108
type text = string;
3b7111b360b1 HTML markup elements.
wenzelm
parents:
diff changeset
   109
3b7111b360b1 HTML markup elements.
wenzelm
parents:
diff changeset
   110
3b7111b360b1 HTML markup elements.
wenzelm
parents:
diff changeset
   111
(* atoms *)
3b7111b360b1 HTML markup elements.
wenzelm
parents:
diff changeset
   112
61381
ddca85598c65 more explicit HTML.symbols;
wenzelm
parents: 61379
diff changeset
   113
val name = enclose "<span class=\"name\">" "</span>" oo output;
ddca85598c65 more explicit HTML.symbols;
wenzelm
parents: 61379
diff changeset
   114
val keyword = enclose "<span class=\"keyword\">" "</span>" oo output;
ddca85598c65 more explicit HTML.symbols;
wenzelm
parents: 61379
diff changeset
   115
val command = enclose "<span class=\"command\">" "</span>" oo output;
6324
3b7111b360b1 HTML markup elements.
wenzelm
parents:
diff changeset
   116
3b7111b360b1 HTML markup elements.
wenzelm
parents:
diff changeset
   117
3b7111b360b1 HTML markup elements.
wenzelm
parents:
diff changeset
   118
(* misc *)
3b7111b360b1 HTML markup elements.
wenzelm
parents:
diff changeset
   119
28840
wenzelm
parents: 27896
diff changeset
   120
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
   121
fun href_path path txt = href_name (Url.implode path) txt;
6376
wenzelm
parents: 6361
diff changeset
   122
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15336
diff changeset
   123
fun href_opt_path NONE txt = txt
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15336
diff changeset
   124
  | href_opt_path (SOME p) txt = href_path p txt;
6376
wenzelm
parents: 6361
diff changeset
   125
6324
3b7111b360b1 HTML markup elements.
wenzelm
parents:
diff changeset
   126
3b7111b360b1 HTML markup elements.
wenzelm
parents:
diff changeset
   127
(* document *)
3b7111b360b1 HTML markup elements.
wenzelm
parents:
diff changeset
   128
61381
ddca85598c65 more explicit HTML.symbols;
wenzelm
parents: 61379
diff changeset
   129
fun begin_document symbols title =
69804
9efccbad7d42 uniform XML header;
wenzelm
parents: 67306
diff changeset
   130
  XML.header ^
62529
8b7bdfc09f3b clarified treatment of fragments of Isabelle symbols during bootstrap;
wenzelm
parents: 61381
diff changeset
   131
  "<!DOCTYPE html PUBLIC \"-//W3C//DTD XHTML 1.0 Transitional//EN\" " ^
8b7bdfc09f3b clarified treatment of fragments of Isabelle symbols during bootstrap;
wenzelm
parents: 61381
diff changeset
   132
  "\"http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd\">\n" ^
8b7bdfc09f3b clarified treatment of fragments of Isabelle symbols during bootstrap;
wenzelm
parents: 61381
diff changeset
   133
  "<html xmlns=\"http://www.w3.org/1999/xhtml\">\n" ^
8b7bdfc09f3b clarified treatment of fragments of Isabelle symbols during bootstrap;
wenzelm
parents: 61381
diff changeset
   134
  "<head>\n" ^
8b7bdfc09f3b clarified treatment of fragments of Isabelle symbols during bootstrap;
wenzelm
parents: 61381
diff changeset
   135
  "<meta http-equiv=\"Content-Type\" content=\"text/html; charset=utf-8\"/>\n" ^
8b7bdfc09f3b clarified treatment of fragments of Isabelle symbols during bootstrap;
wenzelm
parents: 61381
diff changeset
   136
  "<title>" ^ output symbols (title ^ " (" ^ Distribution.version ^ ")") ^ "</title>\n" ^
8b7bdfc09f3b clarified treatment of fragments of Isabelle symbols during bootstrap;
wenzelm
parents: 61381
diff changeset
   137
  "<link media=\"all\" rel=\"stylesheet\" type=\"text/css\" href=\"isabelle.css\"/>\n" ^
8b7bdfc09f3b clarified treatment of fragments of Isabelle symbols during bootstrap;
wenzelm
parents: 61381
diff changeset
   138
  "</head>\n" ^
8b7bdfc09f3b clarified treatment of fragments of Isabelle symbols during bootstrap;
wenzelm
parents: 61381
diff changeset
   139
  "\n" ^
8b7bdfc09f3b clarified treatment of fragments of Isabelle symbols during bootstrap;
wenzelm
parents: 61381
diff changeset
   140
  "<body>\n" ^
8b7bdfc09f3b clarified treatment of fragments of Isabelle symbols during bootstrap;
wenzelm
parents: 61381
diff changeset
   141
  "<div class=\"head\">" ^
8b7bdfc09f3b clarified treatment of fragments of Isabelle symbols during bootstrap;
wenzelm
parents: 61381
diff changeset
   142
  "<h1>" ^ output symbols title ^ "</h1>\n";
6324
3b7111b360b1 HTML markup elements.
wenzelm
parents:
diff changeset
   143
14541
0a7743e2f8dd use css
kleing
parents: 14534
diff changeset
   144
val end_document = "\n</div>\n</body>\n</html>\n";
6324
3b7111b360b1 HTML markup elements.
wenzelm
parents:
diff changeset
   145
3b7111b360b1 HTML markup elements.
wenzelm
parents:
diff changeset
   146
end;