# HG changeset patch
# User sultana
# Date 1392825422 0
# Node ID 2e2e9bc7c4c6a3038f3971afe7ec072ffdc00f6d
# Parent  eb291b215c730bb858e7d3967c29898151ce6d89
made list of test files a parameter to timed_test in TPTP_Test.thy, and updated dependent definitions;

diff -r eb291b215c73 -r 2e2e9bc7c4c6 src/HOL/TPTP/TPTP_Interpret_Test.thy
--- a/src/HOL/TPTP/TPTP_Interpret_Test.thy	Wed Feb 19 15:57:02 2014 +0000
+++ b/src/HOL/TPTP/TPTP_Interpret_Test.thy	Wed Feb 19 15:57:02 2014 +0000
@@ -154,7 +154,7 @@
 ML {*
   if test_all @{context} then
     (report @{context} "Interpreting all problems";
-     S timed_test (interpretation_test (get_timeout @{context})) @{context})
+     S timed_test (interpretation_test (get_timeout @{context})) @{context} (TPTP_Syntax.get_file_list tptp_probs_dir))
   else ()
 *}
 
diff -r eb291b215c73 -r 2e2e9bc7c4c6 src/HOL/TPTP/TPTP_Parser_Test.thy
--- a/src/HOL/TPTP/TPTP_Parser_Test.thy	Wed Feb 19 15:57:02 2014 +0000
+++ b/src/HOL/TPTP/TPTP_Parser_Test.thy	Wed Feb 19 15:57:02 2014 +0000
@@ -51,7 +51,7 @@
          Path.implode #>
          TPTP_Problem_Name.parse_problem_name #>
          TPTP_Problem_Name.mangle_problem_name)
-        (test_files ())
+     (TPTP_Syntax.get_file_list tptp_probs_dir)
 *}
 
 
@@ -121,7 +121,7 @@
 ML {*
   if test_all @{context} then
     (report @{context} "Testing parser";
-     S timed_test parser_test @{context})
+     S timed_test parser_test @{context} (TPTP_Syntax.get_file_list tptp_probs_dir))
   else ()
 *}
 
diff -r eb291b215c73 -r 2e2e9bc7c4c6 src/HOL/TPTP/TPTP_Test.thy
--- a/src/HOL/TPTP/TPTP_Test.thy	Wed Feb 19 15:57:02 2014 +0000
+++ b/src/HOL/TPTP/TPTP_Test.thy	Wed Feb 19 15:57:02 2014 +0000
@@ -33,9 +33,6 @@
   val tptp_probs_dir =
     Path.explode "$TPTP/Problems"
     |> Path.expand;
-
-  (*list of files to under test*)
-  fun test_files () = TPTP_Syntax.get_file_list tptp_probs_dir;
 *}
 
 
@@ -70,11 +67,11 @@
           default_val)
     end
 
-  fun timed_test ctxt f =
+  fun timed_test ctxt f test_files =
     let
       fun f' x = (f x; ())
       val time =
-        Timing.timing (List.app f') (test_files ())
+        Timing.timing (List.app f') test_files
         |> fst
       val duration =
         #elapsed time
@@ -82,7 +79,7 @@
         |> Real.fromLargeInt
       val average =
         (StringCvt.FIX (SOME 3),
-         (duration / Real.fromInt (length (test_files ()))))
+         (duration / Real.fromInt (length test_files)))
         |-> Real.fmt
     in
       report ctxt ("Test timing: " ^ Timing.message time ^ "\n(about " ^ average ^