# HG changeset patch
# User wenzelm
# Date 1621252100 -7200
# Node ID d95d34efbe6f79c35c77fd1dc69cd53dff213a03
# Parent  3eba8d4b624beb9f80edadeadbd2daacae6f5c0a
tuned;

diff -r 3eba8d4b624b -r d95d34efbe6f src/Pure/Admin/build_log.scala
--- a/src/Pure/Admin/build_log.scala	Mon May 17 13:40:01 2021 +0200
+++ b/src/Pure/Admin/build_log.scala	Mon May 17 13:48:20 2021 +0200
@@ -62,8 +62,8 @@
       def unapply(s: String): Option[Entry] =
         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))
+      def getenv(a: String): String =
+        Properties.Eq(a -> quote(Isabelle_System.getenv(a)))
     }
 
     def show(): String =
@@ -227,10 +227,7 @@
     /* settings */
 
     def get_setting(a: String): Option[Settings.Entry] =
-      lines.find(_.startsWith(a + "=")) match {
-        case Some(line) => Settings.Entry.unapply(line)
-        case None => None
-      }
+      lines.collectFirst({ case Settings.Entry(entry) if entry._1 == a => entry })
 
     def get_all_settings: Settings.T =
       for { c <- Settings.all_settings; entry <- get_setting(c.name) }