;;
exception NoProofInProgress;;
let hbugs_client = ref None
let use_hint_callback = ref ignore
;;
exception NoProofInProgress;;
let hbugs_client = ref None
let use_hint_callback = ref ignore
- 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 -> ()
+ 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 -> ()
- (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 ())
+ (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
+ ~describe_hint_callback:!describe_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 ())
- if state <> !hbugs_enabled then (* status has been changed *)
- (if state then enable () else disable ());
- hbugs_enabled := state
+ if state <> !hbugs_enabled then begin (* status has been changed *)
+ if state then enable () else disable ();
+ clear ()
+ end;
+ hbugs_enabled := state
- | Use_ring_Luke -> Tactics.ring ()
- | Use_fourier_Luke -> Tactics.fourier ()
- | Use_reflexivity_Luke -> Tactics.reflexivity ()
- | Use_symmetry_Luke -> Tactics.symmetry ()
- | Use_assumption_Luke -> Tactics.assumption ()
- | Use_contradiction_Luke -> Tactics.contradiction ()
- | Use_exists_Luke -> Tactics.exists ()
- | Use_split_Luke -> Tactics.split ()
- | Use_left_Luke -> Tactics.left ()
- | Use_right_Luke -> Tactics.right ()
- | Use_apply_Luke term ->
+ | Use_ring -> Tactics.ring ()
+ | Use_fourier -> Tactics.fourier ()
+ | Use_reflexivity -> Tactics.reflexivity ()
+ | Use_symmetry -> Tactics.symmetry ()
+ | Use_assumption -> Tactics.assumption ()
+ | Use_contradiction -> Tactics.contradiction ()
+ | Use_exists -> Tactics.exists ()
+ | Use_split -> Tactics.split ()
+ | Use_left -> Tactics.left ()
+ | Use_right -> Tactics.right ()
+ | Use_apply term ->
(* we remove the "cic:" prefix *)
let term' = String.sub term 4 (String.length term - 4) in
Tactics.apply ~term:term' ()
(* we remove the "cic:" prefix *)
let term' = String.sub term 4 (String.length term - 4) in
Tactics.apply ~term:term' ()