--- a/src/Pure/General/file.scala Fri Aug 30 21:14:38 2013 +0200
+++ b/src/Pure/General/file.scala Fri Aug 30 22:22:07 2013 +0200
@@ -126,6 +126,12 @@
def write_gzip(path: Path, text: Iterable[CharSequence]): Unit = write_gzip(path.file, text)
def write_gzip(path: Path, text: CharSequence): Unit = write_gzip(path.file, text)
+ def write_backup(path: Path, text: CharSequence)
+ {
+ path.file renameTo path.backup.file
+ File.write(path, text)
+ }
+
/* copy */
--- a/src/Pure/General/path.scala Fri Aug 30 21:14:38 2013 +0200
+++ b/src/Pure/General/path.scala Fri Aug 30 22:22:07 2013 +0200
@@ -149,6 +149,12 @@
prfx + Path.basic(s + "." + e)
}
+ def backup: Path =
+ {
+ val (prfx, s) = split_path
+ prfx + Path.basic(s + "~")
+ }
+
private val Ext = new Regex("(.*)\\.([^.]*)")
def split_ext: (Path, String) =
--- a/src/Pure/System/options.scala Fri Aug 30 21:14:38 2013 +0200
+++ b/src/Pure/System/options.scala Fri Aug 30 22:22:07 2013 +0200
@@ -66,7 +66,6 @@
private val OPTIONS = Path.explode("etc/options")
private val PREFS_DIR = Path.explode("$ISABELLE_HOME_USER/etc")
private val PREFS = PREFS_DIR + Path.basic("preferences")
- private val PREFS_BACKUP = PREFS_DIR + Path.basic("preferences~")
lazy val options_syntax =
Outer_Syntax.init() + ":" + "=" + "--" +
@@ -359,8 +358,7 @@
.map({ case (x, y, z) => x + " = " + Outer_Syntax.quote_string(y) + z + "\n" }).mkString
Isabelle_System.mkdirs(Options.PREFS_DIR)
- Options.PREFS.file renameTo Options.PREFS_BACKUP.file
- File.write(Options.PREFS,
+ File.write_backup(Options.PREFS,
"(* generated by Isabelle " + Calendar.getInstance.getTime + " *)\n\n" + prefs)
}
}