1.1 --- a/src/HOL/TPTP/TPTP_Interpret_Test.thy	Tue Apr 17 16:14:07 2012 +0100
     1.2 +++ b/src/HOL/TPTP/TPTP_Interpret_Test.thy	Tue Apr 17 16:14:07 2012 +0100
     1.3 @@ -11,7 +11,7 @@
     1.4  begin
     1.5  
     1.6  section "Interpreter tests"
     1.7 -(*
     1.8 +
     1.9  text "Interpret a problem."
    1.10  ML {*
    1.11    val (time, ((type_map, const_map, fmlas), thy)) =
    1.12 @@ -27,19 +27,18 @@
    1.13  
    1.14  text "... and display nicely."
    1.15  ML {*
    1.16 -  List.app (Pretty.writeln o (Syntax.pretty_term @{context}) o #4) fmlas
    1.17 -*}
    1.18 -ML {*
    1.19 +  List.app (Pretty.writeln o (Syntax.pretty_term @{context}) o #4) fmlas;
    1.20 +
    1.21    (*Don't use TPTP_Syntax.string_of_tptp_formula, it's just for testing*)
    1.22    List.app (writeln o TPTP_Syntax.string_of_tptp_formula o #3) fmlas
    1.23  *}
    1.24 -*)
    1.25  
    1.26  subsection "Multiple tests"
    1.27  
    1.28  ML {*
    1.29 +  (*default timeout is 1 min*)
    1.30    fun interpret timeout file thy =
    1.31 -    TimeLimit.timeLimit (Time.fromSeconds (if timeout = 0 then 600 else timeout))
    1.32 +    TimeLimit.timeLimit (Time.fromSeconds (if timeout = 0 then 60 else timeout))
    1.33       (TPTP_Interpret.interpret_file
    1.34         false
    1.35         (Path.dir tptp_probs_dir)
    1.36 @@ -50,18 +49,9 @@
    1.37    fun interpret_timed timeout file thy =
    1.38      Timing.timing (interpret timeout file) thy
    1.39  
    1.40 -  (*default timeout is 10 mins*)
    1.41    fun interpretation_test timeout ctxt =
    1.42      test_fn ctxt
    1.43 -     (fn file => (*FIXME use "interpret" function above*)
    1.44 -       TimeLimit.timeLimit (Time.fromSeconds (if timeout = 0 then 600 else timeout))
    1.45 -        (TPTP_Interpret.interpret_file
    1.46 -          false
    1.47 -          (Path.dir tptp_probs_dir)
    1.48 -          file
    1.49 -          []
    1.50 -          [])
    1.51 -          @{theory}(*FIXME*))
    1.52 +     (fn file => interpret timeout file (Proof_Context.theory_of ctxt))
    1.53       "interpreter"
    1.54       ()
    1.55  
    1.56 @@ -128,19 +118,20 @@
    1.57  *}
    1.58  
    1.59  ML {*
    1.60 - interpretation_tests 5 @{context}
    1.61 + interpretation_tests (get_timeout @{context}) @{context}
    1.62     (some_probs @ take_too_long @ timeouts @ more_probs)
    1.63  *}
    1.64  
    1.65 -declare [[warning_out = ""]]
    1.66  
    1.67  subsection "Test against whole TPTP"
    1.68  
    1.69  text "Run interpretation over all problems. This works only for logics
    1.70   for which interpretation is defined (in TPTP_Parser/tptp_interpret.ML)."
    1.71  ML {*
    1.72 -  report @{context} "Interpreting all problems.";
    1.73 -  (*val _ = S timed_test (interpretation_test 5) @{context}*)
    1.74 +  if test_all @{context} then
    1.75 +    (report @{context} "Interpreting all problems";
    1.76 +     S timed_test (interpretation_test (get_timeout @{context})) @{context})
    1.77 +  else ()
    1.78  *}
    1.79  
    1.80 -end
    1.81 +end
    1.82 \ No newline at end of file