Bug fixed: added a _undoable_action critical section to the reset method of

MatitaScript.script to avoid a Gtk assertion failure.

diff --git a/helm/matita/matita.ml b/helm/matita/matita.ml
index fbf3d500e07fa93736e8088480f340bc05a64183..07def06cd8b12dca4b1d93633f9b5c189a774f33 100644 (file)
--- a/helm/matita/matita.ml
+++ b/helm/matita/matita.ml
@@ -52,7 +52,7 @@ let gui = MatitaGui.instance ()
 let script =
   let s = 
     MatitaScript.script 
-      ~view:(gui#sourceView :> GText.view)
+      ~source_view:gui#sourceView
       ~init:(Lazy.force MatitaEngine.initial_status) 
       ~mathviewer:(MatitaMathView.mathViewer ())
       ~urichooser:(fun uris ->

diff --git a/helm/matita/matitaScript.ml b/helm/matita/matitaScript.ml
index f7094ab95d282763733ab987af03bd7ec28d94f5..bcb715f2dcd8019cd6c70f0a9fe678306495c036 100644 (file)
--- a/helm/matita/matitaScript.ml
+++ b/helm/matita/matitaScript.ml
@@ -415,7 +415,7 @@ let fresh_script_id =
   let i = ref 0 in
   fun () -> incr i; !i
 
-class script  ~(view: GText.view)
+class script  ~(source_view: GSourceView.source_view)
               ~(init: MatitaTypes.status) 
               ~(mathviewer: MatitaTypes.mathViewer) 
               ~set_star
@@ -423,7 +423,8 @@ class script  ~(view: GText.view)
               ~urichooser 
               ~develcreator 
               () =
-let buffer = view#buffer in
+let buffer = source_view#buffer in
+let source_buffer = source_view#source_buffer in
 object (self)
   val scriptId = fresh_script_id ()
   
@@ -553,10 +554,10 @@ object (self)
       | _ -> ()
     end ;
     let mark_position = buffer#get_iter_at_mark mark in
-    if view#move_mark_onscreen mark then
+    if source_view#move_mark_onscreen mark then
      begin
       buffer#move_mark mark mark_position;
-      view#scroll_to_mark ~use_align:true ~xalign:1.0 ~yalign:0.1 mark;
+      source_view#scroll_to_mark ~use_align:true ~xalign:1.0 ~yalign:0.1 mark;
      end;
     while Glib.Main.pending () do ignore(Glib.Main.iteration false); done
 
@@ -612,7 +613,9 @@ object (self)
 
   method reset () =
     self#goto_top;
+    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
 
@@ -747,10 +750,10 @@ end
 
 let _script = ref None
 
-let script ~view ~init ~mathviewer ~urichooser ~develcreator ~ask_confirmation ~set_star ()
+let script ~source_view ~init ~mathviewer ~urichooser ~develcreator ~ask_confirmation ~set_star ()
 =
   let s = new script 
-    ~view ~init ~mathviewer ~ask_confirmation ~urichooser ~develcreator ~set_star () 
+    ~source_view ~init ~mathviewer ~ask_confirmation ~urichooser ~develcreator ~set_star () 
   in
   _script := Some s;
   s

diff --git a/helm/matita/matitaScript.mli b/helm/matita/matitaScript.mli
index 8c776685a5a2b457993df59d3e90170cd4f6650b..a44d615d2b012cf322910a613e13dd76974b4cbd 100644 (file)
--- a/helm/matita/matitaScript.mli
+++ b/helm/matita/matitaScript.mli
@@ -76,7 +76,7 @@ end
   (** @param set_star callback used to set the modified symbol (usually a star
    * "*") on the side of a script name *)
 val script: 
-  view:GText.view -> 
+  source_view:GSourceView.source_view -> 
   init:MatitaTypes.status -> 
   mathviewer: MatitaTypes.mathViewer-> 
   urichooser: (UriManager.uri list -> UriManager.uri list) ->