# HG changeset patch
# User wenzelm
# Date 1493893819 -7200
# Node ID e57e5935c6b4e416627cb1f293b214f424138856
# Parent  7693ba6d65bc9ccb2fd1c1201473a041bc7d0fed
prefer standard getOrElse;

diff -r 7693ba6d65bc -r e57e5935c6b4 src/Pure/Admin/build_release.scala
--- a/src/Pure/Admin/build_release.scala	Thu May 04 12:27:18 2017 +0200
+++ b/src/Pure/Admin/build_release.scala	Thu May 04 12:30:19 2017 +0200
@@ -55,7 +55,7 @@
     val release_info =
     {
       val date = Date.now()
-      val name = proper_string_default(release_name, "Isabelle_" + Date.Format.date(date))
+      val name = proper_string(release_name) getOrElse ("Isabelle_" + Date.Format.date(date))
       val dist_dir = base_dir + Path.explode("dist-" + name)
       val dist_archive = dist_dir + Path.explode(name + ".tar.gz")
       val dist_library_archive = dist_dir + Path.explode(name + "_library.tar.gz")
diff -r 7693ba6d65bc -r e57e5935c6b4 src/Pure/ROOT.scala
--- a/src/Pure/ROOT.scala	Thu May 04 12:27:18 2017 +0200
+++ b/src/Pure/ROOT.scala	Thu May 04 12:30:19 2017 +0200
@@ -19,5 +19,4 @@
   val commas = Library.commas _
   val commas_quote = Library.commas_quote _
   val proper_string = Library.proper_string _
-  val proper_string_default = Library.proper_string_default _
 }
diff -r 7693ba6d65bc -r e57e5935c6b4 src/Pure/library.scala
--- a/src/Pure/library.scala	Thu May 04 12:27:18 2017 +0200
+++ b/src/Pure/library.scala	Thu May 04 12:30:19 2017 +0200
@@ -147,9 +147,6 @@
   def proper_string(s: String): Option[String] =
     if (s == "") None else Some(s)
 
-  def proper_string_default(s: String, default: => String): String =
-    if (s == "") default else s
-
 
   /* quote */