# 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\ + \
" ^ output_chars (Source.exhaust src) ^ "\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