)
;;
+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
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
in
aux dom' list_of_uris
in
- output_html (outputhtml ())
- ("<h1>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 ())
+ ("<h1>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 =
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
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
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
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)
;;
(*
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 ->
| 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
ProofEngine.goal := Some 1 ;
refresh_sequent notebook ;
refresh_proof output ;
+ !save_set_sensitive true
done
with
CicTextualParser0.Eof ->
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
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 _ -> ()
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
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
projects / helm.git / blobdiff