tuned;
authorwenzelm
Fri Mar 19 11:26:40 1999 +0100 (1999-03-19)
changeset 640539922bfb7107
parent 6404 2daaf2943c79
child 6406 0f6076dca737
tuned;
src/Pure/Thy/html.ML
     1.1 --- a/src/Pure/Thy/html.ML	Fri Mar 19 11:24:00 1999 +0100
     1.2 +++ b/src/Pure/Thy/html.ML	Fri Mar 19 11:26:40 1999 +0100
     1.3 @@ -22,8 +22,6 @@
     1.4    val para: text -> text
     1.5    val preform: text -> text
     1.6    val verbatim: string -> text
     1.7 -  val begin_document: string -> text
     1.8 -  val end_document: text
     1.9    val begin_index: Path.T * string -> Path.T * string -> Path.T option -> text
    1.10    val end_index: text
    1.11    val theory_entry: Path.T * string -> text
    1.12 @@ -132,19 +130,15 @@
    1.13  (* document *)
    1.14  
    1.15  fun begin_document title =
    1.16 -  let val txt = plain title in
    1.17 -    "<html>\n\
    1.18 -    \<head>\n\
    1.19 -    \<title>" ^ txt ^ "</title>\n\
    1.20 -    \</head>\n\
    1.21 -    \\n\
    1.22 -    \<body>\n\
    1.23 -    \<h1>" ^ txt ^ "</h1>\n"
    1.24 -  end;
    1.25 +  "<html>\n\
    1.26 +  \<head>\n\
    1.27 +  \<title>" ^ plain (title ^ " (" ^ version ^ ")") ^ "</title>\n\
    1.28 +  \</head>\n\
    1.29 +  \\n\
    1.30 +  \<body>\n\
    1.31 +  \<h1>" ^ plain title ^ "</h1>\n"
    1.32  
    1.33 -val end_document =
    1.34 -  "</body>\n\
    1.35 -  \</html>\n";
    1.36 +val end_document = "\n</body>\n</html>\n";
    1.37  
    1.38  fun up_link (up_path, up_name) =
    1.39    para (href_path up_path "Up" ^ " to index of " ^ plain up_name);
    1.40 @@ -154,16 +148,18 @@
    1.41  
    1.42  fun begin_index up (index_path, session) opt_readme =
    1.43    begin_document ("Index of " ^ session) ^ up_link up ^
    1.44 -  (case opt_readme of None => "" | Some p => href_path p "README" ^ " file") ^
    1.45 -  "\n<hr>\n\n<h2>Theories</h2>\n";
    1.46 +  (case opt_readme of None => "" | Some p => href_path p "README") ^
    1.47 +  "\n<hr>\n\n<h2>Theories</h2>\n<ul>\n";
    1.48  
    1.49  val end_index = end_document;
    1.50  
    1.51 -fun entry (p, s) = href_path p (plain s) ^ "<br>\n";
    1.52 +fun entry (p, s) = "<li>" ^ href_path p (plain s) ^ "\n";
    1.53 +
    1.54  val theory_entry = entry;
    1.55  
    1.56 -fun session_entries [] = ""
    1.57 -  | session_entries es = "\n<hr>\n\n<h2>Sessions</h2>\n" ^ cat_lines (map entry es);
    1.58 +fun session_entries [] = "</ul>"
    1.59 +  | session_entries es =
    1.60 +      "</ul>\n<hr>\n\n<h2>Sessions</h2>\n<ul>\n" ^ implode (map entry es) ^ "</ul>";
    1.61  
    1.62  
    1.63  (* theory *)