1.1 --- a/src/Pure/Thy/html.ML	Thu Dec 14 22:19:39 2006 +0100
     1.2 +++ b/src/Pure/Thy/html.ML	Fri Dec 15 00:08:06 2006 +0100
     1.3 @@ -266,13 +266,13 @@
     1.4  val keyword = enclose "<span class=\"keyword\">" "</span>" o output;
     1.5  val keyword_width = apfst (enclose "<span class=\"keyword\">" "</span>") o output_width;
     1.6  val file_name = enclose "<span class=\"filename\">" "</span>" o output;
     1.7 -val file_path = file_name o Url.pack;
     1.8 +val file_path = file_name o Url.implode;
     1.9  
    1.10  
    1.11  (* misc *)
    1.12  
    1.13  fun href_name s txt = "<a href=" ^ Library.quote s ^ ">" ^ txt ^ "</a>";
    1.14 -fun href_path path txt = href_name (Url.pack path) txt;
    1.15 +fun href_path path txt = href_name (Url.implode path) txt;
    1.16  
    1.17  fun href_opt_name NONE txt = txt
    1.18    | href_opt_name (SOME s) txt = href_name s txt;
    1.19 @@ -400,7 +400,7 @@
    1.20  (* ML file *)
    1.21  
    1.22  fun ml_file path str =
    1.23 -  begin_document ("File " ^ Url.pack path) ^
    1.24 +  begin_document ("File " ^ Url.implode path) ^
    1.25    "\n</div>\n<hr><div class=\"mlsource\">\n" ^
    1.26    verbatim str ^
    1.27    "\n</div>\n<hr>\n<div class=\"mlfooter\">\n" ^