Merge branch 'trunk' into pr379

5 files changed, 28 insertions, 13 deletions

diff --git a/ide/coqOps.ml b/ide/coqOps.ml
index 4a1d688f5..45b5a1007 100644
--- a/ide/coqOps.ml
+++ b/ide/coqOps.ml
@@ -358,7 +358,7 @@ object(self)
         | Good evs ->
           proof#set_goals goals;
           proof#set_evars evs;
-          proof#refresh ();
+          proof#refresh ~force:true;
           Coq.return ()
         )
       )
diff --git a/ide/texmacspp.ml b/ide/texmacspp.ml
index 6fbed38fb..e787e48bf 100644
--- a/ide/texmacspp.ml
+++ b/ide/texmacspp.ml
@@ -15,6 +15,7 @@ open Bigint
 open Decl_kinds
 open Extend
 open Libnames
+open Constrexpr_ops
 
 let unlock loc =
   let start, stop = Loc.unloc loc in
@@ -228,14 +229,15 @@ and pp_decl_notation ((_, s), ce, sc) = (* don't know what it is for now *)
   Element ("decl_notation", ["name", s], [pp_expr ce])
 and pp_local_binder lb = (* don't know what it is for now *)
   match lb with
-  | LocalRawDef ((_, nam), ce) ->
+  | CLocalDef ((loc, nam), ce, ty) ->
       let attrs = ["name", string_of_name nam] in
-      pp_expr ~attr:attrs ce
-  | LocalRawAssum (namll, _, ce) ->
+      let value = match ty with Some t -> CCast (Loc.merge (constr_loc ce) (constr_loc t),ce, CastConv t) | None -> ce in
+      pp_expr ~attr:attrs value
+  | CLocalAssum (namll, _, ce) ->
       let ppl =
         List.map (fun (loc, nam) -> (xmlCst (string_of_name nam) loc)) namll in
       xmlTyped (ppl @ [pp_expr ce])
-  | LocalPattern _ ->
+  | CLocalPattern _ ->
       assert false
 and pp_local_decl_expr lde = (* don't know what it is for now *)
   match lde with
@@ -465,7 +467,8 @@ and pp_expr ?(attr=[]) e =
            [Element ("scrutinees", [], List.map pp_case_expr cel)] @
            [pp_branch_expr_list bel]))
   | CRecord (_, _) -> assert false
-  | CLetIn (loc, (varloc, var), value, body) ->
+  | CLetIn (loc, (varloc, var), value, typ, body) ->
+      let value = match typ with Some t -> CCast (Loc.merge (constr_loc value) (constr_loc t),value, CastConv t) | None -> value in
       xmlApply loc
         (xmlOperator "let" loc ::
          [xmlCst (string_of_name var) varloc; pp_expr value; pp_expr body])
diff --git a/ide/wg_ProofView.ml b/ide/wg_ProofView.ml
index b5405570c..3cbe58388 100644
--- a/ide/wg_ProofView.ml
+++ b/ide/wg_ProofView.ml
@@ -14,7 +14,7 @@ class type proof_view =
   object
     inherit GObj.widget
     method buffer : GText.buffer
-    method refresh : unit -> unit
+    method refresh : force:bool -> unit
     method clear : unit -> unit
     method set_goals : Interface.goals option -> unit
     method set_evars : Interface.evar list option -> unit
@@ -197,6 +197,7 @@ let proof_view () =
     inherit GObj.widget view#as_widget
     val mutable goals = None
     val mutable evars = None
+    val mutable last_width = -1
 
     method buffer = text_buffer
 
@@ -206,13 +207,24 @@ let proof_view () =
 
     method set_evars evs = evars <- evs
 
-    method refresh () =
-      let dummy _ () = () in
-      display (mode_tactic dummy) view goals None evars
+    method refresh ~force =
+      (* We need to block updates here due to the following race:
+         insertion of messages may create a vertical scrollbar, this
+         will trigger a width change, calling refresh again and
+         going into an infinite loop. *)
+      let width = Ideutils.textview_width view  in
+      (* Could still this method race if the scrollbar changes the
+         textview_width ?? *)
+      let needed = force || last_width <> width in
+      if needed then begin
+        last_width <- width;
+        let dummy _ () = () in
+        display (mode_tactic dummy) view goals None evars
+      end
   end
   in
   (* Is there a better way to connect the signal ? *)
   (* Can this be done in the object constructor? *)
-  let w_cb _ = pf#refresh () in
+  let w_cb _ = pf#refresh ~force:false in
   ignore (view#misc#connect#size_allocate w_cb);
   pf
diff --git a/ide/wg_ProofView.mli b/ide/wg_ProofView.mli
index aa01d955d..a90d429d0 100644
--- a/ide/wg_ProofView.mli
+++ b/ide/wg_ProofView.mli
@@ -10,7 +10,7 @@ class type proof_view =
   object
     inherit GObj.widget
     method buffer : GText.buffer
-    method refresh : unit -> unit
+    method refresh : force:bool -> unit
     method clear : unit -> unit
     method set_goals : Interface.goals option -> unit
     method set_evars : Interface.evar list option -> unit
diff --git a/ide/xmlprotocol.ml b/ide/xmlprotocol.ml
index 5f80d6897..d7950e5fd 100644
--- a/ide/xmlprotocol.ml
+++ b/ide/xmlprotocol.ml
@@ -111,7 +111,7 @@ let to_box = let open Pp in
     )
 
 let rec of_pp (pp : Pp.std_ppcmds) = let open Pp in match Pp.repr pp with
-    | Ppcmd_empty         -> constructor "ppdoc" "emtpy"  []
+    | Ppcmd_empty         -> constructor "ppdoc" "empty"  []
     | Ppcmd_string s      -> constructor "ppdoc" "string" [of_string s]
     | Ppcmd_glue sl       -> constructor "ppdoc" "glue"   [of_list of_pp sl]
     | Ppcmd_box (bt,s)    -> constructor "ppdoc" "box"    [of_pair of_box of_pp (bt,s)]