From ce3b9018fe80437a56e56f2bc0b5696b2acb59bb Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 27 Jul 2005 14:16:57 +0000
Subject: [PATCH] Bug fixed: added a _undoable_action critical section to the
 reset method of MatitaScript.script to avoid a Gtk assertion failure.

---
 helm/matita/matita.ml        |  2 +-
 helm/matita/matitaScript.ml  | 15 +++++++++------
 helm/matita/matitaScript.mli |  2 +-
 3 files changed, 11 insertions(+), 8 deletions(-)

diff --git a/helm/matita/matita.ml b/helm/matita/matita.ml
index fbf3d500e..07def06cd 100644
--- 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 f7094ab95..bcb715f2d 100644
--- 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 8c776685a..a44d615d2 100644
--- 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) -> 
-- 
2.39.2