# HG changeset patch # User wenzelm # Date 1621251601 -7200 # Node ID 3eba8d4b624beb9f80edadeadbd2daacae6f5c0a # Parent 5833b556b3b53a77cafec4c04c6d2e8175804505 clarified signature; diff -r 5833b556b3b5 -r 3eba8d4b624b src/Pure/Admin/build_csdp.scala --- a/src/Pure/Admin/build_csdp.scala Mon May 17 13:37:47 2021 +0200 +++ b/src/Pure/Admin/build_csdp.scala Mon May 17 13:40:01 2021 +0200 @@ -23,13 +23,13 @@ def print: Option[String] = if (changed.isEmpty) None else - Some(" * " + platform + ":\n" + changed.map(p => " " + p._1 + "=" + p._2) + Some(" * " + platform + ":\n" + changed.map(p => " " + Properties.Eq(p)) .mkString("\n")) def change(path: Path): Unit = { def change_line(line: String, entry: (String, String)): String = - line.replaceAll(entry._1 + "=.*", entry._1 + "=" + entry._2) + line.replaceAll(entry._1 + "=.*", Properties.Eq(entry)) File.change(path, s => split_lines(s).map(line => changed.foldLeft(line)(change_line)).mkString("\n")) } diff -r 5833b556b3b5 -r 3eba8d4b624b src/Pure/Admin/build_log.scala --- a/src/Pure/Admin/build_log.scala Mon May 17 13:37:47 2021 +0200 +++ b/src/Pure/Admin/build_log.scala Mon May 17 13:40:01 2021 +0200 @@ -60,14 +60,9 @@ object Entry { def unapply(s: String): Option[Entry] = - s.indexOf('=') match { - case -1 => None - case i => - val a = s.substring(0, i) - val b = Library.perhaps_unquote(s.substring(i + 1)) - Some((a, b)) - } - def apply(a: String, b: String): String = a + "=" + quote(b) + for { (a, b) <- Properties.Eq.unapply(s) } + yield (a, Library.perhaps_unquote(b)) + def apply(a: String, b: String): String = Properties.Eq(a -> quote(b)) def getenv(a: String): String = apply(a, Isabelle_System.getenv(a)) } diff -r 5833b556b3b5 -r 3eba8d4b624b src/Pure/General/path.scala --- a/src/Pure/General/path.scala Mon May 17 13:37:47 2021 +0200 +++ b/src/Pure/General/path.scala Mon May 17 13:40:01 2021 +0200 @@ -263,7 +263,7 @@ case Path.Variable(s) => val path = Path.explode(Isabelle_System.getenv_strict(s, env)) if (path.elems.exists(_.isInstanceOf[Path.Variable])) - error("Illegal path variable nesting: " + s + "=" + path.toString) + error("Illegal path variable nesting: " + Properties.Eq(s -> path.toString)) else path.elems case x => List(x) } diff -r 5833b556b3b5 -r 3eba8d4b624b src/Pure/General/properties.scala --- a/src/Pure/General/properties.scala Mon May 17 13:37:47 2021 +0200 +++ b/src/Pure/General/properties.scala Mon May 17 13:40:01 2021 +0200 @@ -14,6 +14,17 @@ type Entry = (java.lang.String, java.lang.String) type T = List[Entry] + object Eq + { + def apply(entry: Entry): java.lang.String = entry._1 + "=" + entry._2 + + def unapply(str: java.lang.String): Option[Entry] = + { + val i = str.indexOf('=') + if (i <= 0) None else Some((str.substring(0, i), str.substring(i + 1))) + } + } + def defined(props: T, name: java.lang.String): java.lang.Boolean = props.exists({ case (x, _) => x == name }) diff -r 5833b556b3b5 -r 3eba8d4b624b src/Pure/PIDE/prover.scala --- a/src/Pure/PIDE/prover.scala Mon May 17 13:37:47 2021 +0200 +++ b/src/Pure/PIDE/prover.scala Mon May 17 13:40:01 2021 +0200 @@ -50,7 +50,7 @@ kind + " [[" + res + "]]" else kind + " " + - (for ((x, y) <- properties) yield x + "=" + y).mkString("{", ",", "}") + " [[" + res + "]]" + (properties.map(Properties.Eq.apply)).mkString("{", ",", "}") + " [[" + res + "]]" } } diff -r 5833b556b3b5 -r 3eba8d4b624b src/Pure/PIDE/yxml.scala --- a/src/Pure/PIDE/yxml.scala Mon May 17 13:37:47 2021 +0200 +++ b/src/Pure/PIDE/yxml.scala Mon May 17 13:40:01 2021 +0200 @@ -71,12 +71,7 @@ else err("unbalanced element " + quote(name)) private def parse_attrib(source: CharSequence): (String, String) = - { - val s = source.toString - val i = s.indexOf('=') - if (i <= 0) err_attribute() - (s.substring(0, i), s.substring(i + 1)) - } + Properties.Eq.unapply(source.toString) getOrElse err_attribute() def parse_body(source: CharSequence, cache: XML.Cache = XML.Cache.none): XML.Body = diff -r 5833b556b3b5 -r 3eba8d4b624b src/Pure/System/options.scala --- a/src/Pure/System/options.scala Mon May 17 13:37:47 2021 +0200 +++ b/src/Pure/System/options.scala Mon May 17 13:40:01 2021 +0200 @@ -355,12 +355,10 @@ } def + (str: String): Options = - { - str.indexOf('=') match { - case -1 => this + (str, None) - case i => this + (str.substring(0, i), str.substring(i + 1)) + str match { + case Properties.Eq((a, b)) => this + (a, b) + case _ => this + (str, None) } - } def ++ (specs: List[Options.Spec]): Options = specs.foldLeft(this) { case (x, (y, z)) => x + (y, z) } diff -r 5833b556b3b5 -r 3eba8d4b624b src/Tools/jEdit/src/keymap_merge.scala --- a/src/Tools/jEdit/src/keymap_merge.scala Mon May 17 13:37:47 2021 +0200 +++ b/src/Tools/jEdit/src/keymap_merge.scala Mon May 17 13:40:01 2021 +0200 @@ -30,7 +30,7 @@ class Shortcut(val property: String, val binding: String) { - override def toString: String = property + "=" + binding + override def toString: String = Properties.Eq(property -> binding) def primary: Boolean = property.endsWith(".shortcut")