20 val href_opt_name: string option -> text -> text |
20 val href_opt_name: string option -> text -> text |
21 val href_opt_path: Path.T option -> text -> text |
21 val href_opt_path: Path.T option -> text -> text |
22 val para: text -> text |
22 val para: text -> text |
23 val preform: text -> text |
23 val preform: text -> text |
24 val verbatim: string -> text |
24 val verbatim: string -> text |
25 val begin_document: string -> text |
|
26 val end_document: text |
|
27 val begin_index: Path.T * string -> Path.T * string -> Path.T option -> text |
25 val begin_index: Path.T * string -> Path.T * string -> Path.T option -> text |
28 val end_index: text |
26 val end_index: text |
29 val theory_entry: Path.T * string -> text |
27 val theory_entry: Path.T * string -> text |
30 val session_entries: (Path.T * string) list -> text |
28 val session_entries: (Path.T * string) list -> text |
31 val source: (string, 'a) Source.source -> text |
29 val source: (string, 'a) Source.source -> text |
130 |
128 |
131 |
129 |
132 (* document *) |
130 (* document *) |
133 |
131 |
134 fun begin_document title = |
132 fun begin_document title = |
135 let val txt = plain title in |
133 "<html>\n\ |
136 "<html>\n\ |
134 \<head>\n\ |
137 \<head>\n\ |
135 \<title>" ^ plain (title ^ " (" ^ version ^ ")") ^ "</title>\n\ |
138 \<title>" ^ txt ^ "</title>\n\ |
136 \</head>\n\ |
139 \</head>\n\ |
137 \\n\ |
140 \\n\ |
138 \<body>\n\ |
141 \<body>\n\ |
139 \<h1>" ^ plain title ^ "</h1>\n" |
142 \<h1>" ^ txt ^ "</h1>\n" |
140 |
143 end; |
141 val end_document = "\n</body>\n</html>\n"; |
144 |
|
145 val end_document = |
|
146 "</body>\n\ |
|
147 \</html>\n"; |
|
148 |
142 |
149 fun up_link (up_path, up_name) = |
143 fun up_link (up_path, up_name) = |
150 para (href_path up_path "Up" ^ " to index of " ^ plain up_name); |
144 para (href_path up_path "Up" ^ " to index of " ^ plain up_name); |
151 |
145 |
152 |
146 |
153 (* session index *) |
147 (* session index *) |
154 |
148 |
155 fun begin_index up (index_path, session) opt_readme = |
149 fun begin_index up (index_path, session) opt_readme = |
156 begin_document ("Index of " ^ session) ^ up_link up ^ |
150 begin_document ("Index of " ^ session) ^ up_link up ^ |
157 (case opt_readme of None => "" | Some p => href_path p "README" ^ " file") ^ |
151 (case opt_readme of None => "" | Some p => href_path p "README") ^ |
158 "\n<hr>\n\n<h2>Theories</h2>\n"; |
152 "\n<hr>\n\n<h2>Theories</h2>\n<ul>\n"; |
159 |
153 |
160 val end_index = end_document; |
154 val end_index = end_document; |
161 |
155 |
162 fun entry (p, s) = href_path p (plain s) ^ "<br>\n"; |
156 fun entry (p, s) = "<li>" ^ href_path p (plain s) ^ "\n"; |
|
157 |
163 val theory_entry = entry; |
158 val theory_entry = entry; |
164 |
159 |
165 fun session_entries [] = "" |
160 fun session_entries [] = "</ul>" |
166 | session_entries es = "\n<hr>\n\n<h2>Sessions</h2>\n" ^ cat_lines (map entry es); |
161 | session_entries es = |
|
162 "</ul>\n<hr>\n\n<h2>Sessions</h2>\n<ul>\n" ^ implode (map entry es) ^ "</ul>"; |
167 |
163 |
168 |
164 |
169 (* theory *) |
165 (* theory *) |
170 |
166 |
171 fun output_source src = implode (output_symbols (Source.exhaust (Symbol.source false src))); |
167 fun output_source src = implode (output_symbols (Source.exhaust (Symbol.source false src))); |