X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FgTopLevel.ml;h=7c28c22ced477ee65adad54bba34af1d2c5ed763;hb=8937d201088466051f7f1d3f0253d66d5afbc39f;hp=9df5f8f75439f8966374aecf0260362c7c3a40fb;hpb=9c82616da7a45061b3b85e32d598df30f5735196;p=helm.git
diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index 9df5f8f75..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;;
@@ -2645,12 +2655,44 @@ object(self)
ProofEngine.goal := Some metano ;
Lazy.force (page#compute) ;
Lazy.force setgoal;
- Hbugs.notify ()
+ if notify_hbugs_on_goal_change then
+ Hbugs.notify ()
with _ -> ()
))
end
;;
+let dump_environment () =
+ try
+ let oc = open_out environmentfile in
+ output_html (outputhtml ()) "Dumping environment ...
";
+ CicEnvironment.dump_to_channel
+ ~callback:(fun uri -> output_html (outputhtml ()) (uri ^ "
"))
+ oc;
+ output_html (outputhtml ()) "... done!
";
+ close_out oc
+ with exc ->
+ output_html (outputhtml ())
+ (Printf.sprintf
+ "
Dump failure, uncaught exception:%s
"
+ (Printexc.to_string exc))
+;;
+let restore_environment () =
+ try
+ let ic = open_in environmentfile in
+ output_html (outputhtml ()) "Restoring environment ...
";
+ CicEnvironment.restore_from_channel
+ ~callback:(fun uri -> output_html (outputhtml ()) (uri ^ "
"))
+ ic;
+ output_html (outputhtml ()) "... done!
";
+ close_in ic
+ with exc ->
+ output_html (outputhtml ())
+ (Printf.sprintf
+ "Restore failure, uncaught exception:%s
"
+ (Printexc.to_string exc))
+;;
+
(* Main window *)
class rendering_window output (notebook : notebook) =
@@ -2693,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);
@@ -2756,7 +2803,10 @@ class rendering_window output (notebook : notebook) =
factory6#add_check_item
~active:false ~key:GdkKeysyms._F5 ~callback:Hbugs.toggle "HBugs enabled"
in
- let _ = factory6#add_item ~callback:Hbugs.notify "(Re)Submit status!" 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"
@@ -2880,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 ()
;;