Small interface improvements.

diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index ed8040e7d07ed25d1d1a83749cbe17fa55c9d1b8..22bb994550a76780df5b9787e9fb091654e60447 100644 (file)
--- a/helm/gTopLevel/gTopLevel.ml
+++ b/helm/gTopLevel/gTopLevel.ml
@@ -128,6 +128,16 @@ let set_outputhtml,outputhtml =
   )
 ;;
 
+exception QedSetSensitiveNotInitialized;;
+let qed_set_sensitive =
+ ref (function _ -> raise QedSetSensitiveNotInitialized)
+;;
+
+exception SaveSetSensitiveNotInitialized;;
+let save_set_sensitive =
+ ref (function _ -> raise SaveSetSensitiveNotInitialized)
+;;
+
 (* COMMAND LINE OPTIONS *)
 
 let usedb = ref true
@@ -214,9 +224,7 @@ let check_window outputhtml uris =
      let scrolled_window =
       GBin.scrolled_window ~border_width:10
        ~packing:
-         (notebook#append_page 
-           ~tab_label:((GMisc.label ~text:uri ())#coerce)
-         )
+         (notebook#append_page ~tab_label:((GMisc.label ~text:uri ())#coerce))
        ()
      in
       lazy 
@@ -648,6 +656,7 @@ let refresh_proof (output : GMathView.math_view) =
    match !ProofEngine.proof with
       None -> assert false
     | Some (uri,metasenv,bo,ty) ->
+       !qed_set_sensitive (List.length metasenv = 0) ;
        (*CSC: Wrong: [] is just plainly wrong *)
        uri,(Cic.CurrentProof (UriManager.name_of_uri uri, metasenv, bo, ty, []))
   in
@@ -1270,7 +1279,8 @@ let load () =
             prooffiletype ^ "</h1>") ;
          output_html outputhtml
           ("<h1 color=\"Green\">Current proof body loaded from " ^
-            prooffile ^ "</h1>")
+            prooffile ^ "</h1>") ;
+        !save_set_sensitive true
      | _ -> assert false
   with
      RefreshSequentException e ->
@@ -1406,8 +1416,7 @@ let setgoal metano =
     | Some (_,metasenv,_,_) -> metasenv
   in
    try
-    ProofEngine.goal := Some metano ;
-    refresh_sequent ~empty_notebook:false notebook ;
+    refresh_sequent ~empty_notebook:false notebook
    with
       RefreshSequentException e ->
        output_html outputhtml
@@ -1486,6 +1495,7 @@ let state () =
             ProofEngine.goal := Some 1 ;
             refresh_sequent notebook ;
             refresh_proof output ;
+            !save_set_sensitive true
      done
     with
        CicTextualParser0.Eof ->
@@ -2039,7 +2049,8 @@ object(self)
        skip_switch_page_event <- false ;
        if not skip then
         try
-         let (_,setgoal,page) = List.nth !pages i in
+         let (metano,setgoal,page) = List.nth !pages i in
+          ProofEngine.goal := Some metano ;
           Lazy.force (page#compute) ;
           Lazy.force setgoal
         with _ -> ()
@@ -2064,8 +2075,18 @@ class rendering_window output (notebook : notebook) =
  let export_to_postscript_menu_item =
   begin
    ignore
-    (factory1#add_item "Load" ~key:GdkKeysyms._L ~callback:load) ;
-   ignore (factory1#add_item "Save" ~key:GdkKeysyms._S ~callback:save) ;
+    (factory1#add_item "Load Unfinished Proof" ~key:GdkKeysyms._L
+      ~callback:load) ;
+   let save_menu_item =
+    factory1#add_item "Save Unfinished Proof" ~key:GdkKeysyms._S ~callback:save
+   in
+   let qed_menu_item =
+    factory1#add_item "Qed" ~key:GdkKeysyms._Q ~callback:qed in
+   ignore
+    (save_set_sensitive := function b -> save_menu_item#misc#set_sensitive b);
+   ignore (!save_set_sensitive false);
+   ignore (qed_set_sensitive:=function b -> qed_menu_item#misc#set_sensitive b);
+   ignore (!qed_set_sensitive false);
    ignore (factory1#add_separator ()) ;
    let export_to_postscript_menu_item =
     factory1#add_item "Export to PostScript..." ~key:GdkKeysyms._E
@@ -2093,8 +2114,6 @@ class rendering_window output (notebook : notebook) =
     proveit_menu_item#misc#set_sensitive b ;
     focus_menu_item#misc#set_sensitive b
  in
- let _ = factory2#add_separator () in
- let _ = factory2#add_item "Qed" ~key:GdkKeysyms._Q ~callback:qed in
  let _ = !focus_and_proveit_set_sensitive false in
  (* settings menu *)
  let settings_menu = factory0#add_submenu "Settings" in