# 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 =