# HG changeset patch
# User wenzelm
# Date 1585343195 -3600
# Node ID d5502ee7c1417bfeb3b97481f2bd1897422f23ce
# Parent  97ccf48c2f0c01924ffaa4f1a6fb6d82bff9c069
tuned;

diff -r 97ccf48c2f0c -r d5502ee7c141 src/Pure/Admin/build_fonts.scala
--- a/src/Pure/Admin/build_fonts.scala	Fri Mar 27 22:01:27 2020 +0100
+++ b/src/Pure/Admin/build_fonts.scala	Fri Mar 27 22:06:35 2020 +0100
@@ -284,7 +284,7 @@
       val domain =
         (for ((name, index) <- targets if index == 0)
           yield Fontforge.font_domain(target_dir + hinted_path(false) + name))
-        .flatten.toSet.toList.sorted
+        .flatten.distinct.sorted
 
       Fontforge.execute(
         Fontforge.commands(
diff -r 97ccf48c2f0c -r d5502ee7c141 src/Pure/Admin/build_jdk.scala
--- a/src/Pure/Admin/build_jdk.scala	Fri Mar 27 22:01:27 2020 +0100
+++ b/src/Pure/Admin/build_jdk.scala	Fri Mar 27 22:06:35 2020 +0100
@@ -144,7 +144,7 @@
         val extracted = archives.map(extract_archive(dir, _))
 
         val version =
-          extracted.map(_._1).toSet.toList match {
+          extracted.map(_._1).distinct match {
             case List(version) => version
             case Nil => error("No archives")
             case versions =>
diff -r 97ccf48c2f0c -r d5502ee7c141 src/Pure/Admin/jenkins.scala
--- a/src/Pure/Admin/jenkins.scala	Fri Mar 27 22:01:27 2020 +0100
+++ b/src/Pure/Admin/jenkins.scala	Fri Mar 27 22:06:35 2020 +0100
@@ -106,7 +106,7 @@
         Isabelle_System.mkdirs(log_dir)
 
         val ml_statistics =
-          session_logs.map(_._1).toSet.toList.sorted.flatMap(session_name =>
+          session_logs.map(_._1).distinct.sorted.flatMap(session_name =>
             read_ml_statistics(store, session_name).
               map(props => (Build_Log.SESSION_NAME -> session_name) :: props))
 
diff -r 97ccf48c2f0c -r d5502ee7c141 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Fri Mar 27 22:01:27 2020 +0100
+++ b/src/Pure/Thy/sessions.scala	Fri Mar 27 22:06:35 2020 +0100
@@ -271,7 +271,7 @@
                   if !ok(path.canonical_file)
                   path1 = File.relative_path(info.dir.canonical, path).getOrElse(path)
                 } yield (path1, name)).toList
-              val bad_dirs = (for { (path1, _) <- bad } yield path1.toString).toSet.toList.sorted
+              val bad_dirs = (for { (path1, _) <- bad } yield path1.toString).distinct.sorted
 
               val errs1 =
                 for { (path1, name) <- bad }