# 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")