search

cpitclaudel / company-coq

A Coq IDE build on top of Proof General's Coq mode
GNU General Public License v3.0
349 stars 30 forks source link

company-coq-mode deletes the goals line #167

Open JasonGross opened 7 years ago

JasonGross commented 7 years ago

In emacs 25.2.50.1: image In emacs 24.5.1: image

cpitclaudel commented 7 years ago

Aren't you just running different versions of company-coq?

cpitclaudel commented 7 years ago

(I pushed a recent change that simplified some code but may have broken the continuous line on terminals). It looks like you're running that code in Emacs 25, but not in Emacs 24.5.

JasonGross commented 7 years ago

Ah, yes, when I fix #166, and update company-coq for emacs 24, the goal line disappears there, too.

JasonGross commented 7 years ago

Is there anything I can change locally in my ~/.emacs to get the goals line back?

cpitclaudel commented 7 years ago

Can you try (setq company-coq-goal-separator-spec nil) before loading company-coq?