(* GLOBAL CONSTANTS *)
let mqi_debug_fun s = debug_print ~level:2 s
-let mqi_handle = MQIC.init mqi_debug_fun
+let mqi_handle = MQIC.init ~log:mqi_debug_fun ()
let xlinkns = Gdome.domString "http://www.w3.org/1999/xlink";;
GtkThread.main ();
match !chosen with
None -> raise NoChoice
- | Some n -> n
+ | Some n -> [n]
;;
let decompose_uris_choice_callback = decompose_uris_choice_callback
let mk_fresh_name_callback = mk_fresh_name_callback
+ let mqi_handle = mqi_handle
end
;;
module InvokeTactics' = InvokeTactics.Make (InvokeTacticsCallbacks);;
| Some metano ->
let uris' =
TacticChaser.matchConclusion mqi_handle
- ~choose_must () ~status:(proof, metano)
+ ~choose_must () (proof, metano)
in
let uri' =
user_uri_choice ~title:"Ambiguous input."
let contradictionb =
GButton.button ~label:"Contradiction"
~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
+ let autob=
+ GButton.button ~label:"Auto"
+ ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
let hbox4 =
GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in
let existsb =
ignore(searchpatternb#connect#clicked searchPattern) ;
ignore(injectionb#connect#clicked InvokeTactics'.injection) ;
ignore(discriminateb#connect#clicked InvokeTactics'.discriminate) ;
+ ignore(autob#connect#clicked InvokeTactics'.auto) ;
(* Zack: spostare in una toolbar
ignore(whdb#connect#clicked whd) ;
ignore(reduceb#connect#clicked reduce) ;