# HG changeset patch # User wenzelm # Date 1358198697 -3600 # Node ID d55eb82ae77b31d9b262dd2d6d46d317f95dce20 # Parent 9a7d81d66d090c198682f1d8909230a323aac3e2 Isabelle_System.mkdirs with explicit error checking (in accordance to ML version), e.g. relevant with read-only DMG file-system on Mac OS X; diff -r 9a7d81d66d09 -r d55eb82ae77b src/Pure/System/isabelle_system.scala --- a/src/Pure/System/isabelle_system.scala Mon Jan 14 21:37:42 2013 +0100 +++ b/src/Pure/System/isabelle_system.scala Mon Jan 14 22:24:57 2013 +0100 @@ -210,6 +210,15 @@ } + /* mkdirs */ + + def mkdirs(path: Path) + { + path.file.mkdirs + if (!path.is_dir) error("Cannot create directory: " + quote(platform_path(path))) + } + + /** external processes **/ diff -r 9a7d81d66d09 -r d55eb82ae77b src/Pure/System/options.scala --- a/src/Pure/System/options.scala Mon Jan 14 21:37:42 2013 +0100 +++ b/src/Pure/System/options.scala Mon Jan 14 22:24:57 2013 +0100 @@ -348,7 +348,7 @@ changed.sortBy(_._1) .map({ case (x, y, z) => x + " = " + Outer_Syntax.quote_string(y) + z + "\n" }).mkString - Options.PREFS_DIR.file.mkdirs() + Isabelle_System.mkdirs(Options.PREFS_DIR) Options.PREFS.file renameTo Options.PREFS_BACKUP.file File.write(Options.PREFS, "(* generated by Isabelle " + Calendar.getInstance.getTime + " *)\n\n" + prefs) diff -r 9a7d81d66d09 -r d55eb82ae77b src/Pure/Tools/build.scala --- a/src/Pure/Tools/build.scala Mon Jan 14 21:37:42 2013 +0100 +++ b/src/Pure/Tools/build.scala Mon Jan 14 22:24:57 2013 +0100 @@ -424,7 +424,7 @@ // global browser info dir if (info.options.bool("browser_info") && !(browser_info + Path.explode("index.html")).is_file) { - browser_info.file.mkdirs() + Isabelle_System.mkdirs(browser_info) File.copy(Path.explode("~~/lib/logo/isabelle.gif"), browser_info + Path.explode("isabelle.gif")) File.write(browser_info + Path.explode("index.html"), @@ -614,7 +614,7 @@ } // prepare log dir - (output_dir + LOG).file.mkdirs() + Isabelle_System.mkdirs(output_dir + LOG) // optional cleanup if (clean_build) {