From d91a0c27402f0f19a30147bb9d87387ca2a91fd0 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Thu, 2 Feb 2017 10:18:48 +0100 Subject: "Standardizing" the name LocalPatten into LocalRawPattern. --- ide/texmacspp.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'ide') diff --git a/ide/texmacspp.ml b/ide/texmacspp.ml index 6fbed38fb4..7bbf393ac9 100644 --- a/ide/texmacspp.ml +++ b/ide/texmacspp.ml @@ -235,7 +235,7 @@ and pp_local_binder lb = (* don't know what it is for now *) let ppl = List.map (fun (loc, nam) -> (xmlCst (string_of_name nam) loc)) namll in xmlTyped (ppl @ [pp_expr ce]) - | LocalPattern _ -> + | LocalRawPattern _ -> assert false and pp_local_decl_expr lde = (* don't know what it is for now *) match lde with -- cgit v1.2.3 From 648ce5e08f7245f2a775abd1304783c4167e9f2e Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Thu, 2 Feb 2017 18:24:58 +0100 Subject: Unifying standard "constr_level" names for constructors of local_binder_expr. RawLocal -> CLocal --- ide/texmacspp.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'ide') diff --git a/ide/texmacspp.ml b/ide/texmacspp.ml index 7bbf393ac9..e705e4e5a1 100644 --- a/ide/texmacspp.ml +++ b/ide/texmacspp.ml @@ -228,14 +228,14 @@ 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 ((_, nam), ce) -> let attrs = ["name", string_of_name nam] in pp_expr ~attr:attrs ce - | LocalRawAssum (namll, _, ce) -> + | CLocalAssum (namll, _, ce) -> let ppl = List.map (fun (loc, nam) -> (xmlCst (string_of_name nam) loc)) namll in xmlTyped (ppl @ [pp_expr ce]) - | LocalRawPattern _ -> + | CLocalPattern _ -> assert false and pp_local_decl_expr lde = (* don't know what it is for now *) match lde with -- cgit v1.2.3 From f9a4ca41bc1313300f5f9b9092fe24825f435706 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Wed, 1 Feb 2017 15:56:45 +0100 Subject: Replacing "cast surgery" in LetIn by a proper field (see PR #404). This is a patch fulfilling the relevant remark of Maxime that an explicit information at the ML type level would be better than "cast surgery" to carry the optional type of a let-in. There are a very few semantic changes. - a "(x:t:=c)" in a block of binders is now written in the more standard way "(x:=c:t)" - in notations, the type of a let-in is not displayed if not explicitly asked so. See discussion at PR #417 for more information. --- ide/texmacspp.ml | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) (limited to 'ide') diff --git a/ide/texmacspp.ml b/ide/texmacspp.ml index e705e4e5a1..e787e48bf1 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,9 +229,10 @@ 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 - | CLocalDef ((_, nam), ce) -> + | CLocalDef ((loc, nam), ce, ty) -> let attrs = ["name", string_of_name nam] in - pp_expr ~attr:attrs 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 @@ -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]) -- cgit v1.2.3 From df1d4dc9c3808a811111e4cd9eeda328b51f20de Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Tue, 28 Mar 2017 00:06:21 +0200 Subject: [coqide] Protect against size_allocate race in proofview. To handle dynamic printing in CoqIDE we listen to the `size_allocate` signal , [see more details in 6885a398229918865378ea24f07d93d2bcdd2802] However, we must be careful to protect against scrollbar creation: it is possible for the `size_allocate` handler to change the size when inserting text (due to scrollbars), thus we may enter in an infinite loop. Our fix is to check if the width has really changed, as done in `Wg_MessageView`. This fixes the problem noted by @herbelin in https://coq.inria.fr/bugs/show_bug.cgi?id=5417 --- ide/coqOps.ml | 2 +- ide/wg_ProofView.ml | 22 +++++++++++++++++----- ide/wg_ProofView.mli | 2 +- 3 files changed, 19 insertions(+), 7 deletions(-) (limited to 'ide') diff --git a/ide/coqOps.ml b/ide/coqOps.ml index 4a1d688f51..45b5a1007a 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/wg_ProofView.ml b/ide/wg_ProofView.ml index b5405570c9..3cbe583881 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 aa01d955d0..a90d429d04 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 -- cgit v1.2.3 From 026edb0b10eaf96f7f9f4e806bd3a0fa19b29407 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 29 Mar 2017 14:27:39 +0200 Subject: [ide] Fix typo in pp serialization. --- ide/xmlprotocol.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'ide') diff --git a/ide/xmlprotocol.ml b/ide/xmlprotocol.ml index 5f80d68974..d7950e5fd5 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)] -- cgit v1.2.3