X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2FmatitaScript.ml;h=0e51213096292c4caf09b2b93058fbf024f8e169;hb=894c3e4038c93b484896e81132eae55046e47605;hp=23de391c6ed37e486d1b0324f429325a41d98af4;hpb=df61a96a76dcad98ebaee2faf875afd31dff7ead;p=helm.git

diff --git a/helm/software/matita/matitaScript.ml b/helm/software/matita/matitaScript.ml
index 23de391c6..0e5121309 100644
--- a/helm/software/matita/matitaScript.ml
+++ b/helm/software/matita/matitaScript.ml
@@ -363,6 +363,9 @@ script ex loc
            | `CANCEL -> raise MatitaTypes.Cancel)
      | _ -> ()
    end;
+   ignore (buffer#move_mark (`NAME "beginning_of_statement")
+    ~where:((buffer#get_iter_at_mark (`NAME "locked"))#forward_chars
+       (Glib.Utf8.length skipped_txt))) ;
    eval_with_engine
     guistuff lexicon_status grafite_status user_goal skipped_txt nonskipped_txt
      (TA.Executable (loc, ex))
@@ -501,6 +504,9 @@ object (self)
   (** text mark and tag representing locked part of a script *)
   val locked_mark =
     buffer#create_mark ~name:"locked" ~left_gravity:true buffer#start_iter
+  val beginning_of_statement_mark =
+    buffer#create_mark ~name:"beginning_of_statement"
+     ~left_gravity:true buffer#start_iter
   val locked_tag = buffer#create_tag [`BACKGROUND "lightblue"; `EDITABLE false]
   val error_tag = buffer#create_tag [`UNDERLINE `SINGLE; `FOREGROUND "red"]