equal
deleted
inserted
replaced
12 sig |
12 sig |
13 val solve_directN: string |
13 val solve_directN: string |
14 val someN: string |
14 val someN: string |
15 val noneN: string |
15 val noneN: string |
16 val unknownN: string |
16 val unknownN: string |
17 val auto: bool Unsynchronized.ref |
|
18 val max_solutions: int Unsynchronized.ref |
17 val max_solutions: int Unsynchronized.ref |
19 val solve_direct: Proof.state -> bool * (string * Proof.state) |
18 val solve_direct: Proof.state -> bool * (string * Proof.state) |
20 val setup: theory -> theory |
19 val setup: theory -> theory |
21 end; |
20 end; |
22 |
21 |
31 val noneN = "none"; |
30 val noneN = "none"; |
32 val unknownN = "none"; |
31 val unknownN = "none"; |
33 |
32 |
34 (* preferences *) |
33 (* preferences *) |
35 |
34 |
36 val auto = Unsynchronized.ref false; |
|
37 val max_solutions = Unsynchronized.ref 5; |
35 val max_solutions = Unsynchronized.ref 5; |
38 |
36 |
39 val _ = |
37 val _ = |
40 ProofGeneral.preference_bool ProofGeneral.category_tracing |
38 ProofGeneral.preference_option ProofGeneral.category_tracing |
41 (SOME "true") |
39 (SOME "true") |
42 auto |
40 @{option auto_solve_direct} |
43 "auto-solve-direct" |
41 "auto-solve-direct" |
44 ("Run " ^ quote solve_directN ^ " automatically"); |
42 ("Run " ^ quote solve_directN ^ " automatically"); |
45 |
43 |
46 |
44 |
47 (* solve_direct command *) |
45 (* solve_direct command *) |
115 |
113 |
116 (* hook *) |
114 (* hook *) |
117 |
115 |
118 fun try_solve_direct auto = do_solve_direct (if auto then Auto_Try else Try) |
116 fun try_solve_direct auto = do_solve_direct (if auto then Auto_Try else Try) |
119 |
117 |
120 val setup = Try.register_tool (solve_directN, (10, auto, try_solve_direct)); |
118 val setup = Try.register_tool (solve_directN, (10, @{option auto_solve_direct}, try_solve_direct)); |
121 |
119 |
122 end; |
120 end; |