src/Pure/Thy/html.ML
author wenzelm
Thu Nov 02 10:16:22 2017 +0100 (20 months ago)
changeset 66987 352b23c97ac8
parent 66044 bd7516709051
child 67306 897344e33c26
permissions -rw-r--r--
support focus_session, for much faster startup of Isabelle/jEdit;
more options for "isabelle jedit";
     1 (*  Title:      Pure/Thy/html.ML
     2     Author:     Markus Wenzel and Stefan Berghofer, TU Muenchen
     3 
     4 HTML presentation elements.
     5 *)
     6 
     7 signature HTML =
     8 sig
     9   type symbols
    10   val make_symbols: (string * int) list -> symbols
    11   val no_symbols: symbols
    12   val present_span: symbols -> Keyword.keywords -> Command_Span.span -> Output.output
    13   type text = string
    14   val begin_document: symbols -> string -> text
    15   val end_document: text
    16   val begin_session_index: symbols -> string -> Url.T -> (Url.T * string) list -> text
    17   val theory_entry: symbols -> Url.T * string -> text
    18   val theory: symbols -> string -> (Url.T option * string) list -> text -> text
    19 end;
    20 
    21 structure HTML: HTML =
    22 struct
    23 
    24 
    25 (* common markup *)
    26 
    27 fun span class = ("<span class=" ^ quote (XML.text class) ^ ">", "</span>");
    28 val enclose_span = uncurry enclose o span;
    29 
    30 val hidden = enclose_span Markup.hiddenN;
    31 
    32 
    33 (* symbol output *)
    34 
    35 abstype symbols = Symbols of string Symtab.table
    36 with
    37 
    38 fun make_symbols codes =
    39   let
    40     val mapping =
    41       map (apsnd (fn c => "&#" ^ Value.print_int c ^ ";")) codes @
    42        [("'", "&#39;"),
    43         ("\<^bsub>", hidden "&#8664;" ^ "<sub>"),
    44         ("\<^esub>", hidden "&#8665;" ^ "</sub>"),
    45         ("\<^bsup>", hidden "&#8663;" ^ "<sup>"),
    46         ("\<^esup>", hidden "&#8662;" ^ "</sup>")];
    47   in Symbols (fold Symtab.update mapping Symtab.empty) end;
    48 
    49 val no_symbols = make_symbols [];
    50 
    51 fun output_sym (Symbols tab) s =
    52   (case Symtab.lookup tab s of
    53     SOME x => x
    54   | NONE => XML.text s);
    55 
    56 end;
    57 
    58 local
    59 
    60 fun output_markup (bg, en) symbols s1 s2 =
    61   hidden s1 ^ enclose bg en (output_sym symbols s2);
    62 
    63 val output_sub = output_markup ("<sub>", "</sub>");
    64 val output_sup = output_markup ("<sup>", "</sup>");
    65 val output_bold = output_markup (span "bold");
    66 
    67 fun output_syms _ [] result = implode (rev result)
    68   | output_syms symbols (s1 :: rest) result =
    69       let
    70         val (s2, ss) = (case rest of [] => ("", []) | s2 :: ss => (s2, ss));
    71         val (s, r) =
    72           if s1 = "\<^sub>" then (output_sub symbols "&#8681;" s2, ss)
    73           else if s1 = "\<^sup>" then (output_sup symbols "&#8679;" s2, ss)
    74           else if s1 = "\<^bold>" then (output_bold symbols "&#10073;" s2, ss)
    75           else (output_sym symbols s1, rest);
    76       in output_syms symbols r (s :: result) end;
    77 
    78 in
    79 
    80 fun output symbols str = output_syms symbols (Symbol.explode str) [];
    81 
    82 end;
    83 
    84 
    85 (* presentation *)
    86 
    87 fun present_span symbols keywords =
    88   let
    89     fun present_markup (name, props) =
    90       (case Properties.get props Markup.kindN of
    91         SOME kind =>
    92           if kind = Markup.commandN orelse kind = Markup.keywordN then enclose_span kind else I
    93       | NONE => I) #> enclose_span name;
    94     fun present_token tok =
    95       fold_rev present_markup (Token.markups keywords tok)
    96         (output symbols (Token.unparse tok));
    97   in implode o map present_token o Command_Span.content end;
    98 
    99 
   100 
   101 (** HTML markup **)
   102 
   103 type text = string;
   104 
   105 
   106 (* atoms *)
   107 
   108 val name = enclose "<span class=\"name\">" "</span>" oo output;
   109 val keyword = enclose "<span class=\"keyword\">" "</span>" oo output;
   110 val command = enclose "<span class=\"command\">" "</span>" oo output;
   111 
   112 
   113 (* misc *)
   114 
   115 fun href_name s txt = "<a href=" ^ quote s ^ ">" ^ txt ^ "</a>";
   116 fun href_path path txt = href_name (Url.implode path) txt;
   117 
   118 fun href_opt_path NONE txt = txt
   119   | href_opt_path (SOME p) txt = href_path p txt;
   120 
   121 fun para txt = "\n<p>" ^ txt ^ "</p>\n";
   122 
   123 
   124 (* document *)
   125 
   126 fun begin_document symbols title =
   127   "<?xml version=\"1.0\" encoding=\"utf-8\" ?>\n" ^
   128   "<!DOCTYPE html PUBLIC \"-//W3C//DTD XHTML 1.0 Transitional//EN\" " ^
   129   "\"http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd\">\n" ^
   130   "<html xmlns=\"http://www.w3.org/1999/xhtml\">\n" ^
   131   "<head>\n" ^
   132   "<meta http-equiv=\"Content-Type\" content=\"text/html; charset=utf-8\"/>\n" ^
   133   "<title>" ^ output symbols (title ^ " (" ^ Distribution.version ^ ")") ^ "</title>\n" ^
   134   "<link media=\"all\" rel=\"stylesheet\" type=\"text/css\" href=\"isabelle.css\"/>\n" ^
   135   "</head>\n" ^
   136   "\n" ^
   137   "<body>\n" ^
   138   "<div class=\"head\">" ^
   139   "<h1>" ^ output symbols title ^ "</h1>\n";
   140 
   141 val end_document = "\n</div>\n</body>\n</html>\n";
   142 
   143 
   144 (* session index *)
   145 
   146 fun begin_session_index symbols session graph docs =
   147   begin_document symbols ("Session " ^ output symbols session) ^
   148   para ("View " ^ href_path graph "theory dependencies" ^
   149     implode (map (fn (p, name) => "<br/>\nView " ^ href_path p name) docs)) ^
   150   "\n</div>\n<div class=\"theories\">\n<h2>Theories</h2>\n<ul>\n";
   151 
   152 fun theory_entry symbols (p, s) = "<li>" ^ href_path p (output symbols s) ^ "</li>\n";
   153 
   154 
   155 (* theory *)
   156 
   157 fun theory symbols A Bs txt =
   158   begin_document symbols ("Theory " ^ A) ^ "\n" ^
   159   command symbols "theory" ^ " " ^ name symbols A ^ "<br/>\n" ^
   160   keyword symbols "imports" ^ " " ^
   161     space_implode " " (map (uncurry href_opt_path o apsnd (name symbols)) Bs) ^
   162   "<br/>\n" ^
   163   enclose "\n</div>\n<div class=\"source\">\n<pre class=\"source\">" "</pre>\n" txt ^
   164   end_document;
   165 
   166 end;