X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FgTopLevel.ml;h=0d0b7c4d171afe54dd25b143cbce86194ca8965c;hb=78a92e3cc2deb60d306da93d9dcf987c1cb219ba;hp=03d12a4c5150057c475785775d702a3b873b1ab5;hpb=9be7ec5bbacfafed8a3e37cfe0095f2aea1b9bf9;p=helm.git diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml index 03d12a4c5..0d0b7c4d1 100644 --- a/helm/gTopLevel/gTopLevel.ml +++ b/helm/gTopLevel/gTopLevel.ml @@ -20,7 +20,7 @@ * MA 02111-1307, USA. * * For details, see the HELM World-Wide-Web page, - * http://cs.unibo.it/helm/. + * http://helm.cs.unibo.it/ *) (******************************************************************************) @@ -35,6 +35,8 @@ let debug_level = ref 1 let debug_print ?(level = 1) s = if !debug_level >= level then prerr_endline s +let error s = prerr_endline ("E: " ^ s) +let warning s = prerr_endline ("W: " ^ s) open Printf @@ -46,35 +48,24 @@ module MQGT = MQGTypes module MQGU = MQGUtil module MQG = MQueryGenerator + +(* 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";; -let prooffile = - try - Sys.getenv "GTOPLEVEL_PROOFFILE" - with - Not_found -> "/public/currentproof" -;; - -let prooffiletype = - try - Sys.getenv "GTOPLEVEL_PROOFFILETYPE" - with - Not_found -> "/public/currentprooftype" -;; - -let environmentfile = - try - Sys.getenv "GTOPLEVEL_ENVIRONMENTFILE" - with - Not_found -> "/public/environment" -;; - let restore_environment_on_boot = true ;; let notify_hbugs_on_goal_change = false ;; @@ -108,18 +99,6 @@ let set_settings_window,settings_window = ) ;; -exception OutputHtmlNotInitialized;; - -let set_outputhtml,outputhtml = - let outputhtml_ref = ref None in - (function (rw: Ui_logger.html_logger) -> outputhtml_ref := Some rw), - (function () -> - match !outputhtml_ref with - | None -> raise OutputHtmlNotInitialized - | Some outputhtml -> (outputhtml: Ui_logger.html_logger) - ) -;; - exception QedSetSensitiveNotInitialized;; let qed_set_sensitive = ref (function _ -> raise QedSetSensitiveNotInitialized) @@ -170,14 +149,11 @@ let string_of_cic_textual_parser_uri uri = String.sub uri' 4 (String.length uri' - 4) ;; -let output_html ?(append_NL = true) (outputhtml: Ui_logger.html_logger) = - outputhtml#log ~append_NL - (* UTILITY FUNCTIONS TO DISAMBIGUATE AN URI *) (* Check window *) -let check_window (outputhtml: Ui_logger.html_logger) uris = +let check_window uris = let window = GWindow.window ~width:800 ~modal:true ~title:"Check" ~border_width:2 () in @@ -208,7 +184,7 @@ let check_window (outputhtml: Ui_logger.html_logger) uris = mmlwidget#load_sequent [] (111,[],expr) with e -> - output_html outputhtml (`Error (`T (Printexc.to_string e))) + HelmLogger.log (`Error (`T (Printexc.to_string e))) ) ) uris in @@ -220,9 +196,9 @@ let check_window (outputhtml: Ui_logger.html_logger) uris = exception NoChoice;; -let - interactive_user_uri_choice ~(selection_mode:[`MULTIPLE|`SINGLE]) ?(ok="Ok") - ?(enable_button_for_non_vars=false) ~title ~msg uris +let interactive_user_uri_choice + ~(selection_mode:[ `SINGLE | `MULTIPLE ]) + ?(ok="Ok") ?(enable_button_for_non_vars=false) ~title ~msg uris = let only_constant_choices = lazy @@ -230,7 +206,7 @@ let (fun uri -> not (String.sub uri (String.length uri - 4) 4 = ".var")) uris) in - if !auto_disambiguation then + if selection_mode <> `SINGLE && !auto_disambiguation then Lazy.force only_constant_choices else begin let choices = ref [] in @@ -289,7 +265,7 @@ let (* actions *) let check_callback () = assert (List.length !choices > 0) ; - check_window (outputhtml ()) !choices + check_window !choices in ignore (window#connect#destroy GMain.Main.quit) ; ignore (cancelb#connect#clicked window#destroy) ; @@ -403,7 +379,7 @@ let interactive_interpretation_choice interpretations = GtkThread.main (); match !chosen with None -> raise NoChoice - | Some n -> n + | Some n -> [n] ;; @@ -429,15 +405,15 @@ let (* innertypes *) let innertypesuri = UriManager.innertypesuri_of_uri uri in Xml.pp ~quiet:true xmlinnertypes (Some (path ^ ".types.xml")) ; - Getter.register innertypesuri - (Configuration.annotations_url ^ + Http_getter.register' innertypesuri + (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")) ; - Getter.register uri - (Configuration.annotations_url ^ + Http_getter.register' uri + (Helm_registry.get "local_library.url" ^ Str.replace_first (Str.regexp "^cic:") "" (UriManager.string_of_uri uri) ^ ".xml" ) ; @@ -451,8 +427,8 @@ let | Some bodyuri -> bodyuri in Xml.pp ~quiet:true bodyxml' (Some (path ^ ".body.xml")) ; - Getter.register bodyuri - (Configuration.annotations_url ^ + Http_getter.register' bodyuri + (Helm_registry.get "local_library.url" ^ Str.replace_first (Str.regexp "^cic:") "" (UriManager.string_of_uri bodyuri) ^ ".xml" ) @@ -465,7 +441,7 @@ exception OpenConjecturesStillThere;; exception WrongProof;; let pathname_of_annuri uristring = - Configuration.annotations_dir ^ + Helm_registry.get "local_library.dir" ^ Str.replace_first (Str.regexp "^cic:") "" uristring ;; @@ -515,14 +491,15 @@ let qed () = (** save an unfinished proof on the filesystem *) let save_unfinished_proof () = - let outputhtml = ((rendering_window ())#outputhtml(* : GHtml.xmhtml*)) in let (xml, bodyxml) = ProofEngine.get_current_status_as_xml () in - Xml.pp ~quiet:true xml (Some prooffiletype) ; - output_html outputhtml - (`Msg (`T ("Current proof type saved to " ^ prooffiletype))) ; - Xml.pp ~quiet:true bodyxml (Some prooffile) ; - output_html outputhtml - (`Msg (`T ("Current proof body saved to " ^ prooffile))) + 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))) ; + Xml.pp ~quiet:true bodyxml (Some proof_file) ; + HelmLogger.log + (`Msg (`T ("Current proof body saved to " ^ proof_file))) ;; (* Used to typecheck the loaded proofs *) @@ -681,7 +658,7 @@ module InvokeTacticsCallbacks = let decompose_uris_choice_callback = decompose_uris_choice_callback let mk_fresh_name_callback = mk_fresh_name_callback - let output_html msg = output_html (outputhtml ()) msg + let mqi_handle = mqi_handle end ;; module InvokeTactics' = InvokeTactics.Make (InvokeTacticsCallbacks);; @@ -690,9 +667,7 @@ module InvokeTactics' = InvokeTactics.Make (InvokeTacticsCallbacks);; module Ignore = Hbugs.Initialize (InvokeTactics');; Hbugs.set_describe_hint_callback (fun hint -> match hint with - | Hbugs_types.Use_apply_Luke term -> - let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in - check_window outputhtml [term] + | Hbugs_types.Use_apply_Luke term -> check_window [term] | _ -> ()) ;; *) @@ -700,7 +675,6 @@ let dummy_uri = "/dummy.con" (** load an unfinished proof from filesystem *) let load_unfinished_proof () = - let outputhtml = ((rendering_window ())#outputhtml(* : GHtml.xmhtml*)) in let output = ((rendering_window ())#output : TermViewer.proof_viewer) in let notebook = (rendering_window ())#notebook in try @@ -711,7 +685,9 @@ let load_unfinished_proof () = None -> raise NoChoice | Some uri0 -> let uri = UriManager.uri_of_string ("cic:" ^ uri0) in - match CicParser.obj_of_xml prooffiletype (Some prooffile) with + 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 ; ProofEngine.set_proof (Some (uri, metasenv, bo, ty)) ; @@ -722,25 +698,23 @@ let load_unfinished_proof () = | (metano,_,_)::_ -> Some metano ) ; refresh_goals notebook ; - output_html outputhtml - (`Msg (`T ("Current proof type loaded from " ^ - prooffiletype))) ; - output_html outputhtml - (`Msg (`T ("Current proof body loaded from " ^ - prooffile))) ; + HelmLogger.log + (`Msg (`T ("Current proof type loaded from " ^ proof_file_type))); + HelmLogger.log + (`Msg (`T ("Current proof body loaded from " ^ proof_file))) ; !save_set_sensitive true; | _ -> assert false with InvokeTactics.RefreshSequentException e -> - output_html outputhtml + HelmLogger.log (`Error (`T ("Exception raised during the refresh of the " ^ "sequent: " ^ Printexc.to_string e))) | InvokeTactics.RefreshProofException e -> - output_html outputhtml + HelmLogger.log (`Error (`T ("Exception raised during the refresh of the " ^ "proof: " ^ Printexc.to_string e))) | e -> - output_html outputhtml + HelmLogger.log (`Error (`T (Printexc.to_string e))) ;; @@ -796,7 +770,7 @@ let edit_aliases () = (try DisambiguatingParser.EnvironmentP3.of_string raw_aliases with e -> - output_html (outputhtml ()) + HelmLogger.log (`Error (`T ("Error while parsing aliases: " ^ Printexc.to_string e))); !disambiguation_env) @@ -809,22 +783,21 @@ let proveit () = let module G = Gdome in let notebook = (rendering_window ())#notebook in let output = (rendering_window ())#output in - let outputhtml = (rendering_window ())#outputhtml in try output#make_sequent_of_selected_term ; refresh_proof output ; refresh_goals notebook with InvokeTactics.RefreshSequentException e -> - output_html outputhtml + HelmLogger.log (`Error (`T ("Exception raised during the refresh of the " ^ "sequent: " ^ Printexc.to_string e))) | InvokeTactics.RefreshProofException e -> - output_html outputhtml + HelmLogger.log (`Error (`T ("Exception raised during the refresh of the " ^ "proof: " ^ Printexc.to_string e))) | e -> - output_html outputhtml + HelmLogger.log (`Error (`T (Printexc.to_string e))) ;; @@ -832,22 +805,21 @@ let focus () = let module L = LogicalOperations in let module G = Gdome in let notebook = (rendering_window ())#notebook in - let outputhtml = ((rendering_window ())#outputhtml(* : GHtml.xmhtml*)) in let output = (rendering_window ())#output in try output#focus_sequent_of_selected_term ; refresh_goals notebook with InvokeTactics.RefreshSequentException e -> - output_html outputhtml + HelmLogger.log (`Error (`T ("Exception raised during the refresh of the " ^ "sequent: " ^ Printexc.to_string e))) | InvokeTactics.RefreshProofException e -> - output_html outputhtml + HelmLogger.log (`Error (`T ("Exception raised during the refresh of the " ^ "proof: " ^ Printexc.to_string e))) | e -> - output_html outputhtml + HelmLogger.log (`Error (`T (Printexc.to_string e))) ;; @@ -859,7 +831,6 @@ let setgoal metano = let module G = Gdome in let notebook = (rendering_window ())#notebook in let output = (rendering_window ())#output in - let outputhtml = (rendering_window ())#outputhtml in let metasenv = match ProofEngine.get_proof () with None -> assert false @@ -869,11 +840,11 @@ let setgoal metano = refresh_goals ~empty_notebook:false notebook with InvokeTactics.RefreshSequentException e -> - output_html outputhtml + HelmLogger.log (`Error (`T ("Exception raised during the refresh of the " ^ "sequent: " ^ Printexc.to_string e))) | e -> - output_html outputhtml + HelmLogger.log (`Error (`T (Printexc.to_string e))) ;; @@ -891,7 +862,6 @@ let let _ = window#event#connect#delete (fun _ -> window#misc#hide () ; true ) in let href = Gdome.domString "href" in let show_in_show_window_obj uri obj = - let outputhtml = ((rendering_window ())#outputhtml(* : GHtml.xmhtml*)) in try let (acic,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts, @@ -908,7 +878,7 @@ let mmlwidget#load_doc mml ; with e -> - output_html outputhtml + HelmLogger.log (`Error (`T (Printexc.to_string e))) in let show_in_show_window_uri uri = @@ -952,8 +922,6 @@ let user_uri_choice ~title ~msg uris = ;; let locate_callback id = - let outputhtml = ((rendering_window ())#outputhtml(* : GHtml.xmhtml*)) in - let out = output_html outputhtml in let query = MQG.locate id in let result = MQI.execute mqi_handle query in let uris = @@ -961,10 +929,10 @@ let locate_callback id = (function uri,_ -> MQueryMisc.wrong_xpointer_format_from_wrong_xpointer_format' uri) result in - out (`Msg (`T "Locate Query:")) ; - MQueryUtil.text_of_query (fun m -> out (`Msg (`T m))) "" query; - out (`Msg (`T "Result:")) ; - MQueryUtil.text_of_result (fun m -> out (`Msg (`T m))) "" result; + HelmLogger.log (`Msg (`T "Locate Query:")) ; + MQueryUtil.text_of_query (fun m -> HelmLogger.log (`Msg (`T m))) "" query; + HelmLogger.log (`Msg (`T "Result:")) ; + MQueryUtil.text_of_result (fun m -> HelmLogger.log (`Msg (`T m))) "" result; user_uri_choice ~title:"Ambiguous input." ~msg: ("Ambiguous input \"" ^ id ^ @@ -1016,24 +984,23 @@ let input_or_locate_uri ~title = ignore (cancelb#connect#clicked (function () -> uri := None ; window#destroy ())) ; let check_callback () = - let outputhtml = ((rendering_window ())#outputhtml(* : GHtml.xmhtml*)) in let uri = "cic:" ^ manual_input#text in try - ignore (Getter.resolve (UriManager.uri_of_string uri)) ; - output_html outputhtml (`Msg (`T "OK")) ; + ignore (Http_getter.resolve' (UriManager.uri_of_string uri)) ; + HelmLogger.log (`Msg (`T "OK")) ; true with - Getter.Unresolved -> - output_html outputhtml + Http_getter_types.Unresolvable_URI _ -> + HelmLogger.log (`Error (`T ("URI " ^ uri ^ " does not correspond to any object."))) ; false | UriManager.IllFormedUri _ -> - output_html outputhtml + HelmLogger.log (`Error (`T ("URI " ^ uri ^ " is not well-formed."))) ; false | e -> - output_html outputhtml + HelmLogger.log (`Error (`T (Printexc.to_string e))) ; false in @@ -1083,13 +1050,12 @@ exception AmbiguousInput;; module DisambiguateCallbacks = struct - let output_html ?append_NL = output_html ?append_NL (outputhtml ()) let interactive_user_uri_choice = fun ~selection_mode ?ok ?enable_button_for_non_vars ~title ~msg ~id -> interactive_user_uri_choice ~selection_mode ?ok ?enable_button_for_non_vars ~title ~msg let interactive_interpretation_choice = interactive_interpretation_choice - let input_or_locate_uri = input_or_locate_uri + let input_or_locate_uri ~title ?id = input_or_locate_uri ~title end ;; @@ -1099,7 +1065,6 @@ module TermEditor' = ChosenTermEditor.Make (DisambiguateCallbacks);; let locate () = let inputt = ((rendering_window ())#inputt : TermEditor.term_editor) in - let outputhtml = ((rendering_window ())#outputhtml(* : GHtml.xmhtml*)) in try match GToolbox.input_string ~title:"Locate" "Enter an identifier to locate:" @@ -1110,7 +1075,7 @@ let locate () = inputt#set_term uri with e -> - output_html outputhtml + HelmLogger.log (`Error (`T (Printexc.to_string e))) ;; @@ -1120,7 +1085,6 @@ exception NotAUriToAConstant;; let new_inductive () = let inputt = ((rendering_window ())#inputt : TermEditor.term_editor) in - let outputhtml = ((rendering_window ())#outputhtml(* : GHtml.xmhtml*)) in let output = ((rendering_window ())#output : TermViewer.proof_viewer) in let notebook = (rendering_window ())#notebook in @@ -1207,10 +1171,9 @@ let new_inductive () = let uri = UriManager.uri_of_string (uristr ^ "/" ^ he ^ ".ind") in begin try - ignore (Getter.resolve uri) ; + ignore (Http_getter.resolve' uri) ; raise UriAlreadyInUse - with - Getter.Unresolved -> + with Http_getter_types.Unresolvable_URI _ -> get_uri := (function () -> uri) ; get_names := (function () -> names) ; inductive := inductiveb#active ; @@ -1219,7 +1182,7 @@ let new_inductive () = end with e -> - output_html outputhtml + HelmLogger.log (`Error (`T (Printexc.to_string e))) )) (* Second phase *) @@ -1326,7 +1289,7 @@ let new_inductive () = window#destroy () with e -> - output_html outputhtml + HelmLogger.log (`Error (`T (Printexc.to_string e))) )) (* Third phase *) @@ -1400,7 +1363,7 @@ let new_inductive () = window2#destroy () with e -> - output_html outputhtml + HelmLogger.log (`Error (`T (Printexc.to_string e))) )) ; window2#show () ; @@ -1446,13 +1409,12 @@ let new_inductive () = show_in_show_window_obj uri obj with e -> - output_html outputhtml + HelmLogger.log (`Error (`T (Printexc.to_string e))) ;; let new_proof () = let inputt = ((rendering_window ())#inputt : TermEditor.term_editor) in - let outputhtml = ((rendering_window ())#outputhtml(* : GHtml.xmhtml*)) in let output = ((rendering_window ())#output : TermViewer.proof_viewer) in let notebook = (rendering_window ())#notebook in @@ -1530,17 +1492,16 @@ let new_proof () = else begin try - ignore (Getter.resolve uri) ; + ignore (Http_getter.resolve' uri) ; raise UriAlreadyInUse - with - Getter.Unresolved -> + with Http_getter_types.Unresolvable_URI _ -> get_metasenv_and_term := (function () -> metasenv,parsed) ; get_uri := (function () -> uri) ; window#destroy () end with e -> - output_html outputhtml + HelmLogger.log (`Error (`T (Printexc.to_string e))) )) ; window#show () ; @@ -1561,15 +1522,15 @@ let new_proof () = refresh_proof output with InvokeTactics.RefreshSequentException e -> - output_html outputhtml + HelmLogger.log (`Error (`T ("Exception raised during the refresh of the " ^ "sequent: " ^ Printexc.to_string e))) | InvokeTactics.RefreshProofException e -> - output_html outputhtml + HelmLogger.log (`Error (`T ("Exception raised during the refresh of the " ^ "proof: " ^ Printexc.to_string e))) | e -> - output_html outputhtml + HelmLogger.log (`Error (`T (Printexc.to_string e))) ;; @@ -1590,7 +1551,6 @@ let check_term_in_scratch scratch_window metasenv context expr = let check scratch_window () = let inputt = ((rendering_window ())#inputt : TermEditor.term_editor) in - let outputhtml = ((rendering_window ())#outputhtml(* : GHtml.xmhtml*)) in let metasenv = match ProofEngine.get_proof () with None -> [] @@ -1610,24 +1570,22 @@ let check scratch_window () = check_term_in_scratch scratch_window metasenv' context expr with e -> - output_html outputhtml + HelmLogger.log (`Error (`T (Printexc.to_string e))) ;; let show () = - let outputhtml = ((rendering_window ())#outputhtml(* : GHtml.xmhtml*)) in try show_in_show_window_uri (input_or_locate_uri ~title:"Show") with e -> - output_html outputhtml + HelmLogger.log (`Error (`T (Printexc.to_string e))) ;; exception NotADefinition;; let open_ () = - let outputhtml = ((rendering_window ())#outputhtml(* : GHtml.xmhtml*)) in let output = ((rendering_window ())#output : TermViewer.proof_viewer) in let notebook = (rendering_window ())#notebook in try @@ -1648,15 +1606,15 @@ let open_ () = !save_set_sensitive true with InvokeTactics.RefreshSequentException e -> - output_html outputhtml + HelmLogger.log (`Error (`T ("Exception raised during the refresh of the " ^ "sequent: " ^ Printexc.to_string e))) | InvokeTactics.RefreshProofException e -> - output_html outputhtml + HelmLogger.log (`Error (`T ("Exception raised during the refresh of the " ^ "proof: " ^ Printexc.to_string e))) | e -> - output_html outputhtml + HelmLogger.log (`Error (`T (Printexc.to_string e))) ;; @@ -1898,7 +1856,6 @@ let refine_constraints (must_obj,must_rel,must_sort) = let completeSearchPattern () = let inputt = ((rendering_window ())#inputt : TermEditor.term_editor) in - let outputhtml = ((rendering_window ())#outputhtml(* : GHtml.xmhtml*)) in try let metasenv,expr = inputt#get_metasenv_and_term ~context:[] ~metasenv:[] in let must = CGSearchPattern.get_constraints expr in @@ -1910,12 +1867,11 @@ let completeSearchPattern () = show_query_results results with e -> - output_html outputhtml + HelmLogger.log (`Error (`T (Printexc.to_string e))) ;; let insertQuery () = - let outputhtml = ((rendering_window ())#outputhtml(* : GHtml.xmhtml*)) in try let chosen = ref None in let window = @@ -1978,7 +1934,7 @@ let insertQuery () = show_query_results results with e -> - output_html outputhtml + HelmLogger.log (`Error (`T (Printexc.to_string e))) ;; @@ -2109,7 +2065,6 @@ let choose_must list_of_must only = let searchPattern () = let inputt = ((rendering_window ())#inputt : TermEditor.term_editor) in - let outputhtml = ((rendering_window ())#outputhtml(* : GHtml.xmhtml*)) in try let proof = match ProofEngine.get_proof () with @@ -2120,10 +2075,8 @@ let searchPattern () = | None -> () | Some metano -> let uris' = - TacticChaser.matchConclusion - mqi_handle - ~output_html:(fun m -> output_html outputhtml (`Msg (`T m))) - ~choose_must () ~status:(proof, metano) + TacticChaser.matchConclusion mqi_handle + ~choose_must () (proof, metano) in let uri' = user_uri_choice ~title:"Ambiguous input." @@ -2134,7 +2087,7 @@ let searchPattern () = InvokeTactics'.apply () with e -> - output_html outputhtml + HelmLogger.log (`Error (`T (Printexc.to_string e))) ;; @@ -2420,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 = @@ -2551,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) ; @@ -2641,29 +2598,25 @@ end let dump_environment () = try - let oc = open_out environmentfile in - output_html (outputhtml ()) (`Msg (`T "Dumping environment ...")); - CicEnvironment.dump_to_channel - ~callback:(fun uri -> output_html (outputhtml ()) (`Msg (`T uri))) - oc; - output_html (outputhtml ()) (`Msg (`T "... done!")) ; + 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!")) ; close_out oc with exc -> - output_html (outputhtml ()) + HelmLogger.log (`Error (`T (Printf.sprintf "Dump failure, uncaught exception:%s" (Printexc.to_string exc)))) ;; let restore_environment () = try - let ic = open_in environmentfile in - output_html (outputhtml ()) (`Msg (`T "Restoring environment ... ")); - CicEnvironment.restore_from_channel - ~callback:(fun uri -> output_html (outputhtml ()) (`Msg (`T uri))) - ic; - output_html (outputhtml ()) (`Msg (`T "... done!")); + 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!")); close_in ic with exc -> - output_html (outputhtml ()) + HelmLogger.log (`Error (`T (Printf.sprintf "Restore failure, uncaught exception:%s" (Printexc.to_string exc)))) ;; @@ -2820,13 +2773,13 @@ class rendering_window output (notebook : notebook) = refresh_proof output with InvokeTactics.RefreshSequentException e -> - output_html (outputhtml ()) + HelmLogger.log (`Error (`T ("An error occurred while refreshing the " ^ "sequent: " ^ Printexc.to_string e))) ; (*notebook#remove_all_pages ~skip_switch_page_event:false ;*) notebook#set_empty_page | InvokeTactics.RefreshProofException e -> - output_html (outputhtml ()) + HelmLogger.log (`Error (`T ("An error occurred while refreshing the proof: " ^ Printexc.to_string e))) ; output#unload ) in @@ -2863,12 +2816,11 @@ class rendering_window output (notebook : notebook) = let frame = GBin.frame ~shadow_type:`IN ~packing:(vboxl#pack ~expand:true ~padding:5) () in - let outputhtml = - new Ui_logger.html_logger + let _ = + new HelmGtkLogger.html_logger ~width:400 ~height: 100 ~show:true ~packing:frame#add () in object - method outputhtml = outputhtml method inputt = inputt method output = (output : TermViewer.proof_viewer) method scratch_window = scratch_window @@ -2890,30 +2842,29 @@ object let settings_window = new settings_window output scrolled_window0 (*export_to_postscript_menu_item*)() (choose_selection output) in set_settings_window settings_window ; - set_outputhtml outputhtml ; - ignore(window#event#connect#delete (fun _ -> GMain.Main.quit () ; true )) ; - CicLogger.log_callback := (outputhtml#log_cic_msg ~append_NL:true) + ignore(window#event#connect#delete (fun _ -> GMain.Main.quit () ; true )) end (* MAIN *) let initialize_everything () = - let module U = Unix in let output = TermViewer.proof_viewer ~width:350 ~height:280 () in let notebook = new notebook in - let rendering_window' = new rendering_window output notebook in - rendering_window'#set_auto_disambiguation !auto_disambiguation; - set_rendering_window rendering_window' ; - let print_error_as_html prefix msg = - output_html (outputhtml ()) (`Error (`T (prefix ^ msg))) - in - Gdome_xslt.setErrorCallback (Some (print_error_as_html "XSLT Error: ")); - Gdome_xslt.setDebugCallback - (Some (print_error_as_html "XSLT Debug Message: ")); - rendering_window'#show () ; - if restore_environment_on_boot && Sys.file_exists environmentfile then - restore_environment (); - GtkThread.main () + let rendering_window' = new rendering_window output notebook in + rendering_window'#set_auto_disambiguation !auto_disambiguation; + set_rendering_window rendering_window'; + let print_error_as_html prefix msg = + HelmLogger.log (`Error (`T (prefix ^ msg))) + in + Gdome_xslt.setErrorCallback (Some (print_error_as_html "XSLT Error: ")); + Gdome_xslt.setDebugCallback + (Some (print_error_as_html "XSLT Debug Message: ")); + rendering_window'#show () ; + if restore_environment_on_boot && + Sys.file_exists (Helm_registry.get "gtoplevel.environment_file") + then + restore_environment (); + GtkThread.main () ;; let main () =