# HG changeset patch
# User wenzelm
# Date 1124192571 -7200
# Node ID c0c213a8f39cbc3164a02fe9caf7733168168453
# Parent ce96639871261bf91bf3423e23926bb9867c3da1
begin_index: list of docs;
diff -r ce9663987126 -r c0c213a8f39c src/Pure/Thy/html.ML
--- a/src/Pure/Thy/html.ML Tue Aug 16 13:42:50 2005 +0200
+++ b/src/Pure/Thy/html.ML Tue Aug 16 13:42:51 2005 +0200
@@ -22,8 +22,7 @@
val para: text -> text
val preform: text -> text
val verbatim: string -> text
- val begin_index: Url.T * string -> Url.T * string -> Url.T option
- -> Url.T option -> Url.T -> text
+ val begin_index: Url.T * string -> Url.T * string -> (Url.T * string) list -> Url.T -> text
val end_index: text
val applet_pages: string -> Url.T * string -> (string * string) list
val theory_entry: Url.T * string -> text
@@ -293,7 +292,8 @@
(* document *)
fun begin_document title =
- "\n\
+ "\n\
\\n\
\\n\
\\n\
@@ -315,11 +315,10 @@
(* session index *)
-fun begin_index up (index_path, session) opt_readme opt_doc graph =
+fun begin_index up (index_path, session) docs graph =
begin_document ("Index of " ^ session) ^ up_link up ^
para ("View " ^ href_path graph "theory dependencies" ^
- (case opt_readme of NONE => "" | SOME p => "
\nView " ^ href_path p "README") ^
- (case opt_doc of NONE => "" | SOME p => "
\nView " ^ href_path p "document")) ^
+ implode (map (fn (p, name) => "
\nView " ^ href_path p name) docs)) ^
"\n\n
\n\n
Theories
\n
\n";
val end_index = end_document;
@@ -342,7 +341,8 @@
(name, begin_document ("Theory dependencies of " ^ session) ^
back_link back ^
para browser_size ^
- "\n
\n\n