X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FgTopLevel.ml;h=7c28c22ced477ee65adad54bba34af1d2c5ed763;hb=f480a8792f70b765c5e15cc16f1251ac6bc21d01;hp=ec19107dde4e030dc56bb6311e324a7ad61b0227;hpb=2bd53620e7f5dea5ddef583ba65ce6c32bbad159;p=helm.git

diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index ec19107dd..7c28c22ce 100644
--- a/helm/gTopLevel/gTopLevel.ml
+++ b/helm/gTopLevel/gTopLevel.ml
@@ -1,4 +1,4 @@
-(* Copyright (C) 2000-2002, HELM Team.
+(* Copyright (C) 2000-2003, HELM Team.
  * 
  * This file is part of HELM, an Hypertextual, Electronic
  * Library of Mathematics, developed at the Computer Science
@@ -77,6 +77,16 @@ let prooffiletype =
   Not_found -> "/public/currentprooftype"
 ;;
 
+let environmentfile =
+ try
+  Sys.getenv "GTOPLEVEL_ENVIRONMENTFILE"
+ with
+  Not_found -> "/public/environment"
+;;
+
+let restore_environment_on_boot = true ;;
+let notify_hbugs_on_goal_change = false ;;
+
 (* GLOBAL REFERENCES (USED BY CALLBACKS) *)
 
 let htmlheader_and_content = ref htmlheader;;
@@ -217,7 +227,8 @@ let check_window outputhtml uris =
  in
   ignore
    (notebook#connect#switch_page
-     (function i -> Lazy.force (List.nth render_terms i)))
+     (function i ->
+       Lazy.force (List.nth render_terms i)))
 ;;
 
 exception NoChoice;;
@@ -565,14 +576,10 @@ let refresh_proof (output : TermViewer.proof_viewer) =
        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, []))
@@ -665,8 +672,18 @@ module InvokeTacticsCallbacks =
  end
 ;;
 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
+  | Hbugs_types.Use_apply_Luke term ->
+      let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
+      check_window outputhtml [term]
+  | _ -> ())
+;;
+
+let dummy_uri = "/dummy.con"
 
   (** load an unfinished proof from filesystem *)
 let load_unfinished_proof () =
@@ -675,7 +692,7 @@ let load_unfinished_proof () =
  let notebook = (rendering_window ())#notebook in
   try
    match 
-    GToolbox.input_string ~title:"Load Unfinished Proof" ~text:"/dummy.con"
+    GToolbox.input_string ~title:"Load Unfinished Proof" ~text:dummy_uri
      "Choose an URI:"
    with
       None -> raise NoChoice
@@ -1482,6 +1499,8 @@ let new_proof () =
  let uri_entry =
   GEdit.entry ~editable:true
    ~packing:(hbox#pack ~expand:true ~fill:true ~padding:5) () in
+ uri_entry#set_text dummy_uri;
+ uri_entry#select_region ~start:1 ~stop:(String.length dummy_uri);
  let hbox1 =
   GPack.hbox ~border_width:0
    ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
@@ -1916,7 +1935,7 @@ let completeSearchPattern () =
    let must = CGSearchPattern.get_constraints expr in
    let must',only = refine_constraints must in
    let query =
-    MQG.query_of_constraints (Some MQGU.universe_for_search_pattern) must' only
+    MQG.query_of_constraints (Some CGSearchPattern.universe) must' only
    in
    let results = MQI.execute mqi_handle query in 
     show_query_results results
@@ -2635,12 +2654,45 @@ object(self)
          let (metano,setgoal,page) = List.nth !pages i in
           ProofEngine.goal := Some metano ;
           Lazy.force (page#compute) ;
-          Lazy.force setgoal
+          Lazy.force setgoal;
+          if notify_hbugs_on_goal_change then
+            Hbugs.notify ()
         with _ -> ()
     ))
 end
 ;;
 
+let dump_environment () =
+  try
+    let oc = open_out environmentfile in
+    output_html (outputhtml ()) "<b>Dumping environment ... </b><br />";
+    CicEnvironment.dump_to_channel
+      ~callback:(fun uri -> output_html (outputhtml ()) (uri ^ "<br />"))
+      oc;
+    output_html (outputhtml ()) "<b>... done!</b><br />";
+    close_out oc
+  with exc ->
+    output_html (outputhtml ())
+      (Printf.sprintf
+        "<h1 color=\"red\">Dump failure, uncaught exception:%s</h1>"
+        (Printexc.to_string exc))
+;;
+let restore_environment () =
+  try
+    let ic = open_in environmentfile in
+    output_html (outputhtml ()) "<b>Restoring environment ... </b><br />";
+    CicEnvironment.restore_from_channel
+      ~callback:(fun uri -> output_html (outputhtml ()) (uri ^ "<br />"))
+      ic;
+    output_html (outputhtml ()) "<b>... done!</b><br />";
+    close_in ic
+  with exc ->
+    output_html (outputhtml ())
+      (Printf.sprintf
+        "<h1 color=\"red\">Restore failure, uncaught exception:%s</h1>"
+        (Printexc.to_string exc))
+;;
+
 (* Main window *)
 
 class rendering_window output (notebook : notebook) =
@@ -2683,6 +2735,11 @@ class rendering_window output (notebook : notebook) =
     factory1#add_item "Save Unfinished Proof" ~key:GdkKeysyms._S
       ~callback:save_unfinished_proof
    in
+   ignore (factory1#add_separator ()) ;
+   ignore (factory1#add_item "Clear Environment" ~callback:CicEnvironment.empty);
+   ignore (factory1#add_item "Dump Environment" ~callback:dump_environment);
+   ignore
+    (factory1#add_item "Restore Environment" ~callback:restore_environment);
    ignore
     (save_set_sensitive := function b -> save_menu_item#misc#set_sensitive b);
    ignore (!save_set_sensitive false);
@@ -2742,10 +2799,21 @@ class rendering_window output (notebook : notebook) =
  (* hbugs menu *)
  let hbugs_menu = factory0#add_submenu "HBugs" in
  let factory6 = new GMenu.factory hbugs_menu ~accel_group in
- let toggle_hbugs_menu_item =
+ let _ =
   factory6#add_check_item
     ~active:false ~key:GdkKeysyms._F5 ~callback:Hbugs.toggle "HBugs enabled"
  in
+ let _ =
+  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 "Start Web Services"
+ in
+ let _ =
+  factory6#add_item ~callback:Hbugs.stop_web_services "Stop Web Services"
+ in
  (* settings menu *)
  let settings_menu = factory0#add_submenu "Settings" in
  let factory3 = new GMenu.factory settings_menu ~accel_group in
@@ -2862,7 +2930,8 @@ let initialize_everything () =
      Gdome_xslt.setDebugCallback
       (Some (print_error_as_html "XSLT Debug Message: "));
      rendering_window'#show () ;
-(*      Hbugs.toggle true; *)
+     if restore_environment_on_boot && Sys.file_exists environmentfile then
+       restore_environment ();
      GtkThread.main ()
 ;;