Better tooltips.

[helm.git] / helm / matita / matitaScript.ml

diff --git a/helm/matita/matitaScript.ml b/helm/matita/matitaScript.ml
index aae0e93d78a857fcbf14587eaa736c59f9bd526a..7e4dcb9fc04e4200a8c00e15a77c02af7e617a37 100644 (file)
--- a/helm/matita/matitaScript.ml
+++ b/helm/matita/matitaScript.ml
@@ -57,7 +57,7 @@ let prepend_text header base =
   if Pcre.pmatch ~rex:heading_nl_RE base then
     sprintf "\n%s%s" header base
   else
-    sprintf "%s\n%s" header base
+    sprintf "\n%s\n%s" header base
 
   (** creates a statement AST for the Goal tactic, e.g. "goal 7" *)
 let goal_ast n =
@@ -337,7 +337,7 @@ let eval_executable guistuff status user_goal parsed_text script ex =
         (match ML.baseuri_of_baseuri_decl (TA.Executable (loc,ex)) with
         | None -> ()
         | Some u -> 
-            if not (MatitacleanLib.is_empty u) then
+            if not (ML.is_empty u) then
               match 
                 guistuff.ask_confirmation 
                   ~title:"Baseuri redefinition" 
@@ -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 ()
   
@@ -415,9 +417,7 @@ object (self)
        (fun _ -> if buffer#modified then 
           set_star self#ppFilename true 
         else 
-          set_star self#ppFilename false));
-    self#reset ();
-    self#template ()
+          set_star self#ppFilename false))
 
   val mutable statements = [];    (** executed statements *)
   val mutable history = [ init ];
@@ -434,6 +434,8 @@ object (self)
     buffer#create_mark ~name:"locked" ~left_gravity:true buffer#start_iter
   val locked_tag = buffer#create_tag [`BACKGROUND "lightblue"; `EDITABLE false]
 
+  method locked_mark = locked_mark
+
     (* history can't be empty, the invariant above grant that it contains at
      * least the init status *)
   method status = match history with hd :: _ -> hd | _ -> assert false
@@ -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 =
@@ -586,34 +594,36 @@ 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 
+    let getoffset () = (buffer#get_iter_at_mark (`MARK locked_mark))#offset in 
     match pos with
     | `Top -> self#goto_top; self#notify
     | `Bottom ->
         (try 
           let rec dowhile pos =
             self#_advance ();
-            if pos#compare (getpos ()) < 0 then
-              dowhile (getpos ())
+            let newpos = getoffset () in
+            if pos - newpos < 0 then
+              dowhile newpos
           in
-          dowhile (getpos ());
+          dowhile (getoffset ());
           self#notify 
         with 
         | Margin -> self#notify
         | exc -> self#notify; raise exc)
     | `Cursor ->
-        let locked_iter () = buffer#get_iter_at_mark (`NAME "locked") in
-        let cursor_iter () = buffer#get_iter_at_mark `INSERT in
-        let cmp = (locked_iter ())#offset - (cursor_iter ())#offset in
+        let locked_offset () =
+         (buffer#get_iter_at_mark (`NAME "locked"))#offset in
+        let cursor_offset () = (buffer#get_iter_at_mark `INSERT)#offset in
+        let cmp = (locked_offset ()) - cursor_offset () in
         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 
+            if (locked_offset ()) - cursor_offset () < 0 &&
+               oldpos - (getoffset ()) < 0 
             then
-              aux (getpos ())
+              aux (getoffset ())
           in
-          aux (getpos ())
+          aux (getoffset ())
         in
         let rec back_until_cursor len = (* go backward until locked < cursor *)
          function
@@ -681,10 +691,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