equal
deleted
inserted
replaced
10 val genuineN: string |
10 val genuineN: string |
11 val noneN: string |
11 val noneN: string |
12 val unknownN: string |
12 val unknownN: string |
13 val setup: theory -> theory |
13 val setup: theory -> theory |
14 (*configuration*) |
14 (*configuration*) |
15 val auto: bool Unsynchronized.ref |
|
16 val batch_tester : string Config.T |
15 val batch_tester : string Config.T |
17 val size : int Config.T |
16 val size : int Config.T |
18 val iterations : int Config.T |
17 val iterations : int Config.T |
19 val depth : int Config.T |
18 val depth : int Config.T |
20 val no_assms : bool Config.T |
19 val no_assms : bool Config.T |
92 val unknownN = "unknown" |
91 val unknownN = "unknown" |
93 |
92 |
94 |
93 |
95 (* preferences *) |
94 (* preferences *) |
96 |
95 |
97 val auto = Unsynchronized.ref false; |
|
98 |
|
99 val _ = |
96 val _ = |
100 ProofGeneral.preference_bool ProofGeneral.category_tracing |
97 ProofGeneral.preference_option ProofGeneral.category_tracing |
101 (SOME "true") |
98 (SOME "true") |
102 auto |
99 @{option auto_quickcheck} |
103 "auto-quickcheck" |
100 "auto-quickcheck" |
104 "Run Quickcheck automatically"; |
101 "Run Quickcheck automatically"; |
105 |
102 |
106 |
103 |
107 (* quickcheck report *) |
104 (* quickcheck report *) |
565 (noneN, state) |
562 (noneN, state) |
566 end) |
563 end) |
567 end |
564 end |
568 |> `(fn (outcome_code, _) => outcome_code = genuineN); |
565 |> `(fn (outcome_code, _) => outcome_code = genuineN); |
569 |
566 |
570 val setup = Try.register_tool (quickcheckN, (20, auto, try_quickcheck)); |
567 val setup = Try.register_tool (quickcheckN, (20, @{option auto_quickcheck}, try_quickcheck)); |
571 |
568 |
572 end; |
569 end; |
573 |
570 |
574 val auto_quickcheck = Quickcheck.auto; |
|