--- a/src/Pure/Thy/html.ML Fri Nov 20 14:29:21 2020 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,142 +0,0 @@
-(* Title: Pure/Thy/html.ML
- Author: Makarius
-
-HTML presentation elements.
-*)
-
-signature HTML =
-sig
- type symbols
- val make_symbols: (string * int) list -> symbols
- val no_symbols: symbols
- val present_span: symbols -> Keyword.keywords -> Command_Span.span -> Output.output
- type text = string
- val name: symbols -> string -> text
- val keyword: symbols -> string -> text
- val command: symbols -> string -> text
- val href_name: string -> string -> string
- val href_path: Url.T -> string -> string
- val begin_document: symbols -> string -> text
- val end_document: text
-end;
-
-structure HTML: HTML =
-struct
-
-
-(* common markup *)
-
-fun span "" = ("<span>", "</span>")
- | span class = ("<span class=" ^ quote (XML.text class) ^ ">", "</span>");
-
-val enclose_span = uncurry enclose o span;
-
-val hidden = enclose_span Markup.hiddenN;
-
-
-(* symbol output *)
-
-abstype symbols = Symbols of string Symtab.table
-with
-
-fun make_symbols codes =
- let
- val mapping =
- map (apsnd (fn c => "&#" ^ Value.print_int c ^ ";")) codes @
- [("'", "'"),
- ("\<^bsub>", hidden "⇘" ^ "<sub>"),
- ("\<^esub>", hidden "⇙" ^ "</sub>"),
- ("\<^bsup>", hidden "⇗" ^ "<sup>"),
- ("\<^esup>", hidden "⇖" ^ "</sup>")];
- in Symbols (fold Symtab.update mapping Symtab.empty) end;
-
-val no_symbols = make_symbols [];
-
-fun output_sym (Symbols tab) s =
- (case Symtab.lookup tab s of
- SOME x => x
- | NONE => XML.text s);
-
-end;
-
-local
-
-fun output_markup (bg, en) symbols s1 s2 =
- hidden s1 ^ enclose bg en (output_sym symbols s2);
-
-val output_sub = output_markup ("<sub>", "</sub>");
-val output_sup = output_markup ("<sup>", "</sup>");
-val output_bold = output_markup (span "bold");
-
-fun output_syms _ [] result = implode (rev result)
- | output_syms symbols (s1 :: rest) result =
- let
- val (s2, ss) = (case rest of [] => ("", []) | s2 :: ss => (s2, ss));
- val (s, r) =
- if s1 = "\<^sub>" then (output_sub symbols "⇩" s2, ss)
- else if s1 = "\<^sup>" then (output_sup symbols "⇧" s2, ss)
- else if s1 = "\<^bold>" then (output_bold symbols "❙" s2, ss)
- else (output_sym symbols s1, rest);
- in output_syms symbols r (s :: result) end;
-
-in
-
-fun output symbols str = output_syms symbols (Symbol.explode str) [];
-
-end;
-
-
-(* presentation *)
-
-fun present_span symbols keywords =
- let
- fun present_markup (name, props) =
- (case Properties.get props Markup.kindN of
- SOME kind =>
- if kind = Markup.commandN orelse kind = Markup.keywordN then enclose_span kind else I
- | NONE => I) #> enclose_span name;
- fun present_token tok =
- fold_rev present_markup (Token.markups keywords tok)
- (output symbols (Token.unparse tok));
- in implode o map present_token o Command_Span.content end;
-
-
-
-(** HTML markup **)
-
-type text = string;
-
-
-(* atoms *)
-
-val name = enclose "<span class=\"name\">" "</span>" oo output;
-val keyword = enclose "<span class=\"keyword\">" "</span>" oo output;
-val command = enclose "<span class=\"command\">" "</span>" oo output;
-
-
-(* misc *)
-
-fun href_name s txt = "<a href=" ^ quote s ^ ">" ^ txt ^ "</a>";
-fun href_path path txt = href_name (Url.implode path) txt;
-
-
-(* document *)
-
-fun begin_document symbols title =
- XML.header ^
- "<!DOCTYPE html PUBLIC \"-//W3C//DTD XHTML 1.0 Transitional//EN\" " ^
- "\"http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd\">\n" ^
- "<html xmlns=\"http://www.w3.org/1999/xhtml\">\n" ^
- "<head>\n" ^
- "<meta http-equiv=\"Content-Type\" content=\"text/html; charset=utf-8\"/>\n" ^
- "<title>" ^ output symbols (title ^ " (" ^ Distribution.version ^ ")") ^ "</title>\n" ^
- "<link media=\"all\" rel=\"stylesheet\" type=\"text/css\" href=\"isabelle.css\"/>\n" ^
- "</head>\n" ^
- "\n" ^
- "<body>\n" ^
- "<div class=\"head\">" ^
- "<h1>" ^ output symbols title ^ "</h1>\n";
-
-val end_document = "\n</div>\n</body>\n</html>\n";
-
-end;