X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FgTopLevel.ml;h=1726725c15370b146e42439def72b6b34c23c655;hb=36f71caeee72cb15185ecbc7644ed1da5c6f8186;hp=7eab7b1ef086f09b68f9223b90f1d68b5650725c;hpb=8498344c49c66aa84cf7484fdbd9c292f9aae5c6;p=helm.git diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml index 7eab7b1ef..1726725c1 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,38 +48,29 @@ 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 ;; +let auto_disambiguation = ref true ;; + (* GLOBAL REFERENCES (USED BY CALLBACKS) *) let check_term = ref (fun _ _ _ -> assert false);; @@ -106,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) @@ -168,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 @@ -194,6 +172,7 @@ let check_window (outputhtml: Ui_logger.html_logger) uris = lazy (let mmlwidget = TermViewer.sequent_viewer + ~mml_of_cic_sequent:ChosenTransformer.mml_of_cic_sequent ~packing:scrolled_window#add ~width:400 ~height:280 () in let expr = let term = @@ -206,7 +185,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 @@ -218,114 +197,135 @@ 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 choices = ref [] in - let chosen = ref false in - let use_only_constants = ref false in - let window = - GWindow.dialog ~modal:true ~title ~width:600 () in - let lMessage = - GMisc.label ~text:msg - ~packing:(window#vbox#pack ~expand:false ~fill:false ~padding:5) () in - let scrolled_window = - GBin.scrolled_window ~border_width:10 - ~packing:(window#vbox#pack ~expand:true ~fill:true ~padding:5) () in - let clist = - let expected_height = 18 * List.length uris in - let height = if expected_height > 400 then 400 else expected_height in - GList.clist ~columns:1 ~packing:scrolled_window#add - ~height ~selection_mode:(selection_mode :> Gtk.Tags.selection_mode) () in - let _ = List.map (function x -> clist#append [x]) uris in - let hbox2 = - GPack.hbox ~border_width:0 - ~packing:(window#vbox#pack ~expand:false ~fill:false ~padding:5) () in - let explain_label = - GMisc.label ~text:"None of the above. Try this one:" - ~packing:(hbox2#pack ~expand:false ~fill:false ~padding:5) () in - let manual_input = - GEdit.entry ~editable:true - ~packing:(hbox2#pack ~expand:true ~fill:true ~padding:5) () in - let hbox = - GPack.hbox ~border_width:0 ~packing:window#action_area#add () in - let okb = - GButton.button ~label:ok - ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in - let _ = okb#misc#set_sensitive false in - let nonvarsb = - GButton.button - ~packing: - (function w -> - if enable_button_for_non_vars then - hbox#pack ~expand:false ~fill:false ~padding:5 w) - ~label:"Try constants only" () in - let checkb = - GButton.button ~label:"Check" - ~packing:(hbox#pack ~padding:5) () in - let _ = checkb#misc#set_sensitive false in - let cancelb = - GButton.button ~label:"Abort" - ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in - (* actions *) - let check_callback () = - assert (List.length !choices > 0) ; - check_window (outputhtml ()) !choices + let only_constant_choices = + lazy + (List.filter + (fun uri -> not (String.sub uri (String.length uri - 4) 4 = ".var")) + uris) in - ignore (window#connect#destroy GMain.Main.quit) ; - ignore (cancelb#connect#clicked window#destroy) ; - ignore - (okb#connect#clicked (function () -> chosen := true ; window#destroy ())) ; - ignore - (nonvarsb#connect#clicked - (function () -> - use_only_constants := true ; - chosen := true ; - window#destroy () - )) ; - ignore (checkb#connect#clicked check_callback) ; - ignore - (clist#connect#select_row - (fun ~row ~column ~event -> - checkb#misc#set_sensitive true ; - okb#misc#set_sensitive true ; - choices := (List.nth uris row)::!choices)) ; - ignore - (clist#connect#unselect_row - (fun ~row ~column ~event -> - choices := - List.filter (function uri -> uri != (List.nth uris row)) !choices)) ; - ignore - (manual_input#connect#changed - (fun _ -> - if manual_input#text = "" then - begin - choices := [] ; - checkb#misc#set_sensitive false ; - okb#misc#set_sensitive false ; - clist#misc#set_sensitive true - end - else - begin - choices := [manual_input#text] ; - clist#unselect_all () ; + if selection_mode <> `SINGLE && !auto_disambiguation then + Lazy.force only_constant_choices + else begin + let choices = ref [] in + let chosen = ref false in + let use_only_constants = ref false in + let window = + GWindow.dialog ~modal:true ~title ~width:600 () in + let lMessage = + GMisc.label ~text:msg + ~packing:(window#vbox#pack ~expand:false ~fill:false ~padding:5) () in + let scrolled_window = + GBin.scrolled_window ~border_width:10 + ~packing:(window#vbox#pack ~expand:true ~fill:true ~padding:5) () in + let clist = + let expected_height = 18 * List.length uris in + let height = if expected_height > 400 then 400 else expected_height in + GList.clist ~columns:1 ~packing:scrolled_window#add + ~height ~selection_mode:(selection_mode :> Gtk.Tags.selection_mode) () in + let _ = List.map (function x -> clist#append [x]) uris in + let hbox2 = + GPack.hbox ~border_width:0 + ~packing:(window#vbox#pack ~expand:false ~fill:false ~padding:5) () in + let explain_label = + GMisc.label ~text:"None of the above. Try this one:" + ~packing:(hbox2#pack ~expand:false ~fill:false ~padding:5) () in + let manual_input = + GEdit.entry ~editable:true + ~packing:(hbox2#pack ~expand:true ~fill:true ~padding:5) () in + let hbox = + GPack.hbox ~border_width:0 ~packing:window#action_area#add () in + let okb = + GButton.button ~label:ok + ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in + let _ = okb#misc#set_sensitive false in + let nonvarsb = + GButton.button + ~packing: + (function w -> + if enable_button_for_non_vars then + hbox#pack ~expand:false ~fill:false ~padding:5 w) + ~label:"Try constants only" () in + let autob = + GButton.button + ~packing: + (fun w -> + if enable_button_for_non_vars then + hbox#pack ~expand:false ~fill:false ~padding:5 w) + ~label:"Auto" () in + let checkb = + GButton.button ~label:"Check" + ~packing:(hbox#pack ~padding:5) () in + let _ = checkb#misc#set_sensitive false in + let cancelb = + GButton.button ~label:"Abort" + ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in + (* actions *) + let check_callback () = + assert (List.length !choices > 0) ; + check_window !choices + in + ignore (window#connect#destroy GMain.Main.quit) ; + ignore (cancelb#connect#clicked window#destroy) ; + ignore + (okb#connect#clicked (function () -> chosen := true ; window#destroy ())) ; + ignore + (nonvarsb#connect#clicked + (function () -> + use_only_constants := true ; + chosen := true ; + window#destroy () + )) ; + ignore (autob#connect#clicked (fun () -> + auto_disambiguation := true; + (rendering_window ())#set_auto_disambiguation true; + use_only_constants := true ; + chosen := true; + window#destroy ())); + ignore (checkb#connect#clicked check_callback) ; + ignore + (clist#connect#select_row + (fun ~row ~column ~event -> checkb#misc#set_sensitive true ; okb#misc#set_sensitive true ; - clist#misc#set_sensitive false - end)); - window#set_position `CENTER ; - window#show () ; - GtkThread.main (); - if !chosen then - if !use_only_constants then - List.filter - (function uri -> not (String.sub uri (String.length uri - 4) 4 = ".var")) - uris - else - if List.length !choices > 0 then !choices else raise NoChoice - else - raise NoChoice + choices := (List.nth uris row)::!choices)) ; + ignore + (clist#connect#unselect_row + (fun ~row ~column ~event -> + choices := + List.filter (function uri -> uri != (List.nth uris row)) !choices)) ; + ignore + (manual_input#connect#changed + (fun _ -> + if manual_input#text = "" then + begin + choices := [] ; + checkb#misc#set_sensitive false ; + okb#misc#set_sensitive false ; + clist#misc#set_sensitive true + end + else + begin + choices := [manual_input#text] ; + clist#unselect_all () ; + checkb#misc#set_sensitive true ; + okb#misc#set_sensitive true ; + clist#misc#set_sensitive false + end)); + window#set_position `CENTER ; + window#show () ; + GtkThread.main (); + if !chosen then + if !use_only_constants then + Lazy.force only_constant_choices + else + if List.length !choices > 0 then !choices else raise NoChoice + else + raise NoChoice + end ;; let interactive_interpretation_choice interpretations = @@ -380,7 +380,7 @@ let interactive_interpretation_choice interpretations = GtkThread.main (); match !chosen with None -> raise NoChoice - | Some n -> n + | Some n -> [n] ;; @@ -406,15 +406,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" ) ; @@ -428,8 +428,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" ) @@ -442,7 +442,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 ;; @@ -455,7 +455,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 @@ -468,6 +468,7 @@ let qed () = match ProofEngine.get_proof () with None -> assert false | Some (uri,[],bo,ty) -> + let uri = match uri with Some uri -> uri | _ -> assert false in if CicReduction.are_convertible [] (CicTypeChecker.type_of_aux' [] [] bo) ty @@ -492,14 +493,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 *) @@ -533,9 +535,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 metasenv context name ~typ with Cic.Name fresh_name -> fresh_name | Cic.Anonymous -> assert false in @@ -564,8 +566,9 @@ 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) with @@ -658,7 +661,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);; @@ -667,9 +670,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] | _ -> ()) ;; *) @@ -677,7 +678,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 @@ -688,10 +688,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 + 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 @@ -699,25 +701,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))) ;; @@ -773,7 +773,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) @@ -786,22 +786,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))) ;; @@ -809,22 +808,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))) ;; @@ -836,7 +834,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 @@ -846,11 +843,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))) ;; @@ -868,7 +865,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, @@ -885,7 +881,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 = @@ -929,8 +925,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 = @@ -938,10 +932,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 ^ @@ -993,24 +987,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 @@ -1058,25 +1051,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 TexTermEditor' = 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:" @@ -1087,7 +1078,7 @@ let locate () = inputt#set_term uri with e -> - output_html outputhtml + HelmLogger.log (`Error (`T (Printexc.to_string e))) ;; @@ -1097,7 +1088,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 @@ -1184,10 +1174,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 ; @@ -1196,7 +1185,7 @@ let new_inductive () = end with e -> - output_html outputhtml + HelmLogger.log (`Error (`T (Printexc.to_string e))) )) (* Second phase *) @@ -1216,7 +1205,7 @@ let new_inductive () = GBin.scrolled_window ~border_width:5 ~packing:(vbox#pack ~expand:true ~padding:0) () in let newinputt = - TexTermEditor'.term_editor + TermEditor'.term_editor mqi_handle ~width:400 ~height:20 ~packing:scrolled_window#add ~share_environment_with:inputt () @@ -1303,7 +1292,7 @@ let new_inductive () = window#destroy () with e -> - output_html outputhtml + HelmLogger.log (`Error (`T (Printexc.to_string e))) )) (* Third phase *) @@ -1328,7 +1317,7 @@ let new_inductive () = GBin.scrolled_window ~border_width:5 ~packing:(vbox#pack ~expand:true ~padding:0) () in let newinputt = - TexTermEditor'.term_editor + TermEditor'.term_editor mqi_handle ~width:400 ~height:20 ~packing:scrolled_window#add ~share_environment_with:inputt () @@ -1377,7 +1366,7 @@ let new_inductive () = window2#destroy () with e -> - output_html outputhtml + HelmLogger.log (`Error (`T (Printexc.to_string e))) )) ; window2#show () ; @@ -1423,13 +1412,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 @@ -1475,7 +1463,7 @@ let new_proof () = ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in (* moved here to have visibility of the ok button *) let newinputt = - TexTermEditor'.term_editor + TermEditor'.term_editor mqi_handle ~width:400 ~height:100 ~packing:scrolled_window#add ~share_environment_with:inputt () @@ -1507,17 +1495,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 () ; @@ -1527,7 +1514,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 ; @@ -1538,15 +1525,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))) ;; @@ -1567,7 +1554,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 -> [] @@ -1587,24 +1573,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 @@ -1618,22 +1602,22 @@ let open_ () = | 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))) ;; @@ -1875,7 +1859,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 @@ -1887,12 +1870,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 = @@ -1955,7 +1937,7 @@ let insertQuery () = show_query_results results with e -> - output_html outputhtml + HelmLogger.log (`Error (`T (Printexc.to_string e))) ;; @@ -2086,7 +2068,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 @@ -2097,10 +2078,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." @@ -2111,7 +2090,7 @@ let searchPattern () = InvokeTactics'.apply () with e -> - output_html outputhtml + HelmLogger.log (`Error (`T (Printexc.to_string e))) ;; @@ -2294,6 +2273,7 @@ class scratch_window = ~packing:(vbox#pack ~expand:true ~padding:5) () in let sequent_viewer = TermViewer.sequent_viewer + ~mml_of_cic_sequent:ChosenTransformer.mml_of_cic_sequent ~packing:(scrolled_window#add) ~width:400 ~height:280 () in object(self) val mutable term = Cic.Rel 1 (* dummy value *) @@ -2374,8 +2354,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:ChosenTransformer.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 @@ -2397,6 +2378,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 = @@ -2528,6 +2512,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) ; @@ -2550,8 +2535,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:ChosenTransformer.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 @@ -2618,29 +2604,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)))) ;; @@ -2778,6 +2760,9 @@ class rendering_window output (notebook : notebook) = let _ = factory3#add_item "Clear Aliases" ~key:GdkKeysyms._K ~callback:clear_aliases in + let autoitem = + factory3#add_check_item "Auto disambiguation" + ~callback:(fun checked -> auto_disambiguation := checked) in let _ = factory3#add_separator () in let _ = factory3#add_item "MathML Widget Preferences..." ~key:GdkKeysyms._P @@ -2794,13 +2779,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 @@ -2823,7 +2808,7 @@ class rendering_window output (notebook : notebook) = GBin.scrolled_window ~border_width:5 ~packing:frame#add () in let inputt = - TexTermEditor'.term_editor + TermEditor'.term_editor mqi_handle ~width:400 ~height:100 ~packing:scrolled_window1#add () ~isnotempty_callback: @@ -2837,17 +2822,17 @@ 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 method notebook = notebook method show = window#show + method set_auto_disambiguation set = autoitem#set_active set initializer notebook#set_empty_page ; (*export_to_postscript_menu_item#misc#set_sensitive false ;*) @@ -2863,29 +2848,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:ChosenTransformer.mml_of_cic_object + ~width:350 ~height:280 () + in let notebook = new notebook in - let rendering_window' = new rendering_window output notebook in - 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 () =