From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 18 Jul 2005 16:38:53 +0000 (+0000)
Subject: Smart scrolling during script advancement implemented.
X-Git-Tag: V_0_7_2~191
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=ad0292419b0204384ff55c946a6aabb73a47c42b;p=helm.git

Smart scrolling during script advancement implemented.
---

diff --git a/helm/matita/matita.ml b/helm/matita/matita.ml
index 2ff07613a..db0fd2b18 100644
--- a/helm/matita/matita.ml
+++ b/helm/matita/matita.ml
@@ -73,7 +73,7 @@ let _ =
 
 let script =
   MatitaScript.script 
-    ~buffer:gui#sourceView#buffer
+    ~view:(gui#sourceView :> GText.view)
     ~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 aae0e93d7..e0e4227dd 100644
--- a/helm/matita/matitaScript.ml
+++ b/helm/matita/matitaScript.ml
@@ -383,13 +383,15 @@ let fresh_script_id =
   let i = ref 0 in
   fun () -> incr i; !i
 
-class script ~(buffer: GText.buffer) ~(init: MatitaTypes.status) 
+class script  ~(view: GText.view)
+              ~(init: MatitaTypes.status) 
               ~(mathviewer: MatitaTypes.mathViewer) 
               ~set_star
               ~ask_confirmation
               ~urichooser 
               ~develcreator 
               () =
+let buffer = view#buffer in
 object (self)
   val scriptId = fresh_script_id ()
   
@@ -519,6 +521,12 @@ List.iter (fun s -> prerr_endline ("'" ^ s ^ "'")) new_statements;
         Incomplete_proof (_,goal) -> self#setGoal goal
       | _ -> ()
     end ;
+    let mark_position = buffer#get_iter_at_mark mark in
+    if 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;
+     end;
     while Glib.Main.pending () do ignore(Glib.Main.iteration false); done
 
   method clean_dirty_lock =
@@ -681,10 +689,10 @@ end
 
 let _script = ref None
 
-let script ~buffer ~init ~mathviewer ~urichooser ~develcreator ~ask_confirmation ~set_star ()
+let script ~view ~init ~mathviewer ~urichooser ~develcreator ~ask_confirmation ~set_star ()
 =
   let s = new script 
-    ~buffer ~init ~mathviewer ~ask_confirmation ~urichooser ~develcreator ~set_star () 
+    ~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 637584aa9..96337cbdb 100644
--- a/helm/matita/matitaScript.mli
+++ b/helm/matita/matitaScript.mli
@@ -72,7 +72,7 @@ end
   (** @param set_star callback used to set the modified symbol (usually a star
    * "*") on the side of a script name *)
 val script: 
-  buffer:GText.buffer -> 
+  view:GText.view -> 
   init:MatitaTypes.status -> 
   mathviewer: MatitaTypes.mathViewer-> 
   urichooser: (UriManager.uri list -> UriManager.uri list) ->