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 ()
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
-