src/Pure/Thy/present.ML

       val sess_prefix = Path.make path;
       val html_prefix = Path.append (Path.expand output_path) sess_prefix;
 
       val (doc_prefix1, documents) =
         if doc = "" then (NONE, [])
-        else if not (File.exists document_path) then
+        else if not (can File.check_dir document_path) then
           (if verbose then Output.raw_stderr "Warning: missing document directory\n" else ();
             (NONE, []))
         else (SOME (Path.append html_prefix document_path, html_prefix),
           read_variants doc_variants);
 

         map (fn (name, _) => (Url.File (Path.ext doc (Path.basic name)), name)) documents;
       val index_text = HTML.begin_index (index_up_lnk, parent_name)
         (Url.File index_path, session_name) docs (Url.explode "medium.html");
     in
       session_info := SOME (make_session_info (name, parent_name, session_name, path, html_prefix,
-      info, doc, doc_graph, documents, doc_prefix1, doc_prefix2, remote_path, verbose, readme));
+        info, doc, doc_graph, documents, doc_prefix1, doc_prefix2, remote_path, verbose, readme));
       browser_info := init_browser_info remote_path path thys;
       add_html_index (0, index_text)
     end);