src/Pure/Thy/thy_read.ML

     close_in instream
   end;
 
 fun file_exists file = (file_info file <> "");
 
+(*Get last directory in path (e.g. /usr/proj/isabelle -> isabelle) *)
+fun last_path s = case space_explode "/" s of
+                      [] => ""
+                    | ds => last_elem ds;
+
 (*Get thy_info for a loaded theory *)
 fun get_thyinfo tname = Symtab.lookup (!loaded_thys, tname);
 
 (*Check if a theory was completly loaded *)
 fun already_loaded thy =

       if (!index_path) = "" then
         error "index_path is empty. Please use 'init_html()' instead of \
               \'make_html := true'"
       else if (!index_path) subdir_of (!base_path) then
         relative_path (!base_path) (!index_path)
-      else
-        last_elem (space_explode "/" (!index_path));
+      else last_path (!index_path);
     val rel_index_path = relative_path tpath (!index_path);
 
     (*Make list of all theories and all theories that own a .thy file*)
     fun list_theories [] theories thy_files = (theories, thy_files)
       | list_theories ((tname, ThyInfo {thy_time, ...}) :: ts)

                  tack_on gif_path "blue_arrow.gif\" ALT = /\\></A>\n");
                close_out out
             end;
  
           val theory_list =
-            open_append (tack_on (!index_path) ".theory_list.txt");
+            open_append (tack_on (!index_path) ".theory_list.txt")
+              handle _ => (make_html := false;
+                           writeln ("Warning: Cannot write to " ^
+                                  (!index_path) ^ " while making HTML files.\n\
+                                  \HTML generation has been switched off.\n\
+                                  \Call init_html() from within a \
+                                  \writeable directory to reactivate it.");
+                           raise MK_HTML)
       in output (theory_list, tname ^ " " ^ abs_path ^ "\n");
          close_out theory_list;
  
          robust_seq add_to_parents new_parents
       end

 
        (*Add theory to list of all loaded theories (for index.html)
          and add it to its parents' sub-charts*)
        if !make_html then
          let val path = path_of tname;
-         in if path = "" then mk_html ()    (*first time theory has been read*)
+         in if path = "" then               (*first time theory has been read*)
+              (mk_html()  handle MK_HTML => ())
             else ()
          end
        else ();
 
        (*Now set the correct info*)

         let val pure_out = open_out ".Pure_sub.html";
             val cpure_out = open_out ".CPure_sub.html";
             val package =
               if cwd subdir_of (!base_path) then
                 relative_path (!base_path) cwd
-              else
-                last_elem (space_explode "/" cwd);
+              else last_path cwd;
         in mk_charthead pure_out "Pure" "Children" false rel_gif_path ""
                         package;
            mk_charthead cpure_out "CPure" "Children" false rel_gif_path ""
                         package;
            output (pure_out, "Pure\n");

         index.html is placed; if index_path is no subdirectory of base_path
         then take the last directory of index_path*)
       val inside_isabelle = (!index_path) subdir_of (!base_path);
       val subdir =
         if inside_isabelle then relative_path (!base_path) (!index_path)
-        else last_elem (space_explode "/" (!index_path));
+        else last_path (!index_path);
       val subdirs = space_explode "/" subdir;
 
       (*Look for index.html in superdirectories; stop when Isabelle's
         main directory is reached*)
       fun find_super_index [] n = ("", n)