src/Pure/Thy/present.ML

   in
    {name = name, ID = ID_of session name, dir = sess_name,
     path =
       if null session then "" else
       if is_some remote_path andalso not is_local then
-        Url.pack (Url.append (the remote_path) (Url.file
+        Url.pack (Url.append (the remote_path) (Url.File
           (Path.append (Path.make session) (html_path name))))
       else Path.pack (Path.append (mk_rel_path curr_sess session) (html_path name)),
     unfold = false,
     parents =
       map (fn s => ID_of (#session (get_info (ThyInfo.theory s))) s) (ThyInfo.get_preds name)}

 
 (* maintain index *)
 
 val session_entries =
   HTML.session_entries o
-    map (fn name => (Url.file (Path.append (Path.basic name) index_path), name));
+    map (fn name => (Url.File (Path.append (Path.basic name) index_path), name));
 
 fun get_entries dir =
   split_lines (File.read (Path.append dir session_entries_path));
 
 fun put_entries entries dir =

           std_error "Warning: missing document directory\n"); (None, None))
         else (Some (Path.append html_prefix doc_path), Some (Path.ext doc doc_path));
 
       val parent_index_path = Path.append Path.parent index_path;
       val index_up_lnk = if first_time then
-          Url.append (the remote_path) (Url.file (Path.append sess_prefix parent_index_path))
-        else Url.file parent_index_path;
+          Url.append (the remote_path) (Url.File (Path.append sess_prefix parent_index_path))
+        else Url.File parent_index_path;
       val readme =
         if File.exists readme_html_path then Some readme_html_path
         else if File.exists readme_path then Some readme_path
         else None;
 
       val index_text = HTML.begin_index (index_up_lnk, parent_name)
-        (Url.file index_path, session_name) (apsome Url.file readme)
-          (apsome Url.file document_path) (Url.unpack "medium.html");
+        (Url.File index_path, session_name) (apsome Url.File readme)
+          (apsome Url.File document_path) (Url.unpack "medium.html");
     in
       session_info := Some (make_session_info (name, parent_name, session_name, path, html_prefix,
       info, doc, doc_graph, doc_prefix1, doc_prefix2, remote_path, verbose, readme));
       browser_info := init_browser_info remote_path path;
       add_html_index index_text

       if length path > 1 then update_index parent_html_prefix name else ();
       (case readme of None => () | Some path => File.copy path (Path.append html_prefix path));
       write_graph graph (Path.append html_prefix graph_path);
       copy_files (Path.unpack "~~/lib/browser/GraphBrowser.jar") html_prefix;
       seq (fn (a, txt) => File.write (Path.append html_prefix (Path.basic a)) txt)
-        (HTML.applet_pages name (Url.file index_path, name));
+        (HTML.applet_pages name (Url.File index_path, name));
       copy_files (Path.unpack "~~/lib/html/isabelle.css") html_prefix;
       seq finish_html thys;
       seq (uncurry File.write) files;
       conditional verbose (fn () =>
         std_error ("Browser info at " ^ show_path html_prefix ^ "\n"))));

 
 fun parent_link remote_path curr_session name =
   let val {name = _, session, is_local} = get_info (ThyInfo.theory name)
   in (if null session then None else
      Some (if is_some remote_path andalso not is_local then
-       Url.append (the remote_path) (Url.file
+       Url.append (the remote_path) (Url.File
          (Path.append (Path.make session) (html_path name)))
-     else Url.file (Path.append (mk_rel_path curr_session session)
+     else Url.File (Path.append (mk_rel_path curr_session session)
        (html_path name))), name)
   end;
 
 fun begin_theory name raw_parents orig_files thy =
     with_session thy (fn {name = sess_name, session, path, html_prefix, remote_path, ...} =>

           let
             val base = Path.base path;
             val base_html = html_ext base;
           in
             add_file (Path.append html_prefix base_html,
-              HTML.ml_file (Url.file base) (File.read path));
-            (Some (Url.file base_html), Url.file raw_path, loadit)
+              HTML.ml_file (Url.File base) (File.read path));
+            (Some (Url.File base_html), Url.File raw_path, loadit)
           end
       | None => (warning ("Browser info: expected to find ML file" ^ quote (Path.pack raw_path));
-          (None, Url.file raw_path, loadit)));
+          (None, Url.File raw_path, loadit)));
 
     val files_html = map prep_file files;
 
     fun prep_html_source (tex_source, html_source, html) =
       let
-        val txt = HTML.begin_theory (Url.file index_path, session)
+        val txt = HTML.begin_theory (Url.File index_path, session)
           name parents files_html (Buffer.content html_source)
       in (tex_source, Buffer.empty, Buffer.add txt html) end;
 
     val entry =
      {name = name, ID = ID_of path name, dir = sess_name, unfold = true,

       parents = map (fn s => ID_of (#session (get_info (ThyInfo.theory s))) s) raw_parents};
 
   in
     change_theory_info name prep_html_source;
     add_graph_entry entry;
-    add_html_index (HTML.theory_entry (Url.file (html_path name), name));
+    add_html_index (HTML.theory_entry (Url.File (html_path name), name));
     add_tex_index (Latex.theory_entry name);
     BrowserInfoData.put {name = sess_name, session = path, is_local = is_some remote_path} thy
   end);