module MQGU = MQGUtil
module MQG = MQueryGenerator
-(* GLOBAL CONSTANTS *)
-let configuration_file = "triciclo.conf.xml"
+(* first of all let's initialize the Helm_registry *)
+let _ =
+ let configuration_file = "gTopLevel.conf.xml" in
+ if not (Sys.file_exists configuration_file) then begin
+ eprintf "E: Can't find configuration file '%s'\n" configuration_file;
+ exit 2
+ end;
+ Helm_registry.load_from configuration_file
+;;
+
+(* GLOBAL CONSTANTS *)
let mqi_debug_fun s = debug_print ~level:2 s
-let mqi_flags = [MQIC.Postgres ; MQIC.Stat ; MQIC.Warn ; MQIC.Log]
-let mqi_handle = MQIC.init mqi_flags 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]
;;
(** save an unfinished proof on the filesystem *)
let save_unfinished_proof () =
let (xml, bodyxml) = ProofEngine.get_current_status_as_xml () in
- let proof_file_type = Helm_registry.get "triciclo.proof_file_type" in
- let proof_file = Helm_registry.get "triciclo.proof_file" in
+ let proof_file_type = Helm_registry.get "gtoplevel.proof_file_type" in
+ let proof_file = Helm_registry.get "gtoplevel.proof_file" in
Xml.pp ~quiet:true xml (Some proof_file_type) ;
HelmLogger.log
(`Msg (`T ("Current proof type saved to " ^ proof_file_type))) ;
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);;
None -> raise NoChoice
| Some uri0 ->
let uri = UriManager.uri_of_string ("cic:" ^ uri0) in
- let proof_file_type = Helm_registry.get "triciclo.proof_file_type" in
- let proof_file = Helm_registry.get "triciclo.proof_file" in
+ let proof_file_type = Helm_registry.get "gtoplevel.proof_file_type" in
+ let proof_file = Helm_registry.get "gtoplevel.proof_file" in
match CicParser.obj_of_xml proof_file_type (Some proof_file) with
Cic.CurrentProof (_,metasenv,bo,ty,_) ->
typecheck_loaded_proof metasenv bo ty ;
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) ;
let dump_environment () =
try
- let oc = open_out (Helm_registry.get "triciclo.environment_file") in
+ let oc = open_out (Helm_registry.get "gtoplevel.environment_file") in
HelmLogger.log (`Msg (`T "Dumping environment ..."));
CicEnvironment.dump_to_channel oc;
HelmLogger.log (`Msg (`T "... done!")) ;
;;
let restore_environment () =
try
- let ic = open_in (Helm_registry.get "triciclo.environment_file") in
+ let ic = open_in (Helm_registry.get "gtoplevel.environment_file") in
HelmLogger.log (`Msg (`T "Restoring environment ... "));
CicEnvironment.restore_from_channel ic;
HelmLogger.log (`Msg (`T "... done!"));
(* MAIN *)
let initialize_everything () =
- if not (Sys.file_exists configuration_file) then begin
- eprintf "E: Can't find configuration file '%s'\n" configuration_file;
- exit 2
- end;
- Helm_registry.load_from configuration_file;
let output = TermViewer.proof_viewer ~width:350 ~height:280 () in
let notebook = new notebook in
let rendering_window' = new rendering_window output notebook in
(Some (print_error_as_html "XSLT Debug Message: "));
rendering_window'#show () ;
if restore_environment_on_boot &&
- Sys.file_exists (Helm_registry.get "triciclo.environment_file")
+ Sys.file_exists (Helm_registry.get "gtoplevel.environment_file")
then
restore_environment ();
GtkThread.main ()