X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FgTopLevel.ml;h=d3e39351c04804cf06a3c0fe8cfdbd21668fd6b7;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=e0e0bfca3385ec92996bd07da6ad0a4c4b8be674;hpb=8dc254e60fb7ee127568bf1b0e5050f49b5167e1;p=helm.git diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml index e0e0bfca3..d3e39351c 100644 --- a/helm/gTopLevel/gTopLevel.ml +++ b/helm/gTopLevel/gTopLevel.ml @@ -20,60 +20,52 @@ * MA 02111-1307, USA. * * For details, see the HELM World-Wide-Web page, - * http://cs.unibo.it/helm/. + * http://helm.cs.unibo.it/ *) -(******************************************************************************) -(* *) -(* PROJECT HELM *) -(* *) -(* Claudio Sacerdoti Coen *) -(* 06/01/2002 *) -(* *) -(* *) -(******************************************************************************) +(*****************************************************************************) +(* *) +(* PROJECT HELM *) +(* *) +(* Claudio Sacerdoti Coen *) +(* 06/01/2002 *) +(* *) +(* *) +(*****************************************************************************) 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 -(* DEBUGGING *) - module MQI = MQueryInterpreter module MQIC = MQIConn module MQGT = MQGTypes module MQGU = MQGUtil module MQG = MQueryGenerator -(* 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 xlinkns = Gdome.domString "http://www.w3.org/1999/xlink";; - -let prooffile = - try - Sys.getenv "GTOPLEVEL_PROOFFILE" - with - Not_found -> "/public/currentproof" +(* 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 ;; -let prooffiletype = - try - Sys.getenv "GTOPLEVEL_PROOFFILETYPE" - with - Not_found -> "/public/currentprooftype" -;; +(* GLOBAL CONSTANTS *) -let environmentfile = - try - Sys.getenv "GTOPLEVEL_ENVIRONMENTFILE" - with - Not_found -> "/public/environment" -;; +let mqi_handle = MQIC.init_if_connected () + +let dbd = + Mysql.quick_connect + ~host:(Helm_registry.get "db.host") + ~user:(Helm_registry.get "db.user") + ~database:(Helm_registry.get "db.database") + () let restore_environment_on_boot = true ;; let notify_hbugs_on_goal_change = false ;; @@ -108,18 +100,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) @@ -141,43 +121,11 @@ let argspec = in Arg.parse argspec ignore "" -(* MISC FUNCTIONS *) - -let term_of_cic_textual_parser_uri uri = - let module C = Cic in - let module CTP = CicTextualParser0 in - match uri with - CTP.ConUri uri -> C.Const (uri,[]) - | CTP.VarUri uri -> C.Var (uri,[]) - | CTP.IndTyUri (uri,tyno) -> C.MutInd (uri,tyno,[]) - | CTP.IndConUri (uri,tyno,consno) -> C.MutConstruct (uri,tyno,consno,[]) -;; - -let string_of_cic_textual_parser_uri uri = - let module C = Cic in - let module CTP = CicTextualParser0 in - let uri' = - match uri with - CTP.ConUri uri -> UriManager.string_of_uri uri - | CTP.VarUri uri -> UriManager.string_of_uri uri - | CTP.IndTyUri (uri,tyno) -> - UriManager.string_of_uri uri ^ "#1/" ^ string_of_int (tyno + 1) - | CTP.IndConUri (uri,tyno,consno) -> - UriManager.string_of_uri uri ^ "#1/" ^ string_of_int (tyno + 1) ^ "/" ^ - string_of_int consno - in - (* 4 = String.length "cic:" *) - 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 @@ -196,19 +144,18 @@ let check_window (outputhtml: Ui_logger.html_logger) uris = lazy (let mmlwidget = TermViewer.sequent_viewer + ~mml_of_cic_sequent:ApplyTransformation.mml_of_cic_sequent ~packing:scrolled_window#add ~width:400 ~height:280 () in let expr = - let term = - term_of_cic_textual_parser_uri - (MQueryMisc.cic_textual_parser_uri_of_string uri) - in - (Cic.Cast (term, CicTypeChecker.type_of_aux' [] [] term)) + let term = CicUtil.term_of_uri uri in + (Cic.Cast (term, fst(CicTypeChecker.type_of_aux' [] [] term + CicUniv.empty_ugraph ))) in try 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 +167,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 +177,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 +236,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 +350,7 @@ let interactive_interpretation_choice interpretations = GtkThread.main (); match !chosen with None -> raise NoChoice - | Some n -> n + | Some n -> [n] ;; @@ -428,16 +375,16 @@ let in (* innertypes *) let innertypesuri = UriManager.innertypesuri_of_uri uri in - Xml.pp ~quiet:true xmlinnertypes (Some (path ^ ".types.xml")) ; - Getter.register innertypesuri - (Configuration.annotations_url ^ + Xml.pp ~gzip:false xmlinnertypes (Some (path ^ ".types.xml")) ; + 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 ^ + Xml.pp ~gzip:false xml (Some (path ^ ".xml")) ; + Http_getter.register' uri + (Helm_registry.get "local_library.url" ^ Str.replace_first (Str.regexp "^cic:") "" (UriManager.string_of_uri uri) ^ ".xml" ) ; @@ -450,9 +397,9 @@ let None -> assert false | Some bodyuri -> bodyuri in - Xml.pp ~quiet:true bodyxml' (Some (path ^ ".body.xml")) ; - Getter.register bodyuri - (Configuration.annotations_url ^ + Xml.pp ~gzip:false bodyxml' (Some (path ^ ".body.xml")) ; + Http_getter.register' bodyuri + (Helm_registry.get "local_library.url" ^ Str.replace_first (Str.regexp "^cic:") "" (UriManager.string_of_uri bodyuri) ^ ".xml" ) @@ -465,7 +412,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 ;; @@ -478,7 +425,7 @@ let save_obj uri obj = (acic,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts, ids_to_inner_types,ids_to_conjectures,ids_to_hypotheses) = - Cic2acic.acic_object_of_cic_object obj + Cic2acic.acic_object_of_cic_object ~eta_fix:false obj in (* let's save the theorem and register it to the getter *) let pathname = pathname_of_annuri (UriManager.buri_of_uri uri) in @@ -488,41 +435,67 @@ let save_obj uri obj = ;; let qed () = - match ProofEngine.get_proof () with - None -> assert false - | Some (uri,[],bo,ty) -> - if - CicReduction.are_convertible [] - (CicTypeChecker.type_of_aux' [] [] bo) ty - then - begin - (*CSC: Wrong: [] is just plainly wrong *) - let proof = Cic.Constant (UriManager.name_of_uri uri,Some bo,ty,[]) in - let (acic,ids_to_inner_types,ids_to_inner_sorts) = - (rendering_window ())#output#load_proof uri proof - in - !qed_set_sensitive false ; - (* let's save the theorem and register it to the getter *) - let pathname = pathname_of_annuri (UriManager.buri_of_uri uri) in - make_dirs pathname ; - save_object_to_disk uri acic ids_to_inner_sorts ids_to_inner_types - pathname - end - else - raise WrongProof - | _ -> raise OpenConjecturesStillThere + match ProofEngine.get_proof () with + None -> assert false + | Some (uri,[],bo,ty) -> + let uri = match uri with Some uri -> uri | _ -> assert false in + (* we want to typecheck in the ENV *) + prerr_endline "-------------> QED"; + let ty_bo,u = + CicTypeChecker.type_of_aux' [] [] bo CicUniv.empty_ugraph in + let b,u1 = CicReduction.are_convertible [] ty_bo ty u in + if b then + begin + (*CSC: Wrong: [] is just plainly wrong *) + let proof = + Cic.Constant (UriManager.name_of_uri uri,Some bo,ty,[],[]) + in + let (acic,ids_to_inner_types,ids_to_inner_sorts) = + (rendering_window ())#output#load_proof proof + in + !qed_set_sensitive false ; + (* let's save the theorem and register it to the getter *) + let pathname = + pathname_of_annuri (UriManager.buri_of_uri uri) + in + let list_of_universes = + CicUnivUtils.universes_of_obj uri + (Cic.Constant ("",None,ty,[],[])) + in + let u1_clean = CicUniv.clean_ugraph u1 list_of_universes in + let u2 = CicUniv.fill_empty_nodes_with_uri u1_clean uri in + (********************************************** + TASSI: to uncomment whe universes will be ON + ***********************************************) + (* + make_dirs pathname ; + save_object_to_disk uri acic ids_to_inner_sorts + ids_to_inner_types pathname; + *) + (* save the universe graph u2 *) + (* add the object to the env *) + CicEnvironment.add_type_checked_term uri (( + Cic.Constant ((UriManager.name_of_uri uri), + (Some bo),ty,[],[])),u2); + (* FIXME: the variable list!! *) + prerr_endline "-------------> FINE"; + end + else + raise WrongProof + | _ -> raise OpenConjecturesStillThere ;; (** 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 ~gzip:false xml (Some proof_file_type) ; + HelmLogger.log + (`Msg (`T ("Current proof type saved to " ^ proof_file_type))) ; + Xml.pp ~gzip:false bodyxml (Some proof_file) ; + HelmLogger.log + (`Msg (`T ("Current proof body saved to " ^ proof_file))) ;; (* Used to typecheck the loaded proofs *) @@ -531,11 +504,11 @@ let typecheck_loaded_proof metasenv bo ty = ignore ( List.fold_left (fun metasenv ((_,context,ty) as conj) -> - ignore (T.type_of_aux' metasenv context ty) ; + ignore (T.type_of_aux' metasenv context ty CicUniv.empty_ugraph) ; metasenv @ [conj] ) [] metasenv) ; - ignore (T.type_of_aux' metasenv [] ty) ; - ignore (T.type_of_aux' metasenv [] bo) + ignore (T.type_of_aux' metasenv [] ty CicUniv.empty_ugraph) ; + ignore (T.type_of_aux' metasenv [] bo CicUniv.empty_ugraph) ;; let decompose_uris_choice_callback uris = @@ -543,9 +516,9 @@ let decompose_uris_choice_callback uris = let module U = UriManager in List.map (function uri -> - match MQueryMisc.cic_textual_parser_uri_of_string uri with - CicTextualParser0.IndTyUri (uri,typeno) -> (uri,typeno,[]) - | _ -> assert false) + match CicUtil.term_of_uri uri with + | Cic.MutInd (uri, typeno, _) -> (uri, typeno, []) + | _ -> assert false) (interactive_user_uri_choice ~selection_mode:`MULTIPLE ~ok:"Ok" ~enable_button_for_non_vars:false ~title:"Decompose" ~msg:"Please, select the Inductive Types to decompose" @@ -556,9 +529,9 @@ let decompose_uris_choice_callback uris = ) ;; -let mk_fresh_name_callback context name ~typ = +let mk_fresh_name_callback metasenv context name ~typ = let fresh_name = - match ProofEngineHelpers.mk_fresh_name context name ~typ with + match FreshNamesGenerator.mk_fresh_name ~subst:[] metasenv context name ~typ with Cic.Name fresh_name -> fresh_name | Cic.Anonymous -> assert false in @@ -587,16 +560,18 @@ let refresh_proof (output : TermViewer.proof_viewer) = else Hbugs.notify () ; (*CSC: Wrong: [] is just plainly wrong *) - uri, - (Cic.CurrentProof (UriManager.name_of_uri uri, metasenv, bo, ty, [])) + let uri = match uri with Some uri -> uri | _ -> assert false in + (uri, + Cic.CurrentProof (UriManager.name_of_uri uri,metasenv,bo,ty,[],[])) in - ignore (output#load_proof uri currentproof) + ignore (output#load_proof currentproof) with e -> match ProofEngine.get_proof () with None -> assert false | Some (uri,metasenv,bo,ty) -> - debug_print ("Offending proof: " ^ CicPp.ppobj (Cic.CurrentProof ("questa",metasenv,bo,ty,[]))); + debug_print ("Offending proof: " ^ + CicPp.ppobj (Cic.CurrentProof ("questa",metasenv,bo,ty,[],[]))); raise (InvokeTactics.RefreshProofException e) let set_proof_engine_goal g = @@ -642,7 +617,7 @@ let refresh_goals ?(empty_notebook=true) notebook = begin notebook#set_current_page ~may_skip_switch_page_event:true metano ; - notebook#proofw#load_sequent metasenv currentsequent + notebook#proofw#load_sequent metasenv currentsequent ; end with e -> @@ -681,7 +656,8 @@ 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 + let dbd = dbd end ;; module InvokeTactics' = InvokeTactics.Make (InvokeTacticsCallbacks);; @@ -690,9 +666,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 +674,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,10 +684,12 @@ 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 - Cic.CurrentProof (_,metasenv,bo,ty,_) -> + 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)) ; + ProofEngine.set_proof (Some (Some uri, metasenv, bo, ty)); refresh_proof output ; set_proof_engine_goal (match metasenv with @@ -722,25 +697,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 +769,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 +782,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 +804,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 +830,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 +839,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,37 +861,30 @@ 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, - ids_to_inner_types,ids_to_conjectures,ids_to_hypotheses) - = - Cic2acic.acic_object_of_cic_object obj - in - let mml = - ChosenTransformer.mml_of_cic_object - ~explode_all:false uri acic ids_to_inner_sorts ids_to_inner_types + let mml,(_,(ids_to_terms,ids_to_father_ids,ids_to_conjectures, + ids_to_hypotheses,_,_)) = + ApplyTransformation.mml_of_cic_object obj in window#set_title (UriManager.string_of_uri uri) ; window#misc#hide () ; window#show () ; - mmlwidget#load_doc mml ; + mmlwidget#load_root mml#get_documentElement ; with e -> - output_html outputhtml + HelmLogger.log (`Error (`T (Printexc.to_string e))) in let show_in_show_window_uri uri = - let obj = CicEnvironment.get_obj uri in + let obj,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in show_in_show_window_obj uri obj in - let show_in_show_window_callback mmlwidget (n : Gdome.element option) _ = + let show_in_show_window_callback mmlwidget ((n : Gdome.element option),_,_,_) = match n with None -> () | Some n' -> - if n'#hasAttributeNS ~namespaceURI:xlinkns ~localName:href then + if n'#hasAttributeNS ~namespaceURI:Misc.xlink_ns ~localName:href then let uri = - (n'#getAttributeNS ~namespaceURI:xlinkns ~localName:href)#to_string + (n'#getAttributeNS ~namespaceURI:Misc.xlink_ns ~localName:href)#to_string in show_in_show_window_uri (UriManager.uri_of_string uri) else @@ -952,23 +915,12 @@ 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 = - List.map - (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; + let uris = MetadataQuery.locate ~dbd id in + HelmLogger.log (`Msg (`T ("Locate Query: " ^ id))) ; + HelmLogger.log (`Msg (`T "Result:")) ; + List.iter (fun uri -> HelmLogger.log (`Msg (`T uri))) uris; user_uri_choice ~title:"Ambiguous input." - ~msg: - ("Ambiguous input \"" ^ id ^ - "\". Please, choose one interpetation:") + ~msg:(sprintf "Ambiguous input \"%s\". Please, choose one interpetation:" id) uris ;; @@ -1016,24 +968,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.Key_not_found _ -> + 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 @@ -1081,25 +1032,23 @@ exception AmbiguousInput;; (* A WIDGET TO ENTER CIC TERMS *) -module Callbacks = +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 ;; -module TermEditor' = ChosenTermEditor.Make(Callbacks);; +module TermEditor' = ChosenTermEditor.Make (DisambiguateCallbacks);; (* OTHER FUNCTIONS *) 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 +1059,7 @@ let locate () = inputt#set_term uri with e -> - output_html outputhtml + HelmLogger.log (`Error (`T (Printexc.to_string e))) ;; @@ -1120,7 +1069,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 +1155,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.Key_not_found _ -> get_uri := (function () -> uri) ; get_names := (function () -> names) ; inductive := inductiveb#active ; @@ -1219,7 +1166,7 @@ let new_inductive () = end with e -> - output_html outputhtml + HelmLogger.log (`Error (`T (Printexc.to_string e))) )) (* Second phase *) @@ -1240,7 +1187,7 @@ let new_inductive () = ~packing:(vbox#pack ~expand:true ~padding:0) () in let newinputt = TermEditor'.term_editor - mqi_handle + ~dbd ~width:400 ~height:20 ~packing:scrolled_window#add ~share_environment_with:inputt () ~isnotempty_callback: @@ -1281,7 +1228,7 @@ let new_inductive () = (fun name (newinputt,cons_names_entry) -> let consnamesstr = cons_names_entry#text in let cons_names = Str.split (Str.regexp " +") consnamesstr in - let metasenv,expr = + let metasenv,expr,ugraph = newinputt#get_metasenv_and_term ~context:[] ~metasenv:[] in match metasenv with @@ -1326,7 +1273,7 @@ let new_inductive () = window#destroy () with e -> - output_html outputhtml + HelmLogger.log (`Error (`T (Printexc.to_string e))) )) (* Third phase *) @@ -1352,7 +1299,7 @@ let new_inductive () = ~packing:(vbox#pack ~expand:true ~padding:0) () in let newinputt = TermEditor'.term_editor - mqi_handle + ~dbd ~width:400 ~height:20 ~packing:scrolled_window#add ~share_environment_with:inputt () ~isnotempty_callback: @@ -1383,7 +1330,7 @@ let new_inductive () = let cons_types = List.map2 (fun name inputt -> - let metasenv,expr = + let metasenv,expr,ugraph = inputt#get_metasenv_and_term ~context ~metasenv:[] in match metasenv with @@ -1400,7 +1347,7 @@ let new_inductive () = window2#destroy () with e -> - output_html outputhtml + HelmLogger.log (`Error (`T (Printexc.to_string e))) )) ; window2#show () ; @@ -1426,33 +1373,39 @@ let new_inductive () = (*CSC: Da finire *) let params = [] in let tys = !get_types_and_cons () in - let obj = Cic.InductiveDefinition(tys,params,!paramsno) in - begin - try - debug_print (CicPp.ppobj obj); - CicTypeChecker.typecheck_mutual_inductive_defs uri - (tys,params,!paramsno) ; - with - e -> - debug_print "Offending mutual (co)inductive type declaration:" ; - debug_print (CicPp.ppobj obj) ; - end ; + let obj = Cic.InductiveDefinition(tys,params,!paramsno,[]) in + let u = + begin + try + debug_print (CicPp.ppobj obj); + CicTypeChecker.typecheck_mutual_inductive_defs uri + (tys,params,!paramsno) CicUniv.empty_ugraph + with + e -> + debug_print "Offending mutual (co)inductive type declaration:" ; + debug_print (CicPp.ppobj obj) ; + (* I think we should fail here! *) + CicUniv.empty_ugraph + end + in (* We already know that obj is well-typed. We need to add it to the *) (* environment in order to compute the inner-types without having to *) (* debrujin it or having to modify lots of other functions to avoid *) (* asking the environment for the MUTINDs we are defining now. *) - CicEnvironment.put_inductive_definition uri obj ; + + (* u should be cleaned before adding it to the env *) + CicEnvironment.put_inductive_definition uri (obj,u) ; save_obj uri obj ; + (* TASSI: FIXME we should save the cleaned u here *) 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 @@ -1499,7 +1452,7 @@ let new_proof () = (* moved here to have visibility of the ok button *) let newinputt = TermEditor'.term_editor - mqi_handle + ~dbd ~width:400 ~height:100 ~packing:scrolled_window#add ~share_environment_with:inputt () ~isnotempty_callback: @@ -1522,7 +1475,7 @@ let new_proof () = (function () -> chosen := true ; try - let metasenv,parsed = newinputt#get_metasenv_and_term [] [] in + let metasenv,parsed,ugraph = newinputt#get_metasenv_and_term [] [] in let uristr = "cic:" ^ uri_entry#text in let uri = UriManager.uri_of_string uristr in if String.sub uristr (String.length uristr - 4) 4 <> ".con" then @@ -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.Key_not_found _ -> 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 () ; @@ -1550,7 +1502,7 @@ let new_proof () = let metasenv,expr = !get_metasenv_and_term () in let _ = CicTypeChecker.type_of_aux' metasenv [] expr in ProofEngine.set_proof - (Some (!get_uri (), (1,[],expr)::metasenv, Cic.Meta (1,[]), expr)) ; + (Some (Some (!get_uri ()), (1,[],expr)::metasenv, Cic.Meta (1,[]), expr)); set_proof_engine_goal (Some 1) ; refresh_goals notebook ; refresh_proof output ; @@ -1561,21 +1513,23 @@ 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))) ;; let check_term_in_scratch scratch_window metasenv context expr = try - let ty = CicTypeChecker.type_of_aux' metasenv context expr in + let ty,ugraph = + CicTypeChecker.type_of_aux' metasenv context expr CicUniv.empty_ugraph + in let expr = Cic.Cast (expr,ty) in scratch_window#show () ; scratch_window#set_term expr ; @@ -1590,7 +1544,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 -> [] @@ -1606,57 +1559,58 @@ let check scratch_window () = canonical_context in try - let metasenv',expr = inputt#get_metasenv_and_term context metasenv in - check_term_in_scratch scratch_window metasenv' context expr + let metasenv',expr,ugraph = + inputt#get_metasenv_and_term context metasenv + in + 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 let uri = input_or_locate_uri ~title:"Open" in - CicTypeChecker.typecheck uri ; + ignore(CicTypeChecker.typecheck uri CicUniv.empty_ugraph); + (* TASSI: typecheck mette la uri nell'env... cosa fa la open_ ?*) let metasenv,bo,ty = - match CicEnvironment.get_cooked_obj uri with - Cic.Constant (_,Some bo,ty,_) -> [],bo,ty - | Cic.CurrentProof (_,metasenv,bo,ty,_) -> metasenv,bo,ty + match fst(CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri ) with + Cic.Constant (_,Some bo,ty,_,_) -> [],bo,ty + | Cic.CurrentProof (_,metasenv,bo,ty,_,_) -> metasenv,bo,ty | Cic.Constant _ | Cic.Variable _ | Cic.InductiveDefinition _ -> raise NotADefinition in - ProofEngine.set_proof (Some (uri, metasenv, bo, ty)) ; + ProofEngine.set_proof (Some (Some uri, metasenv, bo, ty)) ; set_proof_engine_goal None ; refresh_goals notebook ; refresh_proof output ; !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))) ;; @@ -1689,16 +1643,13 @@ let show_query_results results = (clist#connect#select_row (fun ~row ~column ~event -> let (uristr,_) = List.nth results row in - match - MQueryMisc.cic_textual_parser_uri_of_string - (MQueryMisc.wrong_xpointer_format_from_wrong_xpointer_format' - uristr) - with - CicTextualParser0.ConUri uri - | CicTextualParser0.VarUri uri - | CicTextualParser0.IndTyUri (uri,_) - | CicTextualParser0.IndConUri (uri,_,_) -> + match CicUtil.term_of_uri uristr with + | Cic.Const (uri, _) + | Cic.Var (uri, _) + | Cic.MutInd (uri, _, _) + | Cic.MutConstruct (uri, _, _, _) -> show_in_show_window_uri uri + | _ -> assert false ) ) ; window#show () @@ -1898,9 +1849,9 @@ 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 metasenv,expr,ugraph = + inputt#get_metasenv_and_term ~context:[] ~metasenv:[] in let must = CGSearchPattern.get_constraints expr in let must',only = refine_constraints must in let query = @@ -1910,12 +1861,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 +1928,7 @@ let insertQuery () = show_query_results results with e -> - output_html outputhtml + HelmLogger.log (`Error (`T (Printexc.to_string e))) ;; @@ -2109,7 +2059,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 @@ -2119,12 +2068,7 @@ let searchPattern () = match !ProofEngine.goal with | None -> () | Some metano -> - let uris' = - TacticChaser.matchConclusion - mqi_handle - ~output_html:(fun m -> output_html outputhtml (`Msg (`T m))) - ~choose_must () ~status:(proof, metano) - in + let uris' = List.map fst (MetadataQuery.hint ~dbd (proof, metano)) in let uri' = user_uri_choice ~title:"Ambiguous input." ~msg: "Many lemmas can be successfully applied. Please, choose one:" @@ -2134,7 +2078,7 @@ let searchPattern () = InvokeTactics'.apply () with e -> - output_html outputhtml + HelmLogger.log (`Error (`T (Printexc.to_string e))) ;; @@ -2142,7 +2086,7 @@ let choose_selection mmlwidget (element : Gdome.element option) = let module G = Gdome in let rec aux element = if element#hasAttributeNS - ~namespaceURI:Misc.helmns + ~namespaceURI:Misc.helm_ns ~localName:(G.domString "xref") then mmlwidget#set_selection (Some element) @@ -2317,6 +2261,7 @@ class scratch_window = ~packing:(vbox#pack ~expand:true ~padding:5) () in let sequent_viewer = TermViewer.sequent_viewer + ~mml_of_cic_sequent:ApplyTransformation.mml_of_cic_sequent ~packing:(scrolled_window#add) ~width:400 ~height:280 () in object(self) val mutable term = Cic.Rel 1 (* dummy value *) @@ -2397,8 +2342,9 @@ object(self) GBin.scrolled_window ~border_width:10 ~packing:(vbox1#pack ~expand:true ~padding:5) () in let proofw = - TermViewer.sequent_viewer ~width:400 ~height:275 - ~packing:(scrolled_window1#add) () in + TermViewer.sequent_viewer + ~mml_of_cic_sequent:ApplyTransformation.mml_of_cic_sequent + ~width:400 ~height:275 ~packing:(scrolled_window1#add) () in let _ = proofw_ref <- Some proofw in let hbox3 = GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in @@ -2420,6 +2366,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 +2500,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) ; @@ -2573,8 +2523,9 @@ class empty_page = GBin.scrolled_window ~border_width:10 ~packing:(vbox1#pack ~expand:true ~padding:5) () in let proofw = - TermViewer.sequent_viewer ~width:400 ~height:275 - ~packing:(scrolled_window1#add) () in + TermViewer.sequent_viewer + ~mml_of_cic_sequent:ApplyTransformation.mml_of_cic_sequent + ~width:400 ~height:275 ~packing:(scrolled_window1#add) () in object(self) method proofw = (assert false : TermViewer.sequent_viewer) method content = vbox1 @@ -2641,29 +2592,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)))) ;; @@ -2813,20 +2760,19 @@ class rendering_window output (notebook : notebook) = factory3#add_item "Reload Stylesheets" ~callback: (function _ -> - ChosenTransformer.reload_stylesheets () ; if ProofEngine.get_proof () <> None then try refresh_goals 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 @@ -2850,7 +2796,7 @@ class rendering_window output (notebook : notebook) = ~packing:frame#add () in let inputt = TermEditor'.term_editor - mqi_handle + ~dbd ~width:400 ~height:100 ~packing:scrolled_window1#add () ~isnotempty_callback: (function b -> @@ -2863,12 +2809,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 +2835,33 @@ 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 output = + TermViewer.proof_viewer + ~mml_of_cic_object:ApplyTransformation.mml_of_cic_object + ~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 () = @@ -2924,6 +2872,7 @@ let main () = ;; try +(* CicEnvironment.set_trust (fun _ -> false); *) Sys.catch_break true; main (); with Sys.Break -> () (* exit nicely, invoking at_exit functions *)