# HG changeset patch
# User wenzelm
# Date 921839200 -3600
# Node ID 39922bfb7107fd2bd1c911c0ece6f94eb908b5c8
# Parent 2daaf2943c7916fde11f025c46dc2f6f319a1778
tuned;
diff -r 2daaf2943c79 -r 39922bfb7107 src/Pure/Thy/html.ML
--- a/src/Pure/Thy/html.ML Fri Mar 19 11:24:00 1999 +0100
+++ b/src/Pure/Thy/html.ML Fri Mar 19 11:26:40 1999 +0100
@@ -22,8 +22,6 @@
val para: text -> text
val preform: text -> text
val verbatim: string -> text
- val begin_document: string -> text
- val end_document: text
val begin_index: Path.T * string -> Path.T * string -> Path.T option -> text
val end_index: text
val theory_entry: Path.T * string -> text
@@ -132,19 +130,15 @@
(* document *)
fun begin_document title =
- let val txt = plain title in
- "\n\
- \\n\
- \" ^ txt ^ "\n\
- \\n\
- \\n\
- \\n\
- \" ^ txt ^ "
\n"
- end;
+ "\n\
+ \\n\
+ \" ^ plain (title ^ " (" ^ version ^ ")") ^ "\n\
+ \\n\
+ \\n\
+ \\n\
+ \" ^ plain title ^ "
\n"
-val end_document =
- "\n\
- \\n";
+val end_document = "\n\n\n";
fun up_link (up_path, up_name) =
para (href_path up_path "Up" ^ " to index of " ^ plain up_name);
@@ -154,16 +148,18 @@
fun begin_index up (index_path, session) opt_readme =
begin_document ("Index of " ^ session) ^ up_link up ^
- (case opt_readme of None => "" | Some p => href_path p "README" ^ " file") ^
- "\n
\n\nTheories
\n";
+ (case opt_readme of None => "" | Some p => href_path p "README") ^
+ "\n
\n\nTheories
\n\n";
val end_index = end_document;
-fun entry (p, s) = href_path p (plain s) ^ "
\n";
+fun entry (p, s) = "- " ^ href_path p (plain s) ^ "\n";
+
val theory_entry = entry;
-fun session_entries [] = ""
- | session_entries es = "\n
\n\nSessions
\n" ^ cat_lines (map entry es);
+fun session_entries [] = "
"
+ | session_entries es =
+ "\n
\n\nSessions
\n\n" ^ implode (map entry es) ^ "
";
(* theory *)