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
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
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));
let _ = use_hint_callback := use_hint
end
+
+let start_web_services () = ignore (Unix.system "make -C ../hbugs/ start")
+let stop_web_services () = ignore (Unix.system "make -C ../hbugs/ stop")
+