# HG changeset patch
# User wenzelm
# Date 920977965 -3600
# Node ID 3b7111b360b1d073210dbf7cdd9e1902b9274150
# Parent e5b3e46d5dbdcf1c267c8d05df8ca32ce1e1809c
HTML markup elements.
diff -r e5b3e46d5dbd -r 3b7111b360b1 src/Pure/Thy/html.ML
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Thy/html.ML Tue Mar 09 12:12:45 1999 +0100
@@ -0,0 +1,185 @@
+(* Title: Pure/Thy/HTML.ML
+ ID: $Id$
+ Author: Markus Wenzel, TU Muenchen
+
+HTML markup elements.
+*)
+
+signature HTML =
+sig
+ val output: string -> string
+ val output_width: string -> string * real
+ type text (* = string *)
+ val plain: string -> text
+ val name: string -> text
+ val keyword: string -> text
+ val file_name: string -> text
+ val file_path: Path.T -> text
+ val para: text -> text
+ val href_name: string -> text -> text
+ val href_path: Path.T -> text -> text
+ val preform: text -> text
+ val verbatim: string -> text
+ val begin_document: string -> text
+ val end_document: text
+ val insert_here: text
+ val source: (string, 'a) Source.source -> text
+ val begin_theory: Path.T * string -> string -> string list -> ((Path.T * Path.T) * bool) list
+ -> text -> text
+ val end_theory: text
+ val ml_file: Path.T -> string -> text
+ val conclude_theory: text
+ val theorem: string -> thm -> text
+ val section: string -> text
+ val setup: (theory -> theory) list
+end;
+
+structure HTML: HTML =
+struct
+
+
+(** HTML print modes **)
+
+(* mode *)
+
+val htmlN = "HTML";
+fun html_mode f x = setmp print_mode [htmlN] f x;
+
+
+(* symbol output *)
+
+val escape = fn "<" => "<" | ">" => ">" | "&" => "&" | c => c;
+
+val output_chars = implode o map escape;
+
+fun output s =
+ if not (exists_string (equal "<" orf equal ">" orf equal "&") s) then s
+ else implode (map escape (explode s)); (*sic!*)
+
+fun output_width s = (output s, real (size s));
+
+val _ = Symbol.add_mode htmlN output_width;
+
+
+(* token translations *)
+
+fun tagit bg en = apfst (enclose bg en) o output_width;
+fun color col = tagit ("") "";
+
+val html_trans =
+ [("class", color "red"),
+ ("tfree", color "purple"),
+ ("tvar", color "purple"),
+ ("free", color "blue"),
+ ("bound", color "green"),
+ ("var", color "blue"),
+ ("xnum", color "yellow"),
+ ("xstr", color "brown")];
+
+
+
+(** HTML markup **)
+
+type text = string;
+
+
+(* atoms *)
+
+val plain = output;
+fun name s = "" ^ output s ^ "";
+fun keyword s = "" ^ output s ^ "";
+fun file_name s = "" ^ output s ^ "";
+val file_path = file_name o Path.pack;
+
+
+(* misc *)
+
+fun para txt = "\n\n" ^ txt ^ "\n
\n";
+fun href_name s txt = "" ^ txt ^ "";
+fun href_path path txt = href_name (Path.pack path) txt;
+fun preform txt = "" ^ txt ^ "
";
+val verbatim = preform o output;
+
+
+(* document *)
+
+fun begin_document title =
+ let val txt = plain title in
+ "\n\
+ \\n\
+ \" ^ txt ^ "\n\
+ \\n\
+ \\n\
+ \\n\
+ \" ^ txt ^ "
\n"
+ end;
+
+val end_document =
+ "\n\
+ \\n";
+
+val insert_here = "";
+
+
+(* theory *)
+
+fun source src =
+ "\n
\n" ^ output_chars (Source.exhaust src) ^ "
\n
\n";
+
+
+local
+ fun file ((p, p'), loadit) =
+ href_path p' ((if not loadit then enclose "(" ")" else I) (file_path p));
+
+ fun suffix_last _ [] = []
+ | suffix_last s lst = let val (xs, x) = split_last lst in xs @ [x ^ s] end;
+
+ val plus_names = space_implode " + " o map name;
+
+ fun theory (back_path, back_name) A =
+ begin_document ("Theory " ^ A) ^ "\n" ^
+ href_path back_path "Back" ^ " to the index of " ^ plain back_name ^ "\n\n" ^
+ keyword "theory" ^ " " ^ name A ^ " = ";
+in
+
+fun begin_theory back A Bs [] body = theory back A ^ plus_names (suffix_last ":" Bs) ^ "\n" ^ body
+ | begin_theory back A Bs Ps body =
+ theory back A ^ plus_names Bs ^
+ "
" ^ keyword "files" ^ " " ^ space_implode " + " (map file Ps) ^ ":" ^ "\n" ^ body;
+end;
+
+val end_theory = "";
+val conclude_theory = end_document;
+
+
+(* ML file *)
+
+fun ml_file path str =
+ begin_document ("File " ^ Path.pack path) ^
+ "\n
\n" ^ verbatim str ^ "\n
\n" ^ end_document;
+
+
+(* theorem *)
+
+(* FIXME improve freeze_thaw (?) *)
+val string_of_thm =
+ Pretty.setmp_margin 80 Pretty.string_of o
+ Display.pretty_thm_no_quote o #1 o Drule.freeze_thaw;
+
+fun thm th = preform (prefix_lines " " (html_mode string_of_thm th));
+fun theorem a th = para (keyword "theorem" ^ " " ^ name (a ^ ":") ^ "\n" ^ thm th);
+
+
+(* section *)
+
+fun section heading = "\n\n" ^ plain heading ^ "
\n";
+
+
+
+(** theory setup **)
+
+val setup =
+ [Theory.add_mode_tokentrfuns htmlN html_trans];
+
+
+end;