From: Enrico Tassi Date: Wed, 14 Sep 2005 13:52:37 +0000 (+0000) Subject: bugfixes: X-Git-Tag: V_0_1_2_1~2 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=f6e34efbe6ce54f87d62997a0b81ca541a12d3da;p=helm.git bugfixes: 1) ask for saving/mooing only when the user has choosen a file to load 2) opening a file doesn't call goto_top (removing all xml, even if the moo has been generated). This fix should enforce the invariant that a moo exists only if the corrsponding xml objects do. 3) the switch_page callback is inhibited before removing pages in sequentViewers#reset --- diff --git a/helm/matita/matita.ml b/helm/matita/matita.ml index 6e5af0645..2a87554d8 100644 --- a/helm/matita/matita.ml +++ b/helm/matita/matita.ml @@ -91,12 +91,9 @@ let _ = | Incomplete_proof ((proof, goal) as status) -> sequents_viewer#load_sequents status; sequents_viewer#goto_sequent goal - | Proof proof -> - sequents_viewer#load_logo_with_qed - | No_proof -> - sequents_viewer#load_logo - | Intermediate _ -> - assert false (* only the engine may be in this state *) + | Proof proof -> sequents_viewer#load_logo_with_qed + | No_proof -> sequents_viewer#load_logo + | Intermediate _ -> assert false (* only the engine may be in this state *) in script#addObserver sequents_observer; script#addObserver browser_observer diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml index 153d474ab..1b46c03a4 100644 --- a/helm/matita/matitaGui.ml +++ b/helm/matita/matitaGui.ml @@ -606,19 +606,19 @@ class gui () = let script = s () in let status = script#status in try - if source_view#buffer#modified then - begin - match ask_unsaved main#toplevel with - | `YES -> saveScript () - | `NO -> () - | `CANCEL -> raise MatitaTypes.Cancel - end; - (match script_fname with - | None -> () - | Some fname -> - ask_and_save_moo_if_needed main#toplevel fname status); match self#chooseFile () with | Some f -> + if source_view#buffer#modified then + begin + match ask_unsaved main#toplevel with + | `YES -> saveScript () + | `NO -> () + | `CANCEL -> raise MatitaTypes.Cancel + end; + (match script_fname with + | None -> () + | Some fname -> + ask_and_save_moo_if_needed main#toplevel fname status); script#reset (); script#assignFileName f; source_view#source_buffer#begin_not_undoable_action (); diff --git a/helm/matita/matitaMathView.ml b/helm/matita/matitaMathView.ml index 47f8c5a5c..532c3dd97 100644 --- a/helm/matita/matitaMathView.ml +++ b/helm/matita/matitaMathView.ml @@ -430,19 +430,19 @@ class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () = w#remove cicMathView#coerce; scrolledWin <- None | None -> ()); - for i = 0 to pages do notebook#remove_page 0 done; + (match switch_page_callback with + | Some id -> + GtkSignal.disconnect notebook#as_widget id; + switch_page_callback <- None + | None -> ()); + for i = 0 to pages do notebook#remove_page 0 done; notebook#set_show_tabs true; pages <- 0; page2goal <- []; goal2page <- []; goal2win <- []; - _metasenv <- []; + _metasenv <- []; self#script#setGoal ~-1; - (match switch_page_callback with - | Some id -> - GtkSignal.disconnect notebook#as_widget id; - switch_page_callback <- None - | None -> ()) method load_sequents (status: ProofEngineTypes.status) = let ((_, metasenv, _, _), goal) = status in diff --git a/helm/matita/matitaScript.ml b/helm/matita/matitaScript.ml index f181b53d2..8bd0d60d1 100644 --- a/helm/matita/matitaScript.ml +++ b/helm/matita/matitaScript.ml @@ -586,7 +586,7 @@ object (self) method loadFromFile f = buffer#set_text (MatitaMisc.input_file f); - self#goto_top; + self#reset_buffer; buffer#set_modified false method assignFileName file = @@ -613,21 +613,23 @@ object (self) end method private goto_top = - MatitaSync.time_travel ~present:self#status ~past:init; + MatitaSync.time_travel ~present:self#status ~past:init + + method private reset_buffer = statements <- []; history <- [ init ]; userGoal <- ~-1; + self#notify; buffer#remove_tag locked_tag ~start:buffer#start_iter ~stop:buffer#end_iter; buffer#move_mark (`MARK locked_mark) ~where:buffer#start_iter method reset () = - self#goto_top; + self#reset_buffer; source_buffer#begin_not_undoable_action (); buffer#delete ~start:buffer#start_iter ~stop:buffer#end_iter; source_buffer#end_not_undoable_action (); - self#notify; buffer#set_modified false - + method template () = let template = MatitaMisc.input_file BuildTimeConf.script_template in buffer#insert ~iter:(buffer#get_iter `START) template; @@ -645,7 +647,11 @@ object (self) let getoldpos _ = buffer#get_iter_at_mark old_locked_mark in let dispose_old_locked_mark () = buffer#delete_mark old_locked_mark in match pos with - | `Top -> dispose_old_locked_mark (); self#goto_top; self#notify + | `Top -> + dispose_old_locked_mark (); + self#goto_top; + self#reset_buffer; + self#notify | `Bottom -> (try let rec dowhile () =