# HG changeset patch
# User wenzelm
# Date 1544300027 -3600
# Node ID ff2f39a221d4f71cc75e16d577263a729889d74f
# Parent  91f46633bb4effe6cb1a23bcbd5f347c7c7c0857
clarified operations: uniform sorting of results;

diff -r 91f46633bb4e -r ff2f39a221d4 src/Pure/General/file.ML
--- a/src/Pure/General/file.ML	Sat Dec 08 15:13:28 2018 +0100
+++ b/src/Pure/General/file.ML	Sat Dec 08 21:13:47 2018 +0100
@@ -117,7 +117,7 @@
         | SOME entry => read (f entry x));
     in read a end);
 
-fun read_dir path = rev (fold_dir cons path []);
+fun read_dir path = sort_strings (fold_dir cons path []);
 
 
 (* input *)
diff -r 91f46633bb4e -r ff2f39a221d4 src/Pure/General/file.scala
--- a/src/Pure/General/file.scala	Sat Dec 08 15:13:28 2018 +0100
+++ b/src/Pure/General/file.scala	Sat Dec 08 21:13:47 2018 +0100
@@ -144,7 +144,7 @@
     if (!dir.is_dir) error("No such directory: " + dir.toString)
     val files = dir.file.listFiles
     if (files == null) Nil
-    else files.toList.map(_.getName)
+    else files.toList.map(_.getName).sorted
   }
 
   def find_files(
diff -r 91f46633bb4e -r ff2f39a221d4 src/Pure/General/ssh.scala
--- a/src/Pure/General/ssh.scala	Sat Dec 08 15:13:28 2018 +0100
+++ b/src/Pure/General/ssh.scala	Sat Dec 08 21:13:47 2018 +0100
@@ -381,7 +381,7 @@
             catch { case _: SftpException => false }
           }
           else attrs.isDir)
-      }).toList
+      }).toList.sortBy(_.name)
     }
 
     def find_files(