From: Enrico Tassi Date: Wed, 13 Jul 2005 15:52:10 +0000 (+0000) Subject: all interface is locked during advance/retract X-Git-Tag: pre_notation~15 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=904ecbd458b20b47d250889459f9aa9ebd26d04d;p=helm.git all interface is locked during advance/retract --- diff --git a/helm/matita/matita.glade b/helm/matita/matita.glade index 4f77603ad..1f035a0fa 100644 --- a/helm/matita/matita.glade +++ b/helm/matita/matita.glade @@ -1773,7 +1773,7 @@ Copyright (C) 2005, 0 - + True GTK_ORIENTATION_HORIZONTAL GTK_TOOLBAR_BOTH diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml index b54dbb777..652c720b9 100644 --- a/helm/matita/matitaGui.ml +++ b/helm/matita/matitaGui.ml @@ -339,11 +339,29 @@ class gui () = source_buffer#place_cursor (source_buffer#get_iter_at_mark (`NAME "locked")) in + let lock_world _ = + main#buttonsToolbar#misc#set_sensitive false; + source_view#set_editable false + in + let unlock_world _ = + main#buttonsToolbar#misc#set_sensitive true; + source_view#set_editable true + in let advance _ = (MatitaScript.instance ())#advance (); cursor () in let retract _ = (MatitaScript.instance ())#retract (); cursor () in let top _ = (MatitaScript.instance ())#goto `Top (); cursor () in let bottom _ = (MatitaScript.instance ())#goto `Bottom (); cursor () in let jump _ = (MatitaScript.instance ())#goto `Cursor (); cursor () in + let locker f = + fun () -> + lock_world (); + try f ();unlock_world () with exc -> unlock_world (); raise exc + in + let advance = locker advance in + let retract = locker retract in + let top = locker top in + let bottom = locker bottom in + let jump = locker jump in let connect_key sym f = connect_key self#main#mainWinEventBox#event ~modifiers:[`CONTROL] ~stop:true sym f; diff --git a/helm/matita/matitaScript.ml b/helm/matita/matitaScript.ml index d145eec20..b077021e3 100644 --- a/helm/matita/matitaScript.ml +++ b/helm/matita/matitaScript.ml @@ -497,11 +497,11 @@ List.iter (fun s -> prerr_endline ("'" ^ s ^ "'")) new_statements; set_star self#ppFilename false method goto (pos: [`Top | `Bottom | `Cursor]) () = + let getpos _ = buffer#get_iter_at_mark (`MARK locked_mark) in match pos with | `Top -> self#goto_top; self#notify | `Bottom -> (try - let getpos _ = buffer#get_iter_at_mark (`MARK locked_mark) in let rec dowhile pos = self#_advance (); if pos#compare (getpos ()) < 0 then @@ -515,10 +515,15 @@ List.iter (fun s -> prerr_endline ("'" ^ s ^ "'")) new_statements; | `Cursor -> let locked_iter () = buffer#get_iter_at_mark (`NAME "locked") in let cursor_iter () = buffer#get_iter_at_mark `INSERT in - let rec forward_until_cursor () = (* go forward until locked > cursor *) - self#_advance (); - if (locked_iter ())#compare (cursor_iter ()) < 0 then - forward_until_cursor () + let forward_until_cursor () = (* go forward until locked > cursor *) + let rec aux oldpos = + self#_advance (); + if (locked_iter ())#compare (cursor_iter ()) < 0 && + oldpos#compare (getpos ()) < 0 + then + aux (getpos ()) + in + aux (getpos ()) in let rec back_until_cursor () = (* go backward until locked < cursor *) self#_retract ();