diff -r b1388cfb64bb -r 5e7916535860 src/Pure/Thy/html.ML
--- 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 class = ("", "");
-
-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 "⇘" ^ ""),
- ("\<^esub>", hidden "⇙" ^ ""),
- ("\<^bsup>", hidden "⇗" ^ ""),
- ("\<^esup>", hidden "⇖" ^ "")];
- 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 ("", "");
-val output_sup = output_markup ("", "");
-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 "" "" oo output;
-val keyword = enclose "" "" oo output;
-val command = enclose "" "" oo output;
-
-
-(* misc *)
-
-fun href_name s txt = "" ^ txt ^ "";
-fun href_path path txt = href_name (Url.implode path) txt;
-
-
-(* document *)
-
-fun begin_document symbols title =
- XML.header ^
- "\n" ^
- "\n" ^
- "\n" ^
- "\n" ^
- "" ^ output symbols (title ^ " (" ^ Distribution.version ^ ")") ^ "\n" ^
- "\n" ^
- "\n" ^
- "\n" ^
- "\n" ^
- "" ^
- "
" ^ output symbols title ^ "
\n";
-
-val end_document = "\n\n\n\n";
-
-end;