equal
deleted
inserted
replaced
14 val name: symbols -> string -> text |
14 val name: symbols -> string -> text |
15 val keyword: symbols -> string -> text |
15 val keyword: symbols -> string -> text |
16 val command: symbols -> string -> text |
16 val command: symbols -> string -> text |
17 val href_name: string -> string -> string |
17 val href_name: string -> string -> string |
18 val href_path: Url.T -> string -> string |
18 val href_path: Url.T -> string -> string |
19 val href_opt_path: Url.T option -> string -> string |
|
20 val begin_document: symbols -> string -> text |
19 val begin_document: symbols -> string -> text |
21 val end_document: text |
20 val end_document: text |
22 end; |
21 end; |
23 |
22 |
24 structure HTML: HTML = |
23 structure HTML: HTML = |
118 (* misc *) |
117 (* misc *) |
119 |
118 |
120 fun href_name s txt = "<a href=" ^ quote s ^ ">" ^ txt ^ "</a>"; |
119 fun href_name s txt = "<a href=" ^ quote s ^ ">" ^ txt ^ "</a>"; |
121 fun href_path path txt = href_name (Url.implode path) txt; |
120 fun href_path path txt = href_name (Url.implode path) txt; |
122 |
121 |
123 fun href_opt_path NONE txt = txt |
|
124 | href_opt_path (SOME p) txt = href_path p txt; |
|
125 |
|
126 |
122 |
127 (* document *) |
123 (* document *) |
128 |
124 |
129 fun begin_document symbols title = |
125 fun begin_document symbols title = |
130 XML.header ^ |
126 XML.header ^ |