# HG changeset patch
# User wenzelm
# Date 1677268355 -3600
# Node ID df17355f1e2c8fe0a999c1a7d813bbc4bd2e9e80
# Parent  7c57d9586f4c70207dca37ccc53bd4a0287a8133
tuned;

diff -r 7c57d9586f4c -r df17355f1e2c src/Pure/Admin/build_scala.scala
--- a/src/Pure/Admin/build_scala.scala	Fri Feb 24 20:40:50 2023 +0100
+++ b/src/Pure/Admin/build_scala.scala	Fri Feb 24 20:52:35 2023 +0100
@@ -29,8 +29,7 @@
       Isabelle_System.download_file(proper_url, path, progress = progress)
 
     def print: String =
-      "  * " + name + " " + version +
-        (if (base_version.nonEmpty) " for Scala " + base_version else "") +
+      "  * " + name + " " + version + if_proper(base_version, " for Scala " + base_version) +
         ":\n    " + make_url(url)
   }
 
diff -r 7c57d9586f4c -r df17355f1e2c src/Pure/General/mailman.scala
--- a/src/Pure/General/mailman.scala	Fri Feb 24 20:40:50 2023 +0100
+++ b/src/Pure/General/mailman.scala	Fri Feb 24 20:52:35 2023 +0100
@@ -453,9 +453,7 @@
 
     def get(lines: List[String]): List[String] =
       unapply(lines) getOrElse
-        error("Missing delimiters:" +
-          (if (bg.nonEmpty) " " else "") + bg +
-          (if (en.nonEmpty) " " else "") + en)
+        error("Missing delimiters:" + if_proper(bg, " ") + bg + if_proper(en, " ") + en)
   }
 
 
diff -r 7c57d9586f4c -r df17355f1e2c src/Pure/General/rsync.scala
--- a/src/Pure/General/rsync.scala	Fri Feb 24 20:40:50 2023 +0100
+++ b/src/Pure/General/rsync.scala	Fri Feb 24 20:52:35 2023 +0100
@@ -42,7 +42,7 @@
         (if (clean) " --delete-excluded" else "") +
         (if (list) " --list-only --no-human-readable" else "") +
         filter.map(s => " --filter=" + Bash.string(s)).mkString +
-        (if (args.nonEmpty) " " + Bash.strings(args) else "")
+        if_proper(args, " " + Bash.strings(args))
     context.progress.bash(script, echo = true)
   }
 
diff -r 7c57d9586f4c -r df17355f1e2c src/Pure/General/ssh.scala
--- a/src/Pure/General/ssh.scala	Fri Feb 24 20:40:50 2023 +0100
+++ b/src/Pure/General/ssh.scala	Fri Feb 24 20:52:35 2023 +0100
@@ -19,7 +19,7 @@
     if (control_path.isEmpty || control_path == Bash.string(control_path)) {
       "ssh" +
         (if (port > 0) " -p " + port else "") +
-        (if (control_path.nonEmpty) " -o ControlPath=" + control_path else "")
+        if_proper(control_path, " -o ControlPath=" + control_path)
     }
     else error ("Malformed SSH control socket: " + quote(control_path))
 
@@ -130,8 +130,8 @@
           control_master = master, control_path = control_path)
       val cmd =
         Config.command(command, config) +
-        (if (opts.nonEmpty) " " + opts else "") +
-        (if (args.nonEmpty) " -- " + args else "")
+        if_proper(opts, " " + opts) +
+        if_proper(args, " -- " + args)
       Isabelle_System.bash(cmd, cwd = cwd,
         redirect = redirect,
         progress_stdout = progress_stdout,
@@ -155,7 +155,7 @@
     }
 
     def run_ssh(master: Boolean = false, opts: String = "", args: String = ""): Process_Result = {
-      val args1 = Bash.string(host) + (if (args.nonEmpty) " " + args else "")
+      val args1 = Bash.string(host) + if_proper(args, " " + args)
       run_command("ssh", master = master, opts = opts, args = args1)
     }
 
diff -r 7c57d9586f4c -r df17355f1e2c src/Pure/Thy/bibtex.scala
--- a/src/Pure/Thy/bibtex.scala	Fri Feb 24 20:40:50 2023 +0100
+++ b/src/Pure/Thy/bibtex.scala	Fri Feb 24 20:52:35 2023 +0100
@@ -680,7 +680,7 @@
         "\"$BIB2XHTML_HOME/main/bib2xhtml.pl\" -B \"$ISABELLE_BIBTEX\"" +
           " -u -s " + Bash.string(proper_string(style) getOrElse "empty") +
           (if (chronological) " -c" else "") +
-          (if (title != "") " -h " + Bash.string(title) + " " else "") +
+          if_proper(title, " -h " + Bash.string(title) + " ") +
           " " + File.bash_path(in_file) + " " + File.bash_path(out_file),
         cwd = tmp_dir.file).check
 
diff -r 7c57d9586f4c -r df17355f1e2c src/Pure/Tools/dotnet_setup.scala
--- a/src/Pure/Tools/dotnet_setup.scala	Fri Feb 24 20:40:50 2023 +0100
+++ b/src/Pure/Tools/dotnet_setup.scala	Fri Feb 24 20:52:35 2023 +0100
@@ -128,9 +128,9 @@
           if (platform_dir.is_dir && force) Isabelle_System.rm_tree(platform_dir)
           val script =
             platform.exec + " " + File.bash_platform_path(install) +
-              (if (version.nonEmpty) " -Version " + Bash.string(version) else "") +
+              if_proper(version, " -Version " + Bash.string(version)) +
               " -Architecture " + Bash.string(platform.arch) +
-              (if (platform.os.nonEmpty) " -OS " + Bash.string(platform.os) else "") +
+              if_proper(platform.os, " -OS " + Bash.string(platform.os)) +
               " -InstallDir " + Bash.string(platform.name) +
               (if (dry_run) " -DryRun" else "") +
               " -NoPath"
diff -r 7c57d9586f4c -r df17355f1e2c src/Pure/Tools/phabricator.scala
--- a/src/Pure/Tools/phabricator.scala	Fri Feb 24 20:40:50 2023 +0100
+++ b/src/Pure/Tools/phabricator.scala	Fri Feb 24 20:52:35 2023 +0100
@@ -81,7 +81,7 @@
     body: String = "",
     exit: String = ""): String = {
 """#!/bin/bash
-""" + (if (init.nonEmpty) "\n" + init else "") + """
+""" + if_proper(init, "\n" + init) + """
 {
   while { unset REPLY; read -r; test "$?" = 0 -o -n "$REPLY"; }
   do
@@ -92,7 +92,7 @@
     } < /dev/null
   done
 } < """ + File.bash_path(global_config) + "\n" +
-    (if (exit.nonEmpty) "\n" + exit + "\n" else "")
+    if_proper(exit, "\n" + exit + "\n")
   }
 
   sealed case class Config(name: String, root: Path) {