set_metasenv : Cic.metasenv -> unit ;
context: Cic.context ;
set_context : Cic.context -> unit >
- (* output messages *)
- val output_html : Ui_logger.html_msg -> unit
(* GUI refresh functions *)
val refresh_proof : unit -> unit
val refresh_goals : unit -> unit
(UriManager.uri * int * 'a) list ->
(UriManager.uri * int * 'b list) list
val mk_fresh_name_callback : ProofEngineTypes.mk_fresh_name_type
+ val mqi_handle : MQIConn.handle
end
;;
val whd_in_scratch : unit -> unit
val reduce_in_scratch : unit -> unit
val simpl_in_scratch : unit -> unit
+ val auto : unit -> unit
end
module Make (C: Callbacks) : Tactics =
struct
let print_uncaught_exception e =
- C.output_html (`Error (`T (sprintf "Uncaught exception: %s"
+ HelmLogger.log (`Error (`T (sprintf "Uncaught exception: %s"
(Printexc.to_string e))))
let handle_refresh_exception f savedproof savedgoal =
f ()
with
| RefreshSequentException e ->
- C.output_html (`Error (`T
+ HelmLogger.log (`Error (`T
(sprintf "Exception raised during the refresh of the sequent: %s"
(Printexc.to_string e))));
ProofEngine.set_proof savedproof ;
ProofEngine.goal := savedgoal ;
C.refresh_goals ()
| RefreshProofException e ->
- C.output_html (`Error (`T
+ HelmLogger.log (`Error (`T
(sprintf "Exception raised during the refresh of the proof: %s"
(Printexc.to_string e))));
ProofEngine.set_proof savedproof ;
C.refresh_goals () ;
C.refresh_proof ())
savedproof savedgoal
- | [] -> C.output_html (`Error (`T "No term selected"))
- | _ -> C.output_html (`Error (`T "Too many terms selected"))
+ | [] -> HelmLogger.log (`Error (`T "No term selected"))
+ | _ -> HelmLogger.log (`Error (`T "Too many terms selected"))
let call_tactic_with_goal_inputs tactic () =
let module L = LogicalOperations in
handle_refresh_exception
(fun () ->
match (C.sequent_viewer ())#get_selected_terms with
- | [] -> C.output_html (`Error (`T "No term selected"))
+ | [] -> HelmLogger.log (`Error (`T "No term selected"))
| terms ->
tactic terms ;
C.refresh_goals () ;
C.refresh_proof () ;
(C.term_editor ())#reset)
savedproof savedgoal
- | [] -> C.output_html (`Error (`T "No term selected"))
- | _ -> C.output_html (`Error (`T "Too many terms selected"))
+ | [] -> HelmLogger.log (`Error (`T "No term selected"))
+ | _ -> HelmLogger.log (`Error (`T "Too many terms selected"))
let call_tactic_with_goal_input_in_scratch tactic () =
let module L = LogicalOperations in
with
e -> print_uncaught_exception e
end
- | [] -> C.output_html (`Error (`T "No term selected"))
- | _ -> C.output_html (`Error (`T "Too many terms selected"))
+ | [] -> HelmLogger.log (`Error (`T "No term selected"))
+ | _ -> HelmLogger.log (`Error (`T "Too many terms selected"))
let call_tactic_with_goal_inputs_in_scratch tactic () =
let module L = LogicalOperations in
let module G = Gdome in
let scratch_window = C.scratch_window () in
match scratch_window#sequent_viewer#get_selected_terms with
- | [] -> C.output_html (`Error (`T "No term selected"))
+ | [] -> HelmLogger.log (`Error (`T "No term selected"))
| terms ->
try
let expr = tactic terms scratch_window#term in
C.refresh_goals () ;
C.refresh_proof ())
savedproof savedgoal
- | [] -> C.output_html (`Error (`T "No hypothesis selected"))
- | _ -> C.output_html (`Error (`T "Too many hypotheses selected"))
+ | [] -> HelmLogger.log (`Error (`T "No hypothesis selected"))
+ | _ -> HelmLogger.log (`Error (`T "Too many hypotheses selected"))
+
let intros =
(ProofEngine.intros ~mk_fresh_name_callback:C.mk_fresh_name_callback)
let exact = call_tactic_with_input ProofEngine.exact
let apply = call_tactic_with_input ProofEngine.apply
+ let auto = call_tactic (ProofEngine.auto C.mqi_handle)
let elimintrossimpl = call_tactic_with_input ProofEngine.elim_intros_simpl
let elimtype = call_tactic_with_input ProofEngine.elim_type
let whd = call_tactic_with_goal_inputs ProofEngine.whd