# HG changeset patch
# User sultana
# Date 1378241200 -3600
# Node ID 51b562922cb17fbce407ffba3782e1806505f457
# Parent  74cee48bccd667f401f40a84743d17ba38323e7e
get_file_list now returns files sorted by size;

diff -r 74cee48bccd6 -r 51b562922cb1 src/HOL/TPTP/TPTP_Parser/tptp_syntax.ML
--- a/src/HOL/TPTP/TPTP_Parser/tptp_syntax.ML	Tue Sep 03 21:46:40 2013 +0100
+++ b/src/HOL/TPTP/TPTP_Parser/tptp_syntax.ML	Tue Sep 03 21:46:40 2013 +0100
@@ -294,27 +294,38 @@
    |  Include (position, _, _) => position
 
 (*Used for debugging. Returns all files contained within a directory or its
-subdirectories. Follows symbolic links, filters away directories.*)
+subdirectories. Follows symbolic links, filters away directories.
+Files are ordered by size*)
 fun get_file_list path =
   let
-    fun check_file_entry f rest =
-      let
-        (*NOTE needed since no File.is_link and File.read_link*)
-        val f_str = Path.implode f
-      in
-        if File.is_dir f then
-          rest @ get_file_list f
-        else if OS.FileSys.isLink f_str then
-          (*follow links -- NOTE this breaks if links are relative paths*)
-          check_file_entry (Path.explode (OS.FileSys.readLink f_str)) rest
-        else f :: rest
-      end
+    fun get_file_list' acc paths =
+      case paths of
+          [] => acc
+        | (f :: fs) =>
+            let
+              (*NOTE needed since no File.is_link and File.read_link*)
+              val f_str = Path.implode f
+            in
+              if File.is_dir f then
+                let
+                  val contents =
+                    File.read_dir f
+                    |> map
+                        (Path.explode
+                        #> Path.append f)
+                in
+                  get_file_list' acc (fs @ contents)
+                end
+              else if OS.FileSys.isLink f_str then
+                (*follow links -- NOTE this breaks if links are relative paths*)
+                get_file_list' acc (Path.explode (OS.FileSys.readLink f_str) :: fs)
+              else
+                get_file_list' ((f, OS.FileSys.fileSize f_str) :: acc) fs
+            end
   in
-    File.read_dir path
-    |> map
-        (Path.explode
-        #> Path.append path)
-    |> (fn l => fold check_file_entry l [])
+    get_file_list' [] [path]
+    |> sort (fn ((_, n1), (_, n2)) => Int.compare (n1, n2))
+    |> map fst
   end
 
 fun role_to_string role =