From c2809aab05acc486084279fa04fd63b10575c35a Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 16 Apr 2003 14:25:32 +0000 Subject: [PATCH] * Hbugs interface clean-up. * Moved every Hbugs.notify invocation into the refresh_proof function * Added a Hbugs.clear --- helm/gTopLevel/gTopLevel.ml | 29 +++--- helm/gTopLevel/hbugs.ml | 152 +++++++++++++++---------------- helm/gTopLevel/hbugs.mli | 17 ++-- helm/gTopLevel/invokeTactics.ml | 18 +--- helm/gTopLevel/invokeTactics.mli | 1 - 5 files changed, 103 insertions(+), 114 deletions(-) diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml index 1c81ddbbf..9bd242eb8 100644 --- a/helm/gTopLevel/gTopLevel.ml +++ b/helm/gTopLevel/gTopLevel.ml @@ -574,7 +574,17 @@ let refresh_proof (output : TermViewer.proof_viewer) = match !ProofEngine.proof with None -> assert false | Some (uri,metasenv,bo,ty) -> - !qed_set_sensitive (List.length metasenv = 0) ; + if List.length metasenv = 0 then + begin + !qed_set_sensitive true ; +prerr_endline "CSC: ###### REFRESH_PROOF, Hbugs.clear ()" ; + Hbugs.clear () + end + else +begin +prerr_endline "CSC: ###### REFRESH_PROOF, Hbugs.notify ()" ; + Hbugs.notify () ; +end ; (*CSC: Wrong: [] is just plainly wrong *) uri, (Cic.CurrentProof (UriManager.name_of_uri uri, metasenv, bo, ty, [])) @@ -647,7 +657,6 @@ let currentsequent = List.find (function (m,_,_) -> m=metano) metasenv in raise (InvokeTactics.RefreshSequentException e) with Not_found -> prerr_endline ("Offending sequent " ^ string_of_int metano ^ " unknown."); raise (InvokeTactics.RefreshSequentException e) -let __notify_hbugs = ref None;; module InvokeTacticsCallbacks = struct let sequent_viewer () = (rendering_window ())#notebook#proofw @@ -665,15 +674,11 @@ 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 notify_hbugs () = - match !__notify_hbugs with - | Some f -> f () - | None -> assert false end ;; module InvokeTactics' = InvokeTactics.Make (InvokeTacticsCallbacks);; -module Hbugs' = Hbugs.Make (InvokeTactics');; -__notify_hbugs := Some Hbugs'.notify;; +(* Just to initialize the Hbugs module *) +module Ignore = Hbugs.Initialize (InvokeTactics');; (** load an unfinished proof from filesystem *) let load_unfinished_proof () = @@ -707,7 +712,6 @@ let load_unfinished_proof () = ("

Current proof body loaded from " ^ prooffile ^ "

") ; !save_set_sensitive true; - Hbugs'.notify () | _ -> assert false with InvokeTactics.RefreshSequentException e -> @@ -1565,7 +1569,6 @@ let new_proof () = !save_set_sensitive true ; inputt#reset ; ProofEngine.intros ~mk_fresh_name_callback () ; - Hbugs'.notify (); refresh_goals notebook ; refresh_proof output with @@ -2748,7 +2751,7 @@ class rendering_window output (notebook : notebook) = let factory6 = new GMenu.factory hbugs_menu ~accel_group in let toggle_hbugs_menu_item = factory6#add_check_item - ~active:false ~key:GdkKeysyms._F5 ~callback:Hbugs'.toggle "HBugs enabled" + ~active:false ~key:GdkKeysyms._F5 ~callback:Hbugs.toggle "HBugs enabled" in (* settings menu *) let settings_menu = factory0#add_submenu "Settings" in @@ -2843,7 +2846,7 @@ let initialize_everything () = Gdome_xslt.setDebugCallback (Some (print_error_as_html "XSLT Debug Message: ")); rendering_window'#show () ; -(* Hbugs'.toggle true; *) +(* Hbugs.toggle true; *) GtkThread.main () ;; @@ -2857,7 +2860,7 @@ let main () = initialize_everything () ; if !usedb then Mqint.close (); prerr_endline "FOO"; - Hbugs'.quit () + Hbugs.quit () ;; try diff --git a/helm/gTopLevel/hbugs.ml b/helm/gTopLevel/hbugs.ml index b0ad35a74..5392fae85 100644 --- a/helm/gTopLevel/hbugs.ml +++ b/helm/gTopLevel/hbugs.ml @@ -36,59 +36,82 @@ let debug_print = exception NoProofInProgress;; -module type HbugsActions = - sig - val enable: unit -> unit - val disable: unit -> unit - val toggle: bool -> unit - - val quit: unit -> unit - - val notify: unit -> unit +let hbugs_client = ref None +let use_hint_callback = ref ignore + +let quit () = + match !hbugs_client with + | Some c -> c#unregisterFromBroker () + | None -> () + +let hbugs_enabled = ref false + +let get_hbugs_client () = + match !hbugs_client with + | Some c -> c + | None -> assert false + +let disable () = + match !hbugs_client with None -> () | Some c -> c#hide () + + (** send current proof assistant state to hbugs broker *) +let notify () = + try + if !hbugs_enabled then begin + let client = get_hbugs_client () in + let goal = + match !ProofEngine.goal with + | Some g -> g + | None -> raise NoProofInProgress + in + let (type_string, body_string) = + let (type_xml, body_xml) = ProofEngine.get_current_status_as_xml () in + (Xml.pp_to_string type_xml, Xml.pp_to_string body_xml) + in + let new_state = + (Misc.strip_xml_headings type_string, + Misc.strip_xml_headings body_string, + goal) + in + client#stateChange (Some new_state) + end + with NoProofInProgress -> () + +let clear () = + if !hbugs_enabled then + begin + let client = get_hbugs_client () in + client#stateChange None end -module Make (Tactics: InvokeTactics.Tactics) : HbugsActions = +let rec enable () = + (match !hbugs_client with + | None -> (* create an hbugs client and show its window *) + hbugs_client := + (try + Some (new Hbugs_client.hbugsClient + ~use_hint_callback:!use_hint_callback ()) + with e -> + prerr_endline (sprintf "Can't start HBugs client: %s" + (Printexc.to_string e)); + None); + (match !hbugs_client with + |Some client -> + client#show (); + client#subscribeAll () + | None -> ()) + | Some c -> (* show hbugs client window *) + c#show ()) + +let toggle state = + if state <> !hbugs_enabled then (* status has been changed *) + (if state then enable () else disable ()); + hbugs_enabled := state + +module type Unit = sig end + +module Initialize (Tactics: InvokeTactics.Tactics) : Unit = struct - let hbugs_client = ref None - - let quit () = - match !hbugs_client with - | Some c -> c#unregisterFromBroker () - | None -> () - - let hbugs_enabled = ref false - - let get_hbugs_client () = - match !hbugs_client with - | Some c -> c - | None -> assert false - - let disable () = - match !hbugs_client with None -> () | Some c -> c#hide () - - (** send current proof assistant state to hbugs broker *) - let notify () = - try - if !hbugs_enabled then begin - let client = get_hbugs_client () in - let goal = - match !ProofEngine.goal with - | Some g -> g - | None -> raise NoProofInProgress - in - let (type_string, body_string) = - let (type_xml, body_xml) = ProofEngine.get_current_status_as_xml () in - (Xml.pp_to_string type_xml, Xml.pp_to_string body_xml) - in - let new_state = - (Misc.strip_xml_headings type_string, - Misc.strip_xml_headings body_string, - goal) - in - client#stateChange new_state - end - with NoProofInProgress -> () - let use_hint = function | Use_ring_Luke -> Tactics.ring () | Use_fourier_Luke -> Tactics.fourier () @@ -110,32 +133,5 @@ module Make (Tactics: InvokeTactics.Tactics) : HbugsActions = Tactics.apply ~term () | Hints _ -> assert false - let rec enable () = - (match !hbugs_client with - | None -> (* create an hbugs client and show its window *) - hbugs_client := - (try - Some - (new Hbugs_client.hbugsClient - ~on_use_hint: use_hint - ~on_exit: ignore (* TODO disable hbugs on 'on_exit' callback *) - ()) - with e -> - prerr_endline (sprintf "Can't start HBugs client: %s" - (Printexc.to_string e)); - None); - (match !hbugs_client with - |Some client -> - client#show (); - client#subscribeAll () - | None -> ()) - | Some c -> (* show hbugs client window *) - c#show ()) - - let toggle state = - if state <> !hbugs_enabled then (* status has been changed *) - (if state then enable () else disable ()); - hbugs_enabled := state - + let _ = use_hint_callback := use_hint end - diff --git a/helm/gTopLevel/hbugs.mli b/helm/gTopLevel/hbugs.mli index 2982ba09b..022bbf43a 100644 --- a/helm/gTopLevel/hbugs.mli +++ b/helm/gTopLevel/hbugs.mli @@ -26,16 +26,15 @@ * http://helm.cs.unibo.it/ *) -module type HbugsActions = - sig - val enable: unit -> unit - val disable: unit -> unit - val toggle: bool -> unit +val enable: unit -> unit +val disable: unit -> unit +val toggle: bool -> unit - val quit: unit -> unit +val quit: unit -> unit - val notify: unit -> unit - end +val notify: unit -> unit +val clear: unit -> unit -module Make (Tactics: InvokeTactics.Tactics) : HbugsActions +module type Unit = sig end +module Initialize (Tactics: InvokeTactics.Tactics) : Unit diff --git a/helm/gTopLevel/invokeTactics.ml b/helm/gTopLevel/invokeTactics.ml index 775d6a468..318042909 100644 --- a/helm/gTopLevel/invokeTactics.ml +++ b/helm/gTopLevel/invokeTactics.ml @@ -62,8 +62,6 @@ module type Callbacks = (UriManager.uri * int * 'b list) list val mk_fresh_name_callback : Cic.context -> Cic.name -> typ:Cic.term -> Cic.name - (* invoked when the proof assistant's status has changed to notify Hbugs *) - val notify_hbugs : unit -> unit end ;; @@ -119,8 +117,7 @@ module Make (C: Callbacks) : Tactics = try tactic () ; C.refresh_goals () ; - C.refresh_proof () ; - C.notify_hbugs () + C.refresh_proof () with RefreshSequentException e -> C.output_html @@ -172,8 +169,7 @@ module Make (C: Callbacks) : Tactics = tactic expr ; C.refresh_goals () ; C.refresh_proof () ; - (C.term_editor ())#reset ; - C.notify_hbugs () + (C.term_editor ())#reset with RefreshSequentException e -> C.output_html @@ -207,8 +203,7 @@ module Make (C: Callbacks) : Tactics = try tactic term ; C.refresh_goals () ; - C.refresh_proof () ; - C.notify_hbugs () + C.refresh_proof () with RefreshSequentException e -> C.output_html @@ -252,7 +247,6 @@ module Make (C: Callbacks) : Tactics = tactic terms ; C.refresh_goals () ; C.refresh_proof () ; - C.notify_hbugs () with RefreshSequentException e -> C.output_html @@ -304,8 +298,7 @@ module Make (C: Callbacks) : Tactics = tactic ~goal_input:term ~input:expr ; C.refresh_goals () ; C.refresh_proof () ; - (C.term_editor ())#reset ; - C.notify_hbugs () + (C.term_editor ())#reset with RefreshSequentException e -> C.output_html @@ -391,8 +384,7 @@ module Make (C: Callbacks) : Tactics = try tactic hypothesis ; C.refresh_goals () ; - C.refresh_proof () ; - C.notify_hbugs () + C.refresh_proof () with RefreshSequentException e -> C.output_html diff --git a/helm/gTopLevel/invokeTactics.mli b/helm/gTopLevel/invokeTactics.mli index 11b8ecf72..2c11fb3d3 100644 --- a/helm/gTopLevel/invokeTactics.mli +++ b/helm/gTopLevel/invokeTactics.mli @@ -62,7 +62,6 @@ module type Callbacks = (UriManager.uri * int * 'b list) list val mk_fresh_name_callback : Cic.context -> Cic.name -> typ:Cic.term -> Cic.name - val notify_hbugs : unit -> unit end module type Tactics = -- 2.39.2