1.1 --- a/src/HOL/TPTP/TPTP_Parser/tptp_syntax.ML	Tue Sep 03 21:46:40 2013 +0100
     1.2 +++ b/src/HOL/TPTP/TPTP_Parser/tptp_syntax.ML	Tue Sep 03 21:46:40 2013 +0100
     1.3 @@ -294,27 +294,38 @@
     1.4     |  Include (position, _, _) => position
     1.5  
     1.6  (*Used for debugging. Returns all files contained within a directory or its
     1.7 -subdirectories. Follows symbolic links, filters away directories.*)
     1.8 +subdirectories. Follows symbolic links, filters away directories.
     1.9 +Files are ordered by size*)
    1.10  fun get_file_list path =
    1.11    let
    1.12 -    fun check_file_entry f rest =
    1.13 -      let
    1.14 -        (*NOTE needed since no File.is_link and File.read_link*)
    1.15 -        val f_str = Path.implode f
    1.16 -      in
    1.17 -        if File.is_dir f then
    1.18 -          rest @ get_file_list f
    1.19 -        else if OS.FileSys.isLink f_str then
    1.20 -          (*follow links -- NOTE this breaks if links are relative paths*)
    1.21 -          check_file_entry (Path.explode (OS.FileSys.readLink f_str)) rest
    1.22 -        else f :: rest
    1.23 -      end
    1.24 +    fun get_file_list' acc paths =
    1.25 +      case paths of
    1.26 +          [] => acc
    1.27 +        | (f :: fs) =>
    1.28 +            let
    1.29 +              (*NOTE needed since no File.is_link and File.read_link*)
    1.30 +              val f_str = Path.implode f
    1.31 +            in
    1.32 +              if File.is_dir f then
    1.33 +                let
    1.34 +                  val contents =
    1.35 +                    File.read_dir f
    1.36 +                    |> map
    1.37 +                        (Path.explode
    1.38 +                        #> Path.append f)
    1.39 +                in
    1.40 +                  get_file_list' acc (fs @ contents)
    1.41 +                end
    1.42 +              else if OS.FileSys.isLink f_str then
    1.43 +                (*follow links -- NOTE this breaks if links are relative paths*)
    1.44 +                get_file_list' acc (Path.explode (OS.FileSys.readLink f_str) :: fs)
    1.45 +              else
    1.46 +                get_file_list' ((f, OS.FileSys.fileSize f_str) :: acc) fs
    1.47 +            end
    1.48    in
    1.49 -    File.read_dir path
    1.50 -    |> map
    1.51 -        (Path.explode
    1.52 -        #> Path.append path)
    1.53 -    |> (fn l => fold check_file_entry l [])
    1.54 +    get_file_list' [] [path]
    1.55 +    |> sort (fn ((_, n1), (_, n2)) => Int.compare (n1, n2))
    1.56 +    |> map fst
    1.57    end
    1.58  
    1.59  fun role_to_string role =