diff options
Diffstat (limited to 'ide')
| -rw-r--r-- | ide/coqOps.ml | 59 | ||||
| -rw-r--r-- | ide/ide_slave.ml | 2 | ||||
| -rw-r--r-- | ide/texmacspp.ml | 13 | ||||
| -rw-r--r-- | ide/wg_ProofView.ml | 22 | ||||
| -rw-r--r-- | ide/wg_ProofView.mli | 2 | ||||
| -rw-r--r-- | ide/xmlprotocol.ml | 2 |
6 files changed, 52 insertions, 48 deletions
diff --git a/ide/coqOps.ml b/ide/coqOps.ml index 4a1d688f51..3d6a2583fe 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 () ) ) @@ -403,10 +403,9 @@ object(self) List.iter (fun t -> buffer#remove_tag t ~start ~stop) all_tags; List.iter (fun t -> buffer#apply_tag t ~start ~stop) tags - method private attach_tooltip sentence loc text = + method private attach_tooltip ?loc sentence text = let start_sentence, stop_sentence, phrase = self#get_sentence sentence in - let pre_chars, post_chars = - if Loc.is_ghost loc then 0, String.length phrase else Loc.unloc loc in + let pre_chars, post_chars = Option.cata Loc.unloc (0, String.length phrase) loc in let pre = b2c phrase pre_chars in let post = b2c phrase post_chars in let start = start_sentence#forward_chars pre in @@ -469,25 +468,24 @@ object(self) self#mark_as_needed sentence | GlobRef(loc, filepath, modpath, ident, ty), Some (id,sentence) -> log "GlobRef" id; - self#attach_tooltip sentence loc + self#attach_tooltip ~loc sentence (Printf.sprintf "%s %s %s" filepath ident ty) | Message(Error, loc, msg), Some (id,sentence) -> - let loc = Option.default Loc.ghost loc in + let uloc = Option.default Loc.ghost loc in log_pp Pp.(str "ErrorMsg" ++ msg) id; remove_flag sentence `PROCESSING; let rmsg = Pp.string_of_ppcmds msg in - add_flag sentence (`ERROR (loc, rmsg)); + add_flag sentence (`ERROR (uloc, rmsg)); self#mark_as_needed sentence; - self#attach_tooltip sentence loc rmsg; - if not (Loc.is_ghost loc) then - self#position_error_tag_at_sentence sentence (Some (Loc.unloc loc)) + self#attach_tooltip sentence ?loc rmsg; + self#position_tag_at_sentence ?loc Tags.Script.error sentence | Message(Warning, loc, msg), Some (id,sentence) -> - let loc = Option.default Loc.ghost loc in + let uloc = Option.default Loc.ghost loc in log_pp Pp.(str "WarningMsg" ++ msg) id; let rmsg = Pp.string_of_ppcmds msg in - add_flag sentence (`WARNING (loc, rmsg)); - self#attach_tooltip sentence loc rmsg; - self#position_warning_tag_at_sentence sentence loc; + add_flag sentence (`WARNING (uloc, rmsg)); + self#attach_tooltip sentence ?loc rmsg; + self#position_tag_at_sentence ?loc Tags.Script.warning sentence; messages#push Warning msg | Message(lvl, loc, msg), Some (id,sentence) -> log_pp Pp.(str "Msg" ++ msg) id; @@ -522,28 +520,18 @@ object(self) let stop = buffer#get_iter_at_mark sentence.stop in buffer#move_mark ~where:stop (`NAME "start_of_input"); - method private position_error_tag_at_iter iter phrase = function - | None -> () - | Some (start, stop) -> - buffer#apply_tag Tags.Script.error - ~start:(iter#forward_chars (b2c phrase start)) - ~stop:(iter#forward_chars (b2c phrase stop)) - - method private position_error_tag_at_sentence sentence loc = - let start, _, phrase = self#get_sentence sentence in - self#position_error_tag_at_iter start phrase loc - - method private position_warning_tag_at_iter iter_start iter_stop phrase loc = - if Loc.is_ghost loc then - buffer#apply_tag Tags.Script.warning ~start:iter_start ~stop:iter_stop - else - buffer#apply_tag Tags.Script.warning - ~start:(iter_start#forward_chars (b2c phrase loc.Loc.bp)) - ~stop:(iter_stop#forward_chars (b2c phrase loc.Loc.ep)) + method private position_tag_at_iter ?loc iter_start iter_stop tag phrase = match loc with + | None -> + buffer#apply_tag tag ~start:iter_start ~stop:iter_stop + | Some loc -> + let start, stop = Loc.unloc loc in + buffer#apply_tag tag + ~start:(iter_start#forward_chars (b2c phrase start)) + ~stop:(iter_start#forward_chars (b2c phrase stop)) - method private position_warning_tag_at_sentence sentence loc = + method private position_tag_at_sentence ?loc tag sentence = let start, stop, phrase = self#get_sentence sentence in - self#position_warning_tag_at_iter start stop phrase loc + self#position_tag_at_iter ?loc start stop tag phrase method private process_interp_error queue sentence loc msg tip id = Coq.bind (Coq.return ()) (function () -> @@ -552,7 +540,7 @@ object(self) self#discard_command_queue queue; pop_info (); if Stateid.equal id tip || Stateid.equal id Stateid.dummy then begin - self#position_error_tag_at_iter start phrase loc; + self#position_tag_at_iter ~loc start stop Tags.Script.error phrase; buffer#place_cursor ~where:stop; messages#clear; messages#push Feedback.Error msg; @@ -666,6 +654,7 @@ object(self) if Queue.is_empty queue then loop tip [] else loop tip (List.rev topstack) | Fail (id, loc, msg) -> + let loc = Option.cata Loc.make_loc Loc.ghost loc in let sentence = Doc.pop document in self#process_interp_error queue sentence loc msg tip id in Coq.bind coq_query handle_answer diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml index 8cadf1a263..0dfa03cca0 100644 --- a/ide/ide_slave.ml +++ b/ide/ide_slave.ml @@ -193,7 +193,7 @@ let process_goal sigma g = pr_goal_concl_style_env env sigma norm_constr in let process_hyp d (env,l) = - let d = CompactedDecl.map_constr (Reductionops.nf_evar sigma) d in + let d = CompactedDecl.map_constr (fun c -> EConstr.Unsafe.to_constr (Reductionops.nf_evar sigma (EConstr.of_constr c))) d in let d' = CompactedDecl.to_named_context d in (List.fold_right Environ.push_named d' env, (pr_compacted_decl env sigma d) :: l) in diff --git a/ide/texmacspp.ml b/ide/texmacspp.ml index 6fbed38fb4..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,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 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 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)] |