tuned;

--- a/src/Pure/Admin/build_history.scala	Fri Feb 24 20:23:48 2023 +0100
+++ b/src/Pure/Admin/build_history.scala	Fri Feb 24 20:40:50 2023 +0100
@@ -582,7 +582,7 @@
     else {
       ssh.with_tmp_dir { tmp_dir =>
         val output_file = tmp_dir + Path.explode("output")
-        val build_options = (if (afp_repos.isEmpty) "" else " -A") + " " + options
+        val build_options = if_proper(afp_repos, " -A") + " " + options
         try {
           val script =
             ssh.bash_path(Path.explode("Admin/build_other")) +

--- a/src/Pure/Admin/build_status.scala	Fri Feb 24 20:23:48 2023 +0100
+++ b/src/Pure/Admin/build_status.scala	Fri Feb 24 20:40:50 2023 +0100
@@ -44,8 +44,8 @@
             List(
               Build_Log.Session_Status.finished.toString,
               Build_Log.Session_Status.failed.toString)) +
-          (if (only_sessions.isEmpty) ""
-           else " AND " + SQL.member(Build_Log.Data.session_name.ident, only_sessions)) +
+          if_proper(only_sessions,
+            " AND " + SQL.member(Build_Log.Data.session_name.ident, only_sessions)) +
           " AND " + SQL.enclose(sql))
     }
   }
@@ -206,7 +206,7 @@
     val body =
       proper_string(isabelle_version).map("Isabelle/" + _).toList :::
       (if (chapter == AFP.chapter) proper_string(afp_version).map("AFP/" + _) else None).toList
-    if (body.isEmpty) "" else body.mkString(" (", ", ", ")")
+    if_proper(body, body.mkString(" (", ", ", ")"))
   }
 
   def read_data(options: Options,

--- a/src/Pure/Admin/isabelle_cronjob.scala	Fri Feb 24 20:23:48 2023 +0100
+++ b/src/Pure/Admin/isabelle_cronjob.scala	Fri Feb 24 20:40:50 2023 +0100
@@ -157,7 +157,7 @@
     def sql: PostgreSQL.Source =
       Build_Log.Prop.build_engine.toString + " = " + SQL.string(Build_History.engine) + " AND " +
       SQL.member(Build_Log.Prop.build_host.ident, host :: more_hosts) +
-      (if (detect == "") "" else " AND " + SQL.enclose(detect))
+      if_proper(detect, " AND " + SQL.enclose(detect))
 
     def profile: Build_Status.Profile =
       Build_Status.Profile(description, history = history, afp = afp, bulky = bulky, sql = sql)

--- a/src/Pure/General/completion.scala	Fri Feb 24 20:23:48 2023 +0100
+++ b/src/Pure/General/completion.scala	Fri Feb 24 20:40:50 2023 +0100
@@ -60,7 +60,7 @@
     def load(): History = {
       def ignore_error(msg: String): Unit =
         Output.warning("Ignoring bad content of file " + COMPLETION_HISTORY +
-          (if (msg == "") "" else "\n" + msg))
+          if_proper(msg, "\n" + msg))
 
       val content =
         if (COMPLETION_HISTORY.is_file) {
@@ -139,9 +139,8 @@
     YXML.string_of_tree(Semantic.Info(pos, No_Completion))
 
   def report_names(pos: Position.T, names: List[(String, (String, String))], total: Int = 0): String =
-    if (names.isEmpty) ""
-    else
-      YXML.string_of_tree(Semantic.Info(pos, Names(if (total > 0) total else names.length, names)))
+    if_proper(names,
+      YXML.string_of_tree(Semantic.Info(pos, Names(if (total > 0) total else names.length, names))))
 
   def report_theories(pos: Position.T, thys: List[String], total: Int = 0): String =
     report_names(pos, thys.map(name => (name, (Markup.THEORY, name))), total)

--- a/src/Pure/General/json_api.scala	Fri Feb 24 20:23:48 2023 +0100
+++ b/src/Pure/General/json_api.scala	Fri Feb 24 20:40:50 2023 +0100
@@ -22,7 +22,7 @@
       HTTP.Client.get(if (route.isEmpty) url else new URL(url, route))
 
     def get_root(route: String = ""): Root =
-      Root(get(if (route.isEmpty) "" else "/" + route).json)
+      Root(get(if_proper(route, "/" + route)).json)
   }
 
   sealed case class Root(json: JSON.T) {

--- a/src/Pure/General/mailman.scala	Fri Feb 24 20:23:48 2023 +0100
+++ b/src/Pure/General/mailman.scala	Fri Feb 24 20:40:50 2023 +0100
@@ -541,7 +541,7 @@
 
     override def message_content(name: String, lines: List[String]): Message = {
       def err(msg: String = ""): Nothing =
-        error("Malformed message: " + name + (if (msg.isEmpty) "" else "\n" + msg))
+        error("Malformed message: " + name + if_proper(msg, "\n" + msg))
 
       val (head, body) =
         try { (Head.get(lines), make_body(Body.get(lines))) }
@@ -596,7 +596,7 @@
 
     override def message_content(name: String, lines: List[String]): Message = {
       def err(msg: String = ""): Nothing =
-        error("Malformed message: " + name + (if (msg.isEmpty) "" else "\n" + msg))
+        error("Malformed message: " + name + if_proper(msg, "\n" + msg))
 
       val (head, body) =
         try { (Head.get(lines), make_body(Body.get(lines))) }

--- a/src/Pure/General/mercurial.scala	Fri Feb 24 20:23:48 2023 +0100
+++ b/src/Pure/General/mercurial.scala	Fri Feb 24 20:40:50 2023 +0100
@@ -86,7 +86,7 @@
   /* command-line syntax */
 
   def optional(s: String, prefix: String = ""): String =
-    if (s == "") "" else " " + prefix + " " + Bash.string(s)
+    if_proper(s, " " + prefix + " " + Bash.string(s))
 
   def opt_flag(flag: String, b: Boolean): String = if (b) " " + flag else ""
   def opt_rev(s: String): String = optional(s, "--rev")

--- a/src/Pure/General/position.scala	Fri Feb 24 20:23:48 2023 +0100
+++ b/src/Pure/General/position.scala	Fri Feb 24 20:40:50 2023 +0100
@@ -116,18 +116,18 @@
 
   def here(props: T, delimited: Boolean = true): String = {
     val pos = props.filter(Markup.position_property)
-    if (pos.isEmpty) ""
-    else {
-      val s0 =
-        (Line.unapply(pos), File.unapply(pos)) match {
-          case (Some(i), None) => "line " + i.toString
-          case (Some(i), Some(name)) => "line " + i.toString + " of " + quote(name)
-          case (None, Some(name)) => "file " + quote(name)
-          case _ => ""
-        }
-      val s = if (s0 == "") s0 else if (delimited) " (" + s0 + ")" else s0
-      Markup(Markup.POSITION, pos).markup(s)
-    }
+    if_proper(pos,
+      {
+        val s0 =
+          (Line.unapply(pos), File.unapply(pos)) match {
+            case (Some(i), None) => "line " + i.toString
+            case (Some(i), Some(name)) => "line " + i.toString + " of " + quote(name)
+            case (None, Some(name)) => "file " + quote(name)
+            case _ => ""
+          }
+        val s = if (s0 == "") s0 else if (delimited) " (" + s0 + ")" else s0
+        Markup(Markup.POSITION, pos).markup(s)
+      })
   }
 
 

--- a/src/Pure/General/sql.scala	Fri Feb 24 20:23:48 2023 +0100
+++ b/src/Pure/General/sql.scala	Fri Feb 24 20:40:50 2023 +0100
@@ -171,18 +171,16 @@
 
     def insert_cmd(cmd: Source = "INSERT", sql: Source = ""): Source =
       cmd + " INTO " + ident + " VALUES " + enclosure(columns.map(_ => "?")) +
-        (if (sql == "") "" else " " + sql)
+        if_proper(sql, " " + sql)
 
     def insert(sql: Source = ""): Source = insert_cmd(sql = sql)
 
     def delete(sql: Source = ""): Source =
-      "DELETE FROM " + ident +
-        (if (sql == "") "" else " " + sql)
+      "DELETE FROM " + ident + if_proper(sql, " " + sql)
 
     def select(
         select_columns: List[Column] = Nil, sql: Source = "", distinct: Boolean = false): Source =
-      SQL.select(select_columns, distinct = distinct) + ident +
-        (if (sql == "") "" else " " + sql)
+      SQL.select(select_columns, distinct = distinct) + ident + if_proper(sql, " " + sql)
 
     override def toString: Source = ident
   }
@@ -366,8 +364,7 @@
     }
 
     def create_table(table: Table, strict: Boolean = false, sql: Source = ""): Unit =
-      using_statement(
-        table.create(strict, sql_type) + (if (sql == "") "" else " " + sql))(_.execute())
+      using_statement(table.create(strict, sql_type) + if_proper(sql, " " + sql))(_.execute())
 
     def create_index(table: Table, name: String, columns: List[Column],
         strict: Boolean = false, unique: Boolean = false): Unit =
@@ -500,7 +497,7 @@
     }
 
     def insert_permissive(table: SQL.Table, sql: SQL.Source = ""): SQL.Source =
-      table.insert_cmd(sql = sql + (if (sql == "") "" else " ") + "ON CONFLICT DO NOTHING")
+      table.insert_cmd(sql = sql + if_proper(sql, " ") + "ON CONFLICT DO NOTHING")
 
 
     /* notifications: IPC via database server */
@@ -514,8 +511,7 @@
 
     def notify(name: String, payload: String = ""): Unit =
       using_statement(
-        "NOTIFY " + SQL.ident(name) +
-          (if (payload.isEmpty) "" else ", " + SQL.string(payload)))(_.execute())
+        "NOTIFY " + SQL.ident(name) + if_proper(payload, ", " + SQL.string(payload)))(_.execute())
 
     def get_notifications(): List[PGNotification] =
       the_postgresql_connection.getNotifications() match {

--- a/src/Pure/General/timing.scala	Fri Feb 24 20:23:48 2023 +0100
+++ b/src/Pure/General/timing.scala	Fri Feb 24 20:40:50 2023 +0100
@@ -26,7 +26,7 @@
       val timing = stop - start
       if (timing.is_relevant) {
         val msg = if (message == null) null else message(result)
-        output((if (msg == null || msg == "") "" else msg + ": ") + timing.message + " elapsed time")
+        output(if_proper(msg, msg + ": ") + timing.message + " elapsed time")
       }
 
       Exn.release(result)

--- a/src/Pure/Isar/keyword.scala	Fri Feb 24 20:23:48 2023 +0100
+++ b/src/Pure/Isar/keyword.scala	Fri Feb 24 20:40:50 2023 +0100
@@ -114,8 +114,8 @@
   ) {
     override def toString: String =
       kind +
-        (if (load_command.isEmpty) "" else " (" + quote(load_command) + ")") +
-        (if (tags.isEmpty) "" else tags.map(quote).mkString(" % ", " % ", ""))
+        if_proper(load_command, " (" + quote(load_command) + ")") +
+        if_proper(tags, tags.map(quote).mkString(" % ", " % ", ""))
 
     def map(f: String => String): Spec =
       copy(kind = f(kind), load_command = f(load_command), tags = tags.map(f))
@@ -137,9 +137,7 @@
               case Some(load_command) => " (" + quote(load_command) + ")"
               case None => ""
             }
-          val kind_decl =
-            if (kind == "") ""
-            else " :: " + quote(kind) + load_decl
+          val kind_decl = if_proper(kind, " :: " + quote(kind) + load_decl)
           quote(name) + kind_decl
         }
       entries.mkString("keywords\n  ", " and\n  ", "")

--- a/src/Pure/ML/ml_statistics.scala	Fri Feb 24 20:23:48 2023 +0100
+++ b/src/Pure/ML/ml_statistics.scala	Fri Feb 24 20:40:50 2023 +0100
@@ -59,7 +59,7 @@
     }
 
     val env_prefix =
-      if (stats_dir.isEmpty) "" else "export POLYSTATSDIR=" + Bash.string(stats_dir) + "\n"
+      if_proper(stats_dir, "export POLYSTATSDIR=" + Bash.string(stats_dir) + "\n")
 
     Bash.process(env_prefix + "\"$POLYML_EXE\" -q --use src/Pure/ML/ml_statistics.ML --eval " +
         Bash.string("ML_Statistics.monitor " + ML_Syntax.print_long(pid) + " " +

--- a/src/Pure/PIDE/resources.scala	Fri Feb 24 20:23:48 2023 +0100
+++ b/src/Pure/PIDE/resources.scala	Fri Feb 24 20:40:50 2023 +0100
@@ -308,8 +308,7 @@
       "Cyclic dependency of " + show_path(names)
 
     private def required_by(initiators: List[Document.Node.Name]): String =
-      if (initiators.isEmpty) ""
-      else "\n(required by " + show_path(initiators.reverse) + ")"
+      if_proper(initiators, "\n(required by " + show_path(initiators.reverse) + ")")
   }
 
   final class Dependencies[A] private(

--- a/src/Pure/System/isabelle_process.scala	Fri Feb 24 20:23:48 2023 +0100
+++ b/src/Pure/System/isabelle_process.scala	Fri Feb 24 20:40:50 2023 +0100
@@ -58,7 +58,7 @@
       case Session.Terminated(result) =>
         if (!result.ok && !startup.is_finished) {
           val syslog = session.syslog.content()
-          val err = "Session startup failed" + (if (syslog.isEmpty) "" else ":\n" + syslog)
+          val err = "Session startup failed" + if_proper(syslog, ":\n" + syslog)
           startup.fulfill(err)
         }
         terminated.fulfill(result)

--- a/src/Pure/Thy/bibtex.scala	Fri Feb 24 20:23:48 2023 +0100
+++ b/src/Pure/Thy/bibtex.scala	Fri Feb 24 20:40:50 2023 +0100
@@ -813,7 +813,7 @@
 
   def cite_antiquotation(name: String, location: String, citations: List[String]): String = {
     val body =
-      (if (location.isEmpty) "" else Symbol.cartouche(location) + " in ") +
+      if_proper(location, Symbol.cartouche(location) + " in ") +
       citations.map(quote).mkString(" and ")
     cite_antiquotation(name, body)
   }

--- a/src/Pure/Thy/document_build.scala	Fri Feb 24 20:23:48 2023 +0100
+++ b/src/Pure/Thy/document_build.scala	Fri Feb 24 20:40:50 2023 +0100
@@ -357,7 +357,7 @@
       "then\n" +
       "  " + (if (title.nonEmpty) program_running_script(title) else "") +
         exe + " " + root_name_script() + "\n" +
-      (if (after.isEmpty) "" else "  " + after) +
+      if_proper(after, "  " + after) +
       "fi\n"
     }
 

--- a/src/Pure/Thy/latex.scala	Fri Feb 24 20:23:48 2023 +0100
+++ b/src/Pure/Thy/latex.scala	Fri Feb 24 20:40:50 2023 +0100
@@ -231,14 +231,14 @@
     }
 
     def index_item(item: Index_Item.Value): String = {
-      val like = if (item.like.isEmpty) "" else index_escape(item.like) + "@"
+      val like = if_proper(item.like, index_escape(item.like) + "@")
       val text = index_escape(latex_output(item.text))
       like + text
     }
 
     def index_entry(entry: Index_Entry.Value): Text = {
       val items = entry.items.map(index_item).mkString("!")
-      val kind = if (entry.kind.isEmpty) "" else "|" + index_escape(entry.kind)
+      val kind = if_proper(entry.kind, "|" + index_escape(entry.kind))
       latex_macro("index", XML.string(items + kind))
     }
 

--- a/src/Pure/Thy/sessions.scala	Fri Feb 24 20:23:48 2023 +0100
+++ b/src/Pure/Thy/sessions.scala	Fri Feb 24 20:40:50 2023 +0100
@@ -339,9 +339,7 @@
             val resources = new Resources(session_background)
 
             if (verbose || list_files) {
-              val groups =
-                if (info.groups.isEmpty) ""
-                else info.groups.mkString(" (", " ", ")")
+              val groups = if_proper(info.groups, info.groups.mkString(" (", " ", ")"))
               progress.echo("Session " + info.chapter + "/" + session_name + groups)
             }
 

--- a/src/Pure/Tools/dump.scala	Fri Feb 24 20:23:48 2023 +0100
+++ b/src/Pure/Tools/dump.scala	Fri Feb 24 20:40:50 2023 +0100
@@ -353,7 +353,7 @@
             Output.clean_yxml(
               "FAILED theory " + bad.name +
                 (if (bad.status.consolidated) "" else ": " + bad.status.percentage + "% finished") +
-                (if (bad.errors.isEmpty) "" else bad.errors.mkString("\n", "\n", ""))))
+                if_proper(bad.errors, bad.errors.mkString("\n", "\n", ""))))
 
         val pending_msgs =
           use_theories_result.nodes_pending match {

--- a/src/Pure/Tools/phabricator.scala	Fri Feb 24 20:23:48 2023 +0100
+++ b/src/Pure/Tools/phabricator.scala	Fri Feb 24 20:40:50 2023 +0100
@@ -52,7 +52,7 @@
   val default_name = "vcs"
 
   def phabricator_name(name: String = "", ext: String = ""): String =
-    "phabricator" + (if (name.isEmpty) "" else "-" + name) + (if (ext.isEmpty) "" else "." + ext)
+    "phabricator" + if_proper(name, "-" + name) + if_proper(ext, "." + ext)
 
   def isabelle_phabricator_name(name: String = "", ext: String = ""): String =
     "isabelle-" + phabricator_name(name = name, ext = ext)

--- a/src/Pure/term.scala	Fri Feb 24 20:23:48 2023 +0100
+++ b/src/Pure/term.scala	Fri Feb 24 20:40:50 2023 +0100
@@ -41,21 +41,21 @@
 
     override def toString: String =
       if (this == dummyT) "_"
-      else "Type(" + name + (if (args.isEmpty) "" else "," + args) + ")"
+      else "Type(" + name + if_proper(args, "," + args) + ")"
   }
   case class TFree(name: String, sort: Sort = Nil) extends Typ {
     private lazy val hash: Int = ("TFree", name, sort).hashCode()
     override def hashCode(): Int = hash
 
     override def toString: String =
-      "TFree(" + name + (if (sort.isEmpty) "" else "," + sort) + ")"
+      "TFree(" + name + if_proper(sort, "," + sort) + ")"
   }
   case class TVar(name: Indexname, sort: Sort = Nil) extends Typ {
     private lazy val hash: Int = ("TVar", name, sort).hashCode()
     override def hashCode(): Int = hash
 
     override def toString: String =
-      "TVar(" + name + (if (sort.isEmpty) "" else "," + sort) + ")"
+      "TVar(" + name + if_proper(sort, "," + sort) + ")"
   }
   val dummyT: Type = Type("dummy")
 
@@ -72,7 +72,7 @@
 
     override def toString: String =
       if (this == dummy) "_"
-      else "Const(" + name + (if (typargs.isEmpty) "" else "," + typargs) + ")"
+      else "Const(" + name + if_proper(typargs, "," + typargs) + ")"
   }
   case class Free(name: String, typ: Typ = dummyT) extends Term {
     private lazy val hash: Int = ("Free", name, typ).hashCode()