X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FgTopLevel.ml;h=988eb7e143e9a86ba563095a7dac0f4294976904;hb=947e7893dbb23fcaa998266ee8dd9a32b27d3b6e;hp=08e6e539aa7c1eb9922c0562cb66386a4c8fb2a2;hpb=eec68b7deed5396df14bd251127a96c46a868d06;p=helm.git diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml index 08e6e539a..988eb7e14 100644 --- a/helm/gTopLevel/gTopLevel.ml +++ b/helm/gTopLevel/gTopLevel.ml @@ -48,13 +48,21 @@ module MQGT = MQGTypes 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";; @@ -371,7 +379,7 @@ let interactive_interpretation_choice interpretations = GtkThread.main (); match !chosen with None -> raise NoChoice - | Some n -> n + | Some n -> [n] ;; @@ -398,14 +406,14 @@ let let innertypesuri = UriManager.innertypesuri_of_uri uri in Xml.pp ~quiet:true xmlinnertypes (Some (path ^ ".types.xml")) ; Http_getter.register' innertypesuri - (Helm_registry.get "annotations.url" ^ + (Helm_registry.get "local_library.url" ^ Str.replace_first (Str.regexp "^cic:") "" (UriManager.string_of_uri innertypesuri) ^ ".xml" ) ; (* constant type / variable / mutual inductive types definition *) Xml.pp ~quiet:true xml (Some (path ^ ".xml")) ; Http_getter.register' uri - (Helm_registry.get "annotations.url" ^ + (Helm_registry.get "local_library.url" ^ Str.replace_first (Str.regexp "^cic:") "" (UriManager.string_of_uri uri) ^ ".xml" ) ; @@ -420,7 +428,7 @@ let in Xml.pp ~quiet:true bodyxml' (Some (path ^ ".body.xml")) ; Http_getter.register' bodyuri - (Helm_registry.get "annotations.url" ^ + (Helm_registry.get "local_library.url" ^ Str.replace_first (Str.regexp "^cic:") "" (UriManager.string_of_uri bodyuri) ^ ".xml" ) @@ -433,7 +441,7 @@ exception OpenConjecturesStillThere;; exception WrongProof;; let pathname_of_annuri uristring = - Helm_registry.get "annotations.dir" ^ + Helm_registry.get "local_library.dir" ^ Str.replace_first (Str.regexp "^cic:") "" uristring ;; @@ -484,8 +492,8 @@ let qed () = (** 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))) ; @@ -650,6 +658,7 @@ module InvokeTacticsCallbacks = 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);; @@ -676,8 +685,8 @@ let load_unfinished_proof () = 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 ; @@ -2067,7 +2076,7 @@ let searchPattern () = | 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." @@ -2364,6 +2373,9 @@ object(self) 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 = @@ -2495,6 +2507,7 @@ object(self) 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) ; @@ -2585,7 +2598,7 @@ end 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!")) ; @@ -2597,7 +2610,7 @@ let dump_environment () = ;; 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!")); @@ -2835,11 +2848,6 @@ end (* 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 @@ -2853,7 +2861,7 @@ let initialize_everything () = (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 ()