X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FgTopLevel.ml;h=58e785dec3ef37c5ff6cf8dfc4dad4d2819b3ba5;hb=6ab193f88745acd3def85e47d643a92efb2f9fc5;hp=ed8040e7d07ed25d1d1a83749cbe17fa55c9d1b8;hpb=88f556f06db4f8438615141d040b26dcbdc4205d;p=helm.git diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml index ed8040e7d..58e785dec 100644 --- 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 @@ -477,9 +485,11 @@ let disambiguate_input context metasenv dom mk_metasenv_and_expr = in aux dom' list_of_uris in - output_html (outputhtml ()) - ("

Disambiguation phase started: " ^ - string_of_int (List.length resolve_ids) ^ " cases will be tried.") ; + let tests_no = List.length resolve_ids in + if tests_no > 1 then + output_html (outputhtml ()) + ("

Disambiguation phase started: " ^ + string_of_int (List.length resolve_ids) ^ " cases will be tried.") ; (* now we select only the ones that generates well-typed terms *) let resolve_ids' = let rec filter = @@ -648,6 +658,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 @@ -678,7 +689,7 @@ let refresh_sequent ?(empty_notebook=true) notebook = None -> if empty_notebook then begin - notebook#remove_all_pages ; + notebook#remove_all_pages ~skip_switch_page_event:false ; notebook#set_empty_page end else @@ -693,19 +704,29 @@ let refresh_sequent ?(empty_notebook=true) notebook = let sequent_gdome,ids_to_terms,ids_to_father_ids,ids_to_hypotheses = SequentPp.XmlPp.print_sequent metasenv currentsequent in - let sequent_doc = - Xml2Gdome.document_of_xml domImpl sequent_gdome - in - let sequent_mml = - applyStylesheets sequent_doc sequent_styles sequent_args + let regenerate_notebook () = + let skip_switch_page_event = + match metasenv with + (m,_,_)::_ when m = metano -> false + | _ -> true in + notebook#remove_all_pages ~skip_switch_page_event ; + List.iter (function (m,_,_) -> notebook#add_page m) metasenv ; + in if empty_notebook then begin - notebook#remove_all_pages ; - List.iter (function (m,_,_) -> notebook#add_page m) metasenv ; + regenerate_notebook () ; + notebook#set_current_page ~may_skip_switch_page_event:false metano + end + else + begin + let sequent_doc = Xml2Gdome.document_of_xml domImpl sequent_gdome in + let sequent_mml = + applyStylesheets sequent_doc sequent_styles sequent_args + in + notebook#set_current_page ~may_skip_switch_page_event:true metano; + notebook#proofw#load_tree ~dom:sequent_mml end ; - notebook#set_current_page metano ; - notebook#proofw#load_tree ~dom:sequent_mml ; current_goal_infos := Some (ids_to_terms,ids_to_father_ids,ids_to_hypotheses) with @@ -720,9 +741,11 @@ let metasenv = None -> assert false | Some (_,metasenv,_,_) -> metasenv in +try let currentsequent = List.find (function (m,_,_) -> m=metano) metasenv in prerr_endline ("Offending sequent: " ^ SequentPp.TextualPp.print_sequent currentsequent) ; flush stderr ; raise (RefreshSequentException e) +with Not_found -> prerr_endline ("Offending sequent " ^ string_of_int metano ^ " unkown."); raise (RefreshSequentException e) ;; (* @@ -1270,7 +1293,8 @@ let load () = prooffiletype ^ "

") ; output_html outputhtml ("

Current proof body loaded from " ^ - prooffile ^ "

") + prooffile ^ "") ; + !save_set_sensitive true | _ -> assert false with RefreshSequentException e -> @@ -1406,8 +1430,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 +1509,7 @@ let state () = ProofEngine.goal := Some 1 ; refresh_sequent notebook ; refresh_proof output ; + !save_set_sensitive true done with CicTextualParser0.Eof -> @@ -2006,28 +2030,56 @@ object(self) end ;; +class empty_page = + let vbox1 = GPack.vbox () in + let scrolled_window1 = + GBin.scrolled_window ~border_width:10 + ~packing:(vbox1#pack ~expand:true ~padding:5) () in + let proofw = + GMathView.math_view ~width:400 ~height:275 + ~packing:(scrolled_window1#add) () in +object(self) + method proofw = (assert false : GMathView.math_view) + method content = vbox1 + method compute = (assert false : unit) +end +;; + +let empty_page = new empty_page;; + class notebook = object(self) val notebook = GPack.notebook () val pages = ref [] val mutable skip_switch_page_event = false + val mutable empty = true method notebook = notebook method add_page n = let new_page = new page () in + empty <- false ; pages := !pages @ [n,lazy (setgoal n),new_page] ; notebook#append_page ~tab_label:((GMisc.label ~text:("?" ^ string_of_int n) ())#coerce) new_page#content#coerce - method remove_all_pages = - List.iter (function _ -> notebook#remove_page 0) !pages ; + method remove_all_pages ~skip_switch_page_event:skip = + if empty then + notebook#remove_page 0 (* let's remove the empty page *) + else + List.iter (function _ -> notebook#remove_page 0) !pages ; pages := [] ; - method set_current_page n = + skip_switch_page_event <- skip + method set_current_page ~may_skip_switch_page_event n = let (_,_,page) = List.find (function (m,_,_) -> m=n) !pages in let new_page = notebook#page_num page#content#coerce in - if new_page <> notebook#current_page then + if may_skip_switch_page_event && new_page <> notebook#current_page then skip_switch_page_event <- true ; notebook#goto_page new_page - method set_empty_page = self#add_page (-1) + method set_empty_page = + empty <- true ; + pages := [] ; + notebook#append_page + ~tab_label:((GMisc.label ~text:"No proof in progress" ())#coerce) + empty_page#content#coerce method proofw = let (_,_,page) = List.nth !pages notebook#current_page in page#proofw @@ -2039,7 +2091,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 +2117,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 +2156,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