# HG changeset patch
# User wenzelm
# Date 1621253271 -7200
# Node ID bf51c23f3f99e839c2595d13910b7bbd2b891291
# Parent  e7deaadc5eab48431b3ef84e14f6bf7cb41a0305
clarified signature -- avoid odd warning about scala/bug#6675;

diff -r e7deaadc5eab -r bf51c23f3f99 src/Pure/Admin/build_log.scala
--- a/src/Pure/Admin/build_log.scala	Mon May 17 14:07:13 2021 +0200
+++ b/src/Pure/Admin/build_log.scala	Mon May 17 14:07:51 2021 +0200
@@ -63,7 +63,7 @@
         for { (a, b) <- Properties.Eq.unapply(s) }
         yield (a, Library.perhaps_unquote(b))
       def getenv(a: String): String =
-        Properties.Eq(a -> quote(Isabelle_System.getenv(a)))
+        Properties.Eq(a, quote(Isabelle_System.getenv(a)))
     }
 
     def show(): String =
@@ -226,8 +226,8 @@
 
     /* settings */
 
-    def get_setting(a: String): Option[Settings.Entry] =
-      lines.collectFirst({ case Settings.Entry(entry) if entry._1 == a => entry })
+    def get_setting(name: String): Option[Settings.Entry] =
+      lines.collectFirst({ case Settings.Entry(a, b) if a == name => a -> b })
 
     def get_all_settings: Settings.T =
       for { c <- Settings.all_settings; entry <- get_setting(c.name) }
diff -r e7deaadc5eab -r bf51c23f3f99 src/Pure/General/path.scala
--- a/src/Pure/General/path.scala	Mon May 17 14:07:13 2021 +0200
+++ b/src/Pure/General/path.scala	Mon May 17 14:07:51 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: " + Properties.Eq(s -> path.toString))
+            error("Illegal path variable nesting: " + Properties.Eq(s, path.toString))
           else path.elems
         case x => List(x)
       }
diff -r e7deaadc5eab -r bf51c23f3f99 src/Pure/General/properties.scala
--- a/src/Pure/General/properties.scala	Mon May 17 14:07:13 2021 +0200
+++ b/src/Pure/General/properties.scala	Mon May 17 14:07:51 2021 +0200
@@ -16,7 +16,8 @@
 
   object Eq
   {
-    def apply(entry: Entry): java.lang.String = entry._1 + "=" + entry._2
+    def apply(a: java.lang.String, b: java.lang.String): java.lang.String = a + "=" + b
+    def apply(entry: Entry): java.lang.String = apply(entry._1, entry._2)
 
     def unapply(str: java.lang.String): Option[Entry] =
     {
diff -r e7deaadc5eab -r bf51c23f3f99 src/Pure/System/options.scala
--- a/src/Pure/System/options.scala	Mon May 17 14:07:13 2021 +0200
+++ b/src/Pure/System/options.scala	Mon May 17 14:07:51 2021 +0200
@@ -356,7 +356,7 @@
 
   def + (str: String): Options =
     str match {
-      case Properties.Eq((a, b)) => this + (a, b)
+      case Properties.Eq(a, b) => this + (a, b)
       case _ => this + (str, None)
     }
 
diff -r e7deaadc5eab -r bf51c23f3f99 src/Tools/jEdit/src/keymap_merge.scala
--- a/src/Tools/jEdit/src/keymap_merge.scala	Mon May 17 14:07:13 2021 +0200
+++ b/src/Tools/jEdit/src/keymap_merge.scala	Mon May 17 14:07:51 2021 +0200
@@ -30,7 +30,7 @@
 
   class Shortcut(val property: String, val binding: String)
   {
-    override def toString: String = Properties.Eq(property -> binding)
+    override def toString: String = Properties.Eq(property, binding)
 
     def primary: Boolean = property.endsWith(".shortcut")