# HG changeset patch # User wenzelm # Date 1677942950 -3600 # Node ID fd40e36045fd777c0b60489b330ac7ab6ee859d5 # Parent daf632e9ce7e56a5a5272e890940ba38fed41e1d tuned; diff -r daf632e9ce7e -r fd40e36045fd src/Pure/System/isabelle_system.scala --- 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 diff -r daf632e9ce7e -r fd40e36045fd src/Pure/System/options.scala --- 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) diff -r daf632e9ce7e -r fd40e36045fd src/Pure/System/progress.scala --- 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 + "%" } diff -r daf632e9ce7e -r fd40e36045fd src/Pure/Tools/build_docker.scala --- 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 } diff -r daf632e9ce7e -r fd40e36045fd src/Tools/jEdit/jedit_main/isabelle_sidekick.scala --- 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.output(kind) + "" + - (if (name == "") "" else " " + HTML.output(name)) + "" + if_proper(name, " " + HTML.output(name)) + "" val range = Text.Range(offset, offset + source.length) val asset = new Asset(label, label_html, range, source) data.root.add(new DefaultMutableTreeNode(asset))