--- a/src/Pure/Tools/proof_general_pure.ML Wed Dec 11 00:17:09 2013 +0000
+++ b/src/Pure/Tools/proof_general_pure.ML Wed Dec 11 18:02:22 2013 +0100
@@ -161,9 +161,11 @@
"Record full proof objects internally";
val _ =
- ProofGeneral.preference_int ProofGeneral.category_proof
+ ProofGeneral.preference ProofGeneral.category_proof
NONE
- Multithreading.max_threads
+ (Markup.print_int o Multithreading.max_threads_value)
+ (Multithreading.max_threads_update o Markup.parse_int)
+ ProofGeneral.pgipint
"max-threads"
"Maximum number of threads";
@@ -172,7 +174,7 @@
NONE
(fn () => Markup.print_bool (! Goal.parallel_proofs >= 1))
(fn s => Goal.parallel_proofs := (if Markup.parse_bool s then 1 else 0))
- ProofGeneral.pgipbool
+ ProofGeneral.pgipint
"parallel-proofs"
"Check proofs in parallel";