HBugs compile again (but it does not do anything right now: still to be

ported correctly to lablgtk2)

diff --git a/helm/gTopLevel/Makefile b/helm/gTopLevel/Makefile
index 6c2e311d5d8e6350d6c79047d6f753823b03b4eb..9c9aaea62093ff46d45db89e6b32c21e426830ac 100644 (file)
--- a/helm/gTopLevel/Makefile
+++ b/helm/gTopLevel/Makefile
@@ -1,9 +1,8 @@
 BIN_DIR = /usr/local/bin
-#helm-tactics threads hbugs-client mathml-editor
 REQUIRES = lablgtkmathview helm-cic_textual_parser helm-tex_cic_textual_parser \
            helm-cic_proof_checking helm-xml gdome2-xslt helm-cic_unification \
            helm-mathql helm-mathql_interpreter helm-mathql_generator \
-                helm-tactics threads mathml-editor \
+                helm-tactics threads hbugs-client mathml-editor \
            helm-cic_transformations
 PREDICATES = "gnome,init,glade"
 OCAMLOPTIONS = -package "$(REQUIRES)" -predicates "$(PREDICATES)" -pp camlp4o
@@ -19,15 +18,14 @@ all: styles gTopLevel
 opt: styles gTopLevel.opt
 
 start:
-       echo $(MAKE) -C ../hbugs/ start
+       $(MAKE) -C ../hbugs/ start
 stop:
-       echo $(MAKE) -C ../hbugs/ stop
+       $(MAKE) -C ../hbugs/ stop
 
-# invokeTactics.mli hbugs.mli
 INTERFACE_FILES = \
        proofEngine.mli logicalOperations.mli disambiguate.mli \
        termEditor.mli texTermEditor.mli xmlDiff.mli termViewer.mli \
-       invokeTactics.mli
+       invokeTactics.mli hbugs.mli
 
 DEPOBJS = $(INTERFACE_FILES) $(INTERFACE_FILES:%.mli=%.ml) gTopLevel.ml
 

diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index 6aaec3aeda401c9e0f3f0472ebf4e2a3330cc5de..88d819fded0abd67afdc1a8f4a8dce14af9f1835 100644 (file)
--- a/helm/gTopLevel/gTopLevel.ml
+++ b/helm/gTopLevel/gTopLevel.ml
@@ -572,10 +572,10 @@ let refresh_proof (output : TermViewer.proof_viewer) =
        if List.length metasenv = 0 then
         begin
          !qed_set_sensitive true ;
-         (*Hbugs.clear*) ()
+         Hbugs.clear ()
         end
        else
-        (*Hbugs.notify*) () ;
+        Hbugs.notify () ;
        (*CSC: Wrong: [] is just plainly wrong *)
        uri,
         (Cic.CurrentProof (UriManager.name_of_uri uri, metasenv, bo, ty, []))
@@ -674,7 +674,6 @@ module InvokeTacticsCallbacks =
 module InvokeTactics' = InvokeTactics.Make (InvokeTacticsCallbacks);;
 
 (* Just to initialize the Hbugs module *)
-(*
 module Ignore = Hbugs.Initialize (InvokeTactics');;
 Hbugs.set_describe_hint_callback (fun hint ->
   match hint with
@@ -683,7 +682,6 @@ Hbugs.set_describe_hint_callback (fun hint ->
       check_window outputhtml [term]
   | _ -> ())
 ;;
-*)
 
 let dummy_uri = "/dummy.con"
 
@@ -2666,7 +2664,7 @@ object(self)
           Lazy.force (page#compute) ;
           Lazy.force setgoal;
           if notify_hbugs_on_goal_change then
-            (*Hbugs.notify *) ()
+            Hbugs.notify ()
         with _ -> ()
     ))
 end
@@ -2860,18 +2858,18 @@ class rendering_window output (notebook : notebook) =
  let factory6 = new GMenu.factory hbugs_menu ~accel_group in
  let _ =
   factory6#add_check_item
-    ~active:false ~key:GdkKeysyms._F5 ~callback:(*Hbugs.toggle*)(fun _ -> ()) "HBugs enabled"
+    ~active:false ~key:GdkKeysyms._F5 ~callback:Hbugs.toggle "HBugs enabled"
  in
  let _ =
-  factory6#add_item ~key:GdkKeysyms._Return ~callback:(*Hbugs.notify*)(fun _ -> ())
+  factory6#add_item ~key:GdkKeysyms._Return ~callback:Hbugs.notify
    "(Re)Submit status!"
  in
  let _ = factory6#add_separator () in
  let _ =
-  factory6#add_item ~callback:(*Hbugs.start_web_services*)(fun _ -> ()) "Start Web Services"
+  factory6#add_item ~callback:Hbugs.start_web_services "Start Web Services"
  in
  let _ =
-  factory6#add_item ~callback:(*Hbugs.stop_web_services*)(fun _ -> ()) "Stop Web Services"
+  factory6#add_item ~callback:Hbugs.stop_web_services "Stop Web Services"
  in
  (* settings menu *)
  let settings_menu = factory0#add_submenu "Settings" in
@@ -2995,8 +2993,8 @@ let initialize_everything () =
 let main () =
  ignore (GtkMain.Main.init ()) ;
  initialize_everything () ;
- MQIC.close mqi_handle(*;
- Hbugs.quit ()*)
+ MQIC.close mqi_handle;
+ Hbugs.quit ()
 ;;
 
 try