equal
deleted
inserted
replaced
34 val messagesN = "messages" |
34 val messagesN = "messages" |
35 val supported_proversN = "supported_provers" |
35 val supported_proversN = "supported_provers" |
36 val running_proversN = "running_provers" |
36 val running_proversN = "running_provers" |
37 val kill_proversN = "kill_provers" |
37 val kill_proversN = "kill_provers" |
38 val refresh_tptpN = "refresh_tptp" |
38 val refresh_tptpN = "refresh_tptp" |
39 val mash_resetN = "mash_reset" |
39 val reset_mashN = "reset_mash" |
40 val mash_learnN = "mash_learn" |
|
41 |
40 |
42 val auto = Unsynchronized.ref false |
41 val auto = Unsynchronized.ref false |
43 |
42 |
44 val _ = |
43 val _ = |
45 ProofGeneralPgip.add_preference Preferences.category_tracing |
44 ProofGeneralPgip.add_preference Preferences.category_tracing |
375 running_provers () |
374 running_provers () |
376 else if subcommand = kill_proversN then |
375 else if subcommand = kill_proversN then |
377 kill_provers () |
376 kill_provers () |
378 else if subcommand = refresh_tptpN then |
377 else if subcommand = refresh_tptpN then |
379 refresh_systems_on_tptp () |
378 refresh_systems_on_tptp () |
380 else if subcommand = mash_resetN then |
379 else if subcommand = reset_mashN then |
381 mash_reset () |
380 mash_reset ctxt |
382 else if subcommand = mash_learnN then |
|
383 () (* TODO: implement *) |
|
384 else |
381 else |
385 error ("Unknown subcommand: " ^ quote subcommand ^ ".") |
382 error ("Unknown subcommand: " ^ quote subcommand ^ ".") |
386 end |
383 end |
387 |
384 |
388 fun sledgehammer_trans (((subcommand, params), fact_override), opt_i) = |
385 fun sledgehammer_trans (((subcommand, params), fact_override), opt_i) = |