match !ProofEngine.proof with
None -> assert false
| Some (uri,metasenv,bo,ty) ->
- !qed_set_sensitive (List.length metasenv = 0) ;
+ if List.length metasenv = 0 then
+ begin
+ !qed_set_sensitive true ;
+prerr_endline "CSC: ###### REFRESH_PROOF, Hbugs.clear ()" ;
+ Hbugs.clear ()
+ end
+ else
+begin
+prerr_endline "CSC: ###### REFRESH_PROOF, Hbugs.notify ()" ;
+ Hbugs.notify () ;
+end ;
(*CSC: Wrong: [] is just plainly wrong *)
uri,
(Cic.CurrentProof (UriManager.name_of_uri uri, metasenv, bo, ty, []))
raise (InvokeTactics.RefreshSequentException e)
with Not_found -> prerr_endline ("Offending sequent " ^ string_of_int metano ^ " unknown."); raise (InvokeTactics.RefreshSequentException e)
-let __notify_hbugs = ref None;;
module InvokeTacticsCallbacks =
struct
let sequent_viewer () = (rendering_window ())#notebook#proofw
let decompose_uris_choice_callback = decompose_uris_choice_callback
let mk_fresh_name_callback = mk_fresh_name_callback
let output_html msg = output_html (outputhtml ()) msg
- let notify_hbugs () =
- match !__notify_hbugs with
- | Some f -> f ()
- | None -> assert false
end
;;
module InvokeTactics' = InvokeTactics.Make (InvokeTacticsCallbacks);;
-module Hbugs' = Hbugs.Make (InvokeTactics');;
-__notify_hbugs := Some Hbugs'.notify;;
+(* Just to initialize the Hbugs module *)
+module Ignore = Hbugs.Initialize (InvokeTactics');;
(** load an unfinished proof from filesystem *)
let load_unfinished_proof () =
("<h1 color=\"Green\">Current proof body loaded from " ^
prooffile ^ "</h1>") ;
!save_set_sensitive true;
- Hbugs'.notify ()
| _ -> assert false
with
InvokeTactics.RefreshSequentException e ->
!save_set_sensitive true ;
inputt#reset ;
ProofEngine.intros ~mk_fresh_name_callback () ;
- Hbugs'.notify ();
refresh_goals notebook ;
refresh_proof output
with
let factory6 = new GMenu.factory hbugs_menu ~accel_group in
let toggle_hbugs_menu_item =
factory6#add_check_item
- ~active:false ~key:GdkKeysyms._F5 ~callback:Hbugs'.toggle "HBugs enabled"
+ ~active:false ~key:GdkKeysyms._F5 ~callback:Hbugs.toggle "HBugs enabled"
in
(* settings menu *)
let settings_menu = factory0#add_submenu "Settings" in
Gdome_xslt.setDebugCallback
(Some (print_error_as_html "XSLT Debug Message: "));
rendering_window'#show () ;
-(* Hbugs'.toggle true; *)
+(* Hbugs.toggle true; *)
GtkThread.main ()
;;
initialize_everything () ;
if !usedb then Mqint.close ();
prerr_endline "FOO";
- Hbugs'.quit ()
+ Hbugs.quit ()
;;
try
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
-
(UriManager.uri * int * 'b list) list
val mk_fresh_name_callback :
Cic.context -> Cic.name -> typ:Cic.term -> Cic.name
- (* invoked when the proof assistant's status has changed to notify Hbugs *)
- val notify_hbugs : unit -> unit
end
;;
try
tactic () ;
C.refresh_goals () ;
- C.refresh_proof () ;
- C.notify_hbugs ()
+ C.refresh_proof ()
with
RefreshSequentException e ->
C.output_html
tactic expr ;
C.refresh_goals () ;
C.refresh_proof () ;
- (C.term_editor ())#reset ;
- C.notify_hbugs ()
+ (C.term_editor ())#reset
with
RefreshSequentException e ->
C.output_html
try
tactic term ;
C.refresh_goals () ;
- C.refresh_proof () ;
- C.notify_hbugs ()
+ C.refresh_proof ()
with
RefreshSequentException e ->
C.output_html
tactic terms ;
C.refresh_goals () ;
C.refresh_proof () ;
- C.notify_hbugs ()
with
RefreshSequentException e ->
C.output_html
tactic ~goal_input:term ~input:expr ;
C.refresh_goals () ;
C.refresh_proof () ;
- (C.term_editor ())#reset ;
- C.notify_hbugs ()
+ (C.term_editor ())#reset
with
RefreshSequentException e ->
C.output_html
try
tactic hypothesis ;
C.refresh_goals () ;
- C.refresh_proof () ;
- C.notify_hbugs ()
+ C.refresh_proof ()
with
RefreshSequentException e ->
C.output_html
projects / helm.git / commitdiff