# HG changeset patch
# User wenzelm
# Date 1377894127 -7200
# Node ID b3bf6d72fea55d5c2550ee003dae5ce53c6e3eb2
# Parent  646a224ca76a890ad9b84df8597b4ac85817fb9b
more general backup files;

diff -r 646a224ca76a -r b3bf6d72fea5 src/Pure/General/file.scala
--- 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 */
 
diff -r 646a224ca76a -r b3bf6d72fea5 src/Pure/General/path.scala
--- 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) =
diff -r 646a224ca76a -r b3bf6d72fea5 src/Pure/System/options.scala
--- 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)
   }
 }