From 6bfd11a764024577d1a427d9b6e3074d66ff09fa Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Sun, 7 Sep 2003 09:50:09 +0000 Subject: [PATCH] added support for external configuration of describe_hint_callback --- helm/gTopLevel/hbugs.ml | 9 +++++++-- helm/gTopLevel/hbugs.mli | 7 +++++++ 2 files changed, 14 insertions(+), 2 deletions(-) diff --git a/helm/gTopLevel/hbugs.ml b/helm/gTopLevel/hbugs.ml index 19722a1d2..833d11bfd 100644 --- a/helm/gTopLevel/hbugs.ml +++ b/helm/gTopLevel/hbugs.ml @@ -31,13 +31,16 @@ open Printf;; let debug_print = let debug = true in - fun s -> prerr_endline (sprintf "DEBUG: %s" s) + fun s -> prerr_endline (sprintf "HBUGS DEBUG: %s" s) ;; exception NoProofInProgress;; let hbugs_client = ref None let use_hint_callback = ref ignore +let describe_hint_callback = ref ignore + +let set_describe_hint_callback c = describe_hint_callback := c let quit () = match !hbugs_client with @@ -89,7 +92,9 @@ let rec enable () = hbugs_client := (try Some (new Hbugs_client.hbugsClient - ~use_hint_callback:!use_hint_callback ()) + ~use_hint_callback:!use_hint_callback + ~describe_hint_callback:!describe_hint_callback + ()) with e -> prerr_endline (sprintf "Can't start HBugs client: %s" (Printexc.to_string e)); diff --git a/helm/gTopLevel/hbugs.mli b/helm/gTopLevel/hbugs.mli index b98a641af..70687afca 100644 --- a/helm/gTopLevel/hbugs.mli +++ b/helm/gTopLevel/hbugs.mli @@ -48,3 +48,10 @@ module Initialize (Tactics: InvokeTactics.Tactics) : Unit val start_web_services: unit -> unit val stop_web_services: unit -> unit +(* Other callbacks *) + +open Hbugs_types + + (* what to do when the user single click on an hint *) +val set_describe_hint_callback: (hint -> unit) -> unit + -- 2.39.2