From fe1e7e151af9690f312259a4c1c969a1388bee5f Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Wed, 11 Feb 2004 12:03:40 +0000 Subject: [PATCH] new getter, logger, and the hell --- helm/gTopLevel/.depend | 6 +- helm/gTopLevel/Makefile | 15 +- helm/gTopLevel/batchParser.ml | 5 - helm/gTopLevel/gTopLevel.ml | 279 ++++++++++++----------------- helm/gTopLevel/invokeTactics.ml | 28 ++- helm/gTopLevel/invokeTactics.mli | 2 - helm/gTopLevel/oldDisambiguate.ml | 11 +- helm/gTopLevel/oldDisambiguate.mli | 1 - helm/gTopLevel/regtest.ml | 5 + helm/gTopLevel/testlibrary.ml | 10 +- 10 files changed, 152 insertions(+), 210 deletions(-) diff --git a/helm/gTopLevel/.depend b/helm/gTopLevel/.depend index bbc649700..f22b5a1ad 100644 --- a/helm/gTopLevel/.depend +++ b/helm/gTopLevel/.depend @@ -31,11 +31,13 @@ hbugs.cmo: invokeTactics.cmi proofEngine.cmi hbugs.cmi hbugs.cmx: invokeTactics.cmx proofEngine.cmx hbugs.cmi chosenTermEditor.cmo: termEditor.cmi chosenTermEditor.cmi chosenTermEditor.cmx: termEditor.cmx chosenTermEditor.cmi +helmGtkLogger.cmo: helmGtkLogger.cmi +helmGtkLogger.cmx: helmGtkLogger.cmi gTopLevel.cmo: chosenTermEditor.cmi chosenTransformer.cmi \ - disambiguatingParser.cmi hbugs.cmi invokeTactics.cmi \ + disambiguatingParser.cmi hbugs.cmi helmGtkLogger.cmi invokeTactics.cmi \ logicalOperations.cmi proofEngine.cmi termEditor.cmi termViewer.cmi gTopLevel.cmx: chosenTermEditor.cmx chosenTransformer.cmx \ - disambiguatingParser.cmx hbugs.cmx invokeTactics.cmx \ + disambiguatingParser.cmx hbugs.cmx helmGtkLogger.cmx invokeTactics.cmx \ logicalOperations.cmx proofEngine.cmx termEditor.cmx termViewer.cmx regtest.cmo: batchParser.cmi regtest.cmx: batchParser.cmx diff --git a/helm/gTopLevel/Makefile b/helm/gTopLevel/Makefile index 13d3507b5..9cba34bc7 100644 --- a/helm/gTopLevel/Makefile +++ b/helm/gTopLevel/Makefile @@ -1,5 +1,6 @@ BIN_DIR = /usr/local/bin TEST_REQUIRES = \ + helm-registry \ helm-mathql_interpreter \ helm-mathql_generator \ helm-tactics \ @@ -14,7 +15,8 @@ REQUIRES = \ gdome2-xslt \ hbugs-client PREDICATES = "gnome,init,glade" -OCAMLOPTIONS = -package "$(REQUIRES)" -predicates "$(PREDICATES)" -pp camlp4o +OCAMLOPTIONS = \ + -package "$(REQUIRES)" -predicates "$(PREDICATES)" -pp camlp4o -thread OCAMLFIND = ocamlfind OCAMLDEBUGOPTIONS = -g OCAMLC = $(OCAMLFIND) ocamlc $(OCAMLDEBUGOPTIONS) $(OCAMLOPTIONS) @@ -47,7 +49,8 @@ INTERFACE_FILES = \ termViewer.mli \ invokeTactics.mli \ hbugs.mli \ - chosenTermEditor.mli + chosenTermEditor.mli \ + helmGtkLogger.mli DEPOBJS = \ $(INTERFACE_FILES) $(INTERFACE_FILES:%.mli=%.ml) \ @@ -82,17 +85,17 @@ gTopLevel.opt: $(TOPLEVELOBJS:.cmo=.cmx) $(LIBRARIES_OPT) $(OCAMLOPT) -thread -linkpkg -o $@ $(TOPLEVELOBJS:.cmo=.cmx) testlibrary: $(TESTLIBOBJS) $(TEST_LIBRARIES) - $(OCAMLFIND) ocamlc $(OCAMLDEBUGOPTIONS) -linkpkg \ + $(OCAMLFIND) ocamlc -thread $(OCAMLDEBUGOPTIONS) -linkpkg \ -package "$(TEST_REQUIRES)" -o $@ $(TESTLIBOBJS) testlibrary.opt: $(TESTLIBOBJS:.cmo=.cmx) $(TEST_LIBRARIES_OPT) - $(OCAMLFIND) ocamlopt -linkpkg -package "$(TEST_REQUIRES)" -o $@ \ + $(OCAMLFIND) ocamlopt -thread -linkpkg -package "$(TEST_REQUIRES)" -o $@ \ $(TESTLIBOBJS:.cmo=.cmx) regtest: $(REGTESTOBJS) $(TEST_LIBRARIES) - $(OCAMLFIND) ocamlc $(OCAMLDEBUGOPTIONS) -linkpkg \ + $(OCAMLFIND) ocamlc -thread $(OCAMLDEBUGOPTIONS) -linkpkg \ -package "$(TEST_REQUIRES)" -o $@ $(REGTESTOBJS) regtest.opt: $(REGTESTOBJS:.cmo=.cmx) $(TEST_LIBRARIES_OPT) - $(OCAMLFIND) ocamlopt -linkpkg -package "$(TEST_REQUIRES)" -o $@ \ + $(OCAMLFIND) ocamlopt -thread -linkpkg -package "$(TEST_REQUIRES)" -o $@ \ $(REGTESTOBJS:.cmo=.cmx) .SUFFIXES: .ml .mli .cmo .cmi .cmx diff --git a/helm/gTopLevel/batchParser.ml b/helm/gTopLevel/batchParser.ml index bd7165bec..61220ecce 100644 --- a/helm/gTopLevel/batchParser.ml +++ b/helm/gTopLevel/batchParser.ml @@ -40,11 +40,6 @@ let uri_pred_of_conf tryvars varsprefix = module DisambiguateCallbacks = struct - let output_html ?(append_NL = true) msg = - if verbose then - (if append_NL then print_string else print_endline) - (Ui_logger.string_of_html_msg msg) - let interactive_user_uri_choice ~selection_mode ?ok ?enable_button_for_non_vars ~title ~msg ~id choices = List.filter !uri_predicate choices diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml index 03d12a4c5..c0aa8e830 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 @@ -48,33 +50,14 @@ module MQG = MQueryGenerator (* GLOBAL CONSTANTS *) +let configuration_file = "triciclo.conf.xml" + 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 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 +91,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 +141,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 +176,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 @@ -289,7 +257,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) ; @@ -429,15 +397,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 "annotations.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 "annotations.url" ^ Str.replace_first (Str.regexp "^cic:") "" (UriManager.string_of_uri uri) ^ ".xml" ) ; @@ -451,8 +419,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 "annotations.url" ^ Str.replace_first (Str.regexp "^cic:") "" (UriManager.string_of_uri bodyuri) ^ ".xml" ) @@ -465,7 +433,7 @@ exception OpenConjecturesStillThere;; exception WrongProof;; let pathname_of_annuri uristring = - Configuration.annotations_dir ^ + Helm_registry.get "annotations.dir" ^ Str.replace_first (Str.regexp "^cic:") "" uristring ;; @@ -515,14 +483,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 "triciclo.proof_file_type" in + let proof_file = Helm_registry.get "triciclo.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 +650,6 @@ 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 end ;; module InvokeTactics' = InvokeTactics.Make (InvokeTacticsCallbacks);; @@ -690,9 +658,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 +666,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 +676,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 "triciclo.proof_file_type" in + let proof_file = Helm_registry.get "triciclo.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 +689,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 +761,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 +774,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 +796,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 +822,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 +831,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 +853,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 +869,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 +913,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 +920,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 +975,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,7 +1041,6 @@ 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 @@ -1099,7 +1056,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 +1066,7 @@ let locate () = inputt#set_term uri with e -> - output_html outputhtml + HelmLogger.log (`Error (`T (Printexc.to_string e))) ;; @@ -1120,7 +1076,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 +1162,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 +1173,7 @@ let new_inductive () = end with e -> - output_html outputhtml + HelmLogger.log (`Error (`T (Printexc.to_string e))) )) (* Second phase *) @@ -1326,7 +1280,7 @@ let new_inductive () = window#destroy () with e -> - output_html outputhtml + HelmLogger.log (`Error (`T (Printexc.to_string e))) )) (* Third phase *) @@ -1400,7 +1354,7 @@ let new_inductive () = window2#destroy () with e -> - output_html outputhtml + HelmLogger.log (`Error (`T (Printexc.to_string e))) )) ; window2#show () ; @@ -1446,13 +1400,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 +1483,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 +1513,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 +1542,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 +1561,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 +1597,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 +1847,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 +1858,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 +1925,7 @@ let insertQuery () = show_query_results results with e -> - output_html outputhtml + HelmLogger.log (`Error (`T (Printexc.to_string e))) ;; @@ -2109,7 +2056,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,9 +2066,7 @@ let searchPattern () = | None -> () | Some metano -> let uris' = - TacticChaser.matchConclusion - mqi_handle - ~output_html:(fun m -> output_html outputhtml (`Msg (`T m))) + TacticChaser.matchConclusion mqi_handle ~choose_must () ~status:(proof, metano) in let uri' = @@ -2134,7 +2078,7 @@ let searchPattern () = InvokeTactics'.apply () with e -> - output_html outputhtml + HelmLogger.log (`Error (`T (Printexc.to_string e))) ;; @@ -2641,29 +2585,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 "triciclo.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 "triciclo.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 +2760,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 +2803,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 +2829,34 @@ 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 + 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 - 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 "triciclo.environment_file") + then + restore_environment (); + GtkThread.main () ;; let main () = diff --git a/helm/gTopLevel/invokeTactics.ml b/helm/gTopLevel/invokeTactics.ml index 2b0e58d21..5f01eff9f 100644 --- a/helm/gTopLevel/invokeTactics.ml +++ b/helm/gTopLevel/invokeTactics.ml @@ -53,8 +53,6 @@ module type Callbacks = 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 @@ -112,7 +110,7 @@ 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 = @@ -120,14 +118,14 @@ module Make (C: Callbacks) : Tactics = 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 ; @@ -194,8 +192,8 @@ module Make (C: Callbacks) : Tactics = 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 @@ -205,7 +203,7 @@ module Make (C: Callbacks) : Tactics = 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 () ; @@ -244,8 +242,8 @@ module Make (C: Callbacks) : Tactics = 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 @@ -263,15 +261,15 @@ module Make (C: Callbacks) : Tactics = 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 @@ -295,8 +293,8 @@ module Make (C: Callbacks) : Tactics = 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 = diff --git a/helm/gTopLevel/invokeTactics.mli b/helm/gTopLevel/invokeTactics.mli index a304e7e3b..41cc917b7 100644 --- a/helm/gTopLevel/invokeTactics.mli +++ b/helm/gTopLevel/invokeTactics.mli @@ -51,8 +51,6 @@ module type Callbacks = 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 diff --git a/helm/gTopLevel/oldDisambiguate.ml b/helm/gTopLevel/oldDisambiguate.ml index 82b918d68..39be585e5 100644 --- a/helm/gTopLevel/oldDisambiguate.ml +++ b/helm/gTopLevel/oldDisambiguate.ml @@ -40,7 +40,6 @@ open Printf module type Callbacks = sig - val output_html : ?append_NL:bool -> Ui_logger.html_msg -> unit val interactive_user_uri_choice : selection_mode:[`SINGLE | `MULTIPLE] -> ?ok:string -> @@ -68,12 +67,12 @@ module Make(C:Callbacks) = (function uri,_ -> MQueryMisc.wrong_xpointer_format_from_wrong_xpointer_format' uri ) result in - C.output_html (`Msg (`T "Locate query:")); + HelmLogger.log (`Msg (`T "Locate query:")); MQueryUtil.text_of_query - (fun s -> C.output_html ~append_NL:false (`Msg (`T s))) + (fun s -> HelmLogger.log ~append_NL:false (`Msg (`T s))) "" query; - C.output_html (`Msg (`T "Result:")); - MQueryUtil.text_of_result (fun s -> C.output_html (`Msg (`T s))) "" result; + HelmLogger.log (`Msg (`T "Result:")); + MQueryUtil.text_of_result (fun s -> HelmLogger.log (`Msg (`T s))) "" result; let uris' = match uris with [] -> @@ -140,7 +139,7 @@ module Make(C:Callbacks) = ) 1 list_of_uris in if tests_no > 1 then - C.output_html (`Msg (`T (sprintf + HelmLogger.log (`Msg (`T (sprintf "Disambiguation phase started: up to %d cases will be tried" tests_no))); (* and now we compute the list of all possible assignments from *) diff --git a/helm/gTopLevel/oldDisambiguate.mli b/helm/gTopLevel/oldDisambiguate.mli index 372f50085..8fcc1c934 100644 --- a/helm/gTopLevel/oldDisambiguate.mli +++ b/helm/gTopLevel/oldDisambiguate.mli @@ -38,7 +38,6 @@ module type Callbacks = sig - val output_html : ?append_NL:bool -> Ui_logger.html_msg -> unit val interactive_user_uri_choice : selection_mode:[`SINGLE | `MULTIPLE] -> ?ok:string -> diff --git a/helm/gTopLevel/regtest.ml b/helm/gTopLevel/regtest.ml index c146683ad..aebc74688 100644 --- a/helm/gTopLevel/regtest.ml +++ b/helm/gTopLevel/regtest.ml @@ -259,6 +259,11 @@ let main generate dump fnames tryvars varsprefix = end let _ = + Helm_registry.load_from "triciclo.conf.xml"; + HelmLogger.register_log_callback + (fun ?(append_NL = true) msg -> + (if append_NL then prerr_endline else prerr_string) + (HelmLogger.string_of_html_msg msg)); let fnames = ref [] in let gen = ref false in let tryvars = ref false in diff --git a/helm/gTopLevel/testlibrary.ml b/helm/gTopLevel/testlibrary.ml index 7f23b2f12..5abdec6e1 100644 --- a/helm/gTopLevel/testlibrary.ml +++ b/helm/gTopLevel/testlibrary.ml @@ -15,11 +15,6 @@ let uri_predicate = ref BatchParser.constants_only module DisambiguateCallbacks = struct - let output_html ?(append_NL = true) msg = - if verbose then - (if append_NL then print_string else print_endline) - (Ui_logger.string_of_html_msg msg) - let interactive_user_uri_choice ~selection_mode ?ok ?enable_button_for_non_vars ~title ~msg ~id choices = List.filter !uri_predicate choices @@ -132,6 +127,11 @@ let do_file status fname = fname (Printexc.to_string exn) let _ = + Helm_registry.load_from "triciclo.conf.xml"; + HelmLogger.register_log_callback + (fun ?(append_NL = true) msg -> + (if append_NL then prerr_endline else prerr_string) + (HelmLogger.string_of_html_msg msg)); let names = ref [] in let tryvars = ref false in let varsprefix = ref "" in -- 2.39.2