--- a/src/Pure/System/isabelle_system.scala Sat Mar 04 12:59:22 2023 +0100
+++ b/src/Pure/System/isabelle_system.scala Sat Mar 04 16:15:50 2023 +0100
@@ -296,7 +296,7 @@
base_dir: JFile = isabelle_tmp_prefix(),
initialized: Boolean = true
): JFile = {
- val suffix = if (ext == "") "" else "." + ext
+ val suffix = if_proper(ext, "." + ext)
val file = Files.createTempFile(base_dir.toPath, name, suffix).toFile
if (initialized) file.deleteOnExit() else file.delete()
file
--- a/src/Pure/System/options.scala Sat Mar 04 12:59:22 2023 +0100
+++ b/src/Pure/System/options.scala Sat Mar 04 16:15:50 2023 +0100
@@ -64,7 +64,7 @@
private def print(default: Boolean): String = {
val x = if (default) default_value else value
"option " + name + " : " + typ.print + " = " + print_value(x) + print_standard +
- (if (description == "") "" else "\n -- " + quote(description))
+ if_proper(description, "\n -- " + quote(description))
}
def print: String = print(false)
--- a/src/Pure/System/progress.scala Sat Mar 04 12:59:22 2023 +0100
+++ b/src/Pure/System/progress.scala Sat Mar 04 16:15:50 2023 +0100
@@ -28,7 +28,7 @@
def message: Message =
Message(Kind.writeln, print_session + print_theory + print_percentage)
- def print_session: String = if (session == "") "" else session + ": "
+ def print_session: String = if_proper(session, session + ": ")
def print_theory: String = "theory " + theory
def print_percentage: String =
percentage match { case None => "" case Some(p) => " " + p + "%" }
--- a/src/Pure/Tools/build_docker.scala Sat Mar 04 12:59:22 2023 +0100
+++ b/src/Pure/Tools/build_docker.scala Sat Mar 04 16:15:50 2023 +0100
@@ -104,7 +104,7 @@
}
val quiet_option = if (verbose) "" else " -q"
- val tag_option = if (tag == "") "" else " -t " + Bash.string(tag)
+ val tag_option = if_proper(tag, " -t " + Bash.string(tag))
progress.bash("docker build" + quiet_option + tag_option + " " + File.bash_path(tmp_dir),
echo = true).check
}
--- a/src/Tools/jEdit/jedit_main/isabelle_sidekick.scala Sat Mar 04 12:59:22 2023 +0100
+++ b/src/Tools/jEdit/jedit_main/isabelle_sidekick.scala Sat Mar 04 16:15:50 2023 +0100
@@ -278,10 +278,10 @@
val name = chunk.name
val source = chunk.source
if (kind != "") {
- val label = kind + (if (name == "") "" else " " + name)
+ val label = kind + if_proper(name, " " + name)
val label_html =
"<html><b>" + HTML.output(kind) + "</b>" +
- (if (name == "") "" else " " + HTML.output(name)) + "</html>"
+ if_proper(name, " " + HTML.output(name)) + "</html>"
val range = Text.Range(offset, offset + source.length)
val asset = new Asset(label, label_html, range, source)
data.root.add(new DefaultMutableTreeNode(asset))