[isabelle-dev] Option type for auto tools timeout

[Holger Gast]

Hi developers,

changeset 061b8257ab9f of one week ago changed the type of the time
limit option for automatic provers from int to real.
(In response to a previous discussion.)

diff -r c600f6ae4b09 -r 061b8257ab9f src/Tools/auto_tools.ML
--- a/src/Tools/auto_tools.ML   Fri Dec 03 08:40:47 2010 +0100
+++ b/src/Tools/auto_tools.ML   Fri Dec 03 09:55:45 2010 +0100
@@ -6,10 +6,11 @@

 signature AUTO_TOOLS =
 sig
-  val time_limit: int Unsynchronized.ref
+  val time_limit: real Unsynchronized.ref

and correspondingly further down in the same file:

   ProofGeneralPgip.add_preference Preferences.category_tracing
-    (Preferences.nat_pref time_limit
-      "auto-tools-time-limit"
-      "Time limit for automatic tools (in milliseconds).")
+    (Preferences.real_pref time_limit
+      auto_tools_time_limitN "Time limit for automatic tools (in seconds).")

Despite the change to "Preferences.real_pref" here, the query for options during
startup yields type "int" for the option (cut from the *isabelle* Emacs buffer):

<haspref name="auto-tools-time-limit" descr="Time limit for automatic tools (in
seconds)." default="4.0"><pgipint/></haspref>

I guess this should be consistently output as pgipreal?

Since somebody on the list will know immediately where to look,
and maybe change things, I did not dig any further.

Thank you very much,

Holger