clarified operations: uniform sorting of results;

--- 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 *)

--- 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(

--- 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(