src/Pure/Thy/present.ML
changeset 42005 78bb3ec281c2
parent 42004 e06351ffb475
child 42006 7eecd020e367
     1.1 --- a/src/Pure/Thy/present.ML	Sun Mar 20 18:09:32 2011 +0100
     1.2 +++ b/src/Pure/Thy/present.ML	Sun Mar 20 18:56:36 2011 +0100
     1.3 @@ -292,7 +292,7 @@
     1.4  
     1.5        val (doc_prefix1, documents) =
     1.6          if doc = "" then (NONE, [])
     1.7 -        else if not (File.exists document_path) then
     1.8 +        else if not (can File.check_dir document_path) then
     1.9            (if verbose then Output.raw_stderr "Warning: missing document directory\n" else ();
    1.10              (NONE, []))
    1.11          else (SOME (Path.append html_prefix document_path, html_prefix),
    1.12 @@ -314,7 +314,7 @@
    1.13          (Url.File index_path, session_name) docs (Url.explode "medium.html");
    1.14      in
    1.15        session_info := SOME (make_session_info (name, parent_name, session_name, path, html_prefix,
    1.16 -      info, doc, doc_graph, documents, doc_prefix1, doc_prefix2, remote_path, verbose, readme));
    1.17 +        info, doc, doc_graph, documents, doc_prefix1, doc_prefix2, remote_path, verbose, readme));
    1.18        browser_info := init_browser_info remote_path path thys;
    1.19        add_html_index (0, index_text)
    1.20      end);