X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FgTopLevel.ml;h=7d3985af3a56b63ef24059f16bac82e8f3a06232;hb=5333af1b6dba295b496e75b0ba864f87ebc1eb88;hp=9df5f8f75439f8966374aecf0260362c7c3a40fb;hpb=e636941304a5567a90e0d271e25325c0c8b5fce1;p=helm.git
diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index 9df5f8f75..7d3985af3 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;;
@@ -470,7 +480,7 @@ let save_obj uri obj =
;;
let qed () =
- match !ProofEngine.proof with
+ match ProofEngine.get_proof () with
None -> assert false
| Some (uri,[],bo,ty) ->
if
@@ -559,10 +569,10 @@ let mk_fresh_name_callback context name ~typ =
let refresh_proof (output : TermViewer.proof_viewer) =
try
let uri,currentproof =
- match !ProofEngine.proof with
+ match ProofEngine.get_proof () with
None -> assert false
| Some (uri,metasenv,bo,ty) ->
- ProofEngine.proof := Some(uri,metasenv,bo,ty);
+ ProofEngine.set_proof (Some (uri,metasenv,bo,ty)) ;
if List.length metasenv = 0 then
begin
!qed_set_sensitive true ;
@@ -577,12 +587,16 @@ let refresh_proof (output : TermViewer.proof_viewer) =
ignore (output#load_proof uri currentproof)
with
e ->
- match !ProofEngine.proof with
+ match ProofEngine.get_proof () with
None -> assert false
| Some (uri,metasenv,bo,ty) ->
prerr_endline ("Offending proof: " ^ CicPp.ppobj (Cic.CurrentProof ("questa",metasenv,bo,ty,[]))) ; flush stderr ;
raise (InvokeTactics.RefreshProofException e)
+let set_proof_engine_goal g =
+ ProofEngine.goal := g
+;;
+
let refresh_goals ?(empty_notebook=true) notebook =
try
match !ProofEngine.goal with
@@ -596,7 +610,7 @@ let refresh_goals ?(empty_notebook=true) notebook =
notebook#proofw#unload
| Some metano ->
let metasenv =
- match !ProofEngine.proof with
+ match ProofEngine.get_proof () with
None -> assert false
| Some (_,metasenv,_,_) -> metasenv
in
@@ -612,18 +626,18 @@ let refresh_goals ?(empty_notebook=true) notebook =
notebook#remove_all_pages ~skip_switch_page_event ;
List.iter (function (m,_,_) -> notebook#add_page m) metasenv ;
in
- if empty_notebook then
- begin
- regenerate_notebook () ;
- notebook#set_current_page
- ~may_skip_switch_page_event:false metano
- end
- else
- begin
- notebook#set_current_page
- ~may_skip_switch_page_event:true metano ;
- notebook#proofw#load_sequent metasenv currentsequent
- end
+ if empty_notebook then
+ begin
+ regenerate_notebook () ;
+ notebook#set_current_page
+ ~may_skip_switch_page_event:false metano
+ end
+ else
+ begin
+ notebook#set_current_page
+ ~may_skip_switch_page_event:true metano ;
+ notebook#proofw#load_sequent metasenv currentsequent
+ end
with
e ->
let metano =
@@ -632,7 +646,7 @@ let metano =
| Some m -> m
in
let metasenv =
- match !ProofEngine.proof with
+ match ProofEngine.get_proof () with
None -> assert false
| Some (_,metasenv,_,_) -> metasenv
in
@@ -691,14 +705,13 @@ let load_unfinished_proof () =
match CicParser.obj_of_xml prooffiletype (Some prooffile) with
Cic.CurrentProof (_,metasenv,bo,ty,_) ->
typecheck_loaded_proof metasenv bo ty ;
- ProofEngine.proof :=
- Some (uri, metasenv, bo, ty) ;
- ProofEngine.goal :=
+ ProofEngine.set_proof (Some (uri, metasenv, bo, ty)) ;
+ refresh_proof output ;
+ set_proof_engine_goal
(match metasenv with
[] -> None
| (metano,_,_)::_ -> Some metano
) ;
- refresh_proof output ;
refresh_goals notebook ;
output_html outputhtml
("
Current proof type loaded from " ^
@@ -866,7 +879,7 @@ let setgoal metano =
let notebook = (rendering_window ())#notebook in
let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
let metasenv =
- match !ProofEngine.proof with
+ match ProofEngine.get_proof () with
None -> assert false
| Some (_,metasenv,_,_) -> metasenv
in
@@ -1569,9 +1582,9 @@ prerr_endline ("######################## " ^ xxx) ;
try
let metasenv,expr = !get_metasenv_and_term () in
let _ = CicTypeChecker.type_of_aux' metasenv [] expr in
- ProofEngine.proof :=
- Some (!get_uri (), (1,[],expr)::metasenv, Cic.Meta (1,[]), expr) ;
- ProofEngine.goal := Some 1 ;
+ ProofEngine.set_proof
+ (Some (!get_uri (), (1,[],expr)::metasenv, Cic.Meta (1,[]), expr)) ;
+ set_proof_engine_goal (Some 1) ;
refresh_goals notebook ;
refresh_proof output ;
!save_set_sensitive true ;
@@ -1612,7 +1625,7 @@ let check scratch_window () =
let inputt = ((rendering_window ())#inputt : TermEditor.term_editor) in
let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
let metasenv =
- match !ProofEngine.proof with
+ match ProofEngine.get_proof () with
None -> []
| Some (_,metasenv,_,_) -> metasenv
in
@@ -1661,9 +1674,8 @@ let open_ () =
| Cic.Variable _
| Cic.InductiveDefinition _ -> raise NotADefinition
in
- ProofEngine.proof :=
- Some (uri, metasenv, bo, ty) ;
- ProofEngine.goal := None ;
+ ProofEngine.set_proof (Some (uri, metasenv, bo, ty)) ;
+ set_proof_engine_goal None ;
refresh_goals notebook ;
refresh_proof output ;
!save_set_sensitive true
@@ -2133,7 +2145,7 @@ let searchPattern () =
let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
try
let proof =
- match !ProofEngine.proof with
+ match ProofEngine.get_proof () with
None -> assert false
| Some proof -> proof
in
@@ -2642,15 +2654,47 @@ object(self)
if not skip then
try
let (metano,setgoal,page) = List.nth !pages i in
- ProofEngine.goal := Some metano ;
+ set_proof_engine_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 +2737,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 +2805,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"
@@ -2780,7 +2832,7 @@ class rendering_window output (notebook : notebook) =
~callback:
(function _ ->
ApplyStylesheets.reload_stylesheets () ;
- if !ProofEngine.proof <> None then
+ if ProofEngine.get_proof () <> None then
try
refresh_goals notebook ;
refresh_proof output
@@ -2880,7 +2932,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 ()
;;