-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