coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] external editor in coqide

From: Jason -Zhong Sheng- Hu <fdhzs2010 AT hotmail.com>
To: Jeremy Dawson <Jeremy.Dawson AT anu.edu.au>, "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: Re: [Coq-Club] external editor in coqide
Date: Tue, 29 Jan 2019 03:29:00 +0000
Accept-language: en-CA, en-US
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=fdhzs2010 AT hotmail.com; spf=Pass smtp.mailfrom=fdhzs2010 AT hotmail.com; spf=Pass smtp.helo=postmaster AT NAM01-BN3-obe.outbound.protection.outlook.com
Ironport-phdr: 9a23:waqZFBwiH6E5szfXCy+O+j09IxM/srCxBDY+r6Qd2uwfIJqq85mqBkHD//Il1AaPAd2Lraocw8Pt8InYEVQa5piAtH1QOLdtbDQizfssogo7HcSeAlf6JvO5JwYzHcBFSUM3tyrjaRsdF8nxfUDdrWOv5jAOBBr/KRB1JuPoEYLOksi7ze+/94HQbglSmDaxfa55IQmrownWqsQYm5ZpJLwryhvOrHtIeuBWyn1tKFmOgRvy5dq+8YB6/ShItP0v68BPUaPhf6QlVrNYFygpM3o05MLwqxbOSxaE62YGXWUXlhpIBBXF7A3/U5zsvCb2qvZx1S+HNsDtU7s6RSqt4LtqSB/wiScIKTg58H3MisdtiK5XuQ+tqwBjz4LRZoyeKfhwcb7Hfd4CRWRPQNtfVzBPDI2/YYsADfYOMulDoobnu1cCsQGzCRWwCO/xzDJDm3/43bc90+QkCQzI2BYvH8kJsHTSsd75LaQdUeCyzKnOwjXIcu5Y2Tfj54jOfRAtuOyHU7BtccHMzkQvGR7KjlWRqIz+IT+ZyvkBv3SA4upgUuKvl2snpBtwojir3Msjlo7JhocMx13C6C53zoE1JdiiR056Z96pCIBQtiGBN4tqX8MiX2ZouDw7yrIcvZ67ZzIGx4ggxx7abfGMbouG4gr7WeuePTt0nnZodKylixqu60StyOLxWtG60FlUrSdJjtzBu3UT2BHc8MeLVP5w80Wu1DuB2QDe7+9ELE8omqfYLpMt36M/m5USvEnFAyT4gl/5jLWMeUUh4uWo6/roYrHhppKEL4F5lgbwPrgzlsCmHOk2KgYDU3Gc+eunyrLv50r5QKhWjvItlanZrZbaKtkBqq6hGQ9V1Zoj5AijADe60dQYmn8HIEhCeBKak4jpP1bOIPf7Dfuln1uslzJry+jHPr3nHJrNMmDOnbj9cbpn70NQ1hA/wcxF659WBbwNOPfzVVXwtNzcAB85KQu0w+P/BdVzy4weWWOOArSHPK/OrFOE+vkiI+mLZI8JvTbyMfkl5/r0gXAlnl8deLGl3YELZ3CgAvRmP0KZbGLwjdcGCGcGpxYxTOj3iFKZSjNTfHazX6ck5j4hEo6mDIHDRpqsgLObxiu7EIdWNSh6DQWuHG3lcpTMd/4TcyWUaptDnyYJUKnnZ4Y+zhaonAb81vxqIveS8zBO8dqp399soubXiBsa9DpuDs3b3XvHBzV/mXpNTDsr1oh+p1Z8wxGNy/4rreZfEIlx7uhOVE9/B57byeMyMND/XA2ENveUAAKoTtW0GmtpF4oZw9gSZk98H5OpiRWVjHniOKMci7HeXM98yanbxXWkYp8lky+XhplktEEvR450DUPjg6d+8wbJAIuQyBeZkLqvfKUYmiXK8TXalDbcjARjSAd1FJ79czUHfEKP9ob54V/HRr6qT78gN1kZkJPQGu5xctTsyG5+arLjNdDZPz3jvU6VXU/N7JXXKY3gdiMawTnXD1UCn0YL53GaOAMiByCn5WXDEDhpElGpaETpo7Bz

Have you installed a vim with gui at all? try gvim

https://www.systutorials.com/docs/linux/man/1-gex/

Sincerely Yours,

Jason Hu

From: coq-club-request AT inria.fr <coq-club-request AT inria.fr> on behalf of Jeremy Dawson <Jeremy.Dawson AT anu.edu.au>
Sent: January 28, 2019 10:21 PM
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] external editor in coqide

Hi Laurent,

I tried this, and it said /bin/sh: 1: gex: not found

Is it in fact the name of the editor that should go here?
Is gex another (similar?) editor?

So I tried putting vi here, and I got
Vim: Warning: Output is not to a terminal

What should I try next?

Cheers,

Jeremy

On 24/1/19 8:45 pm, Laurent Thery wrote:
>
>
> On 1/24/19 6:44 AM, Jeremy Dawson wrote:
>> So how do I start up my usual text editor (vi) while using coqide?
>
> You can configurate the editor in Edit->Preferences->Externals->External
> Editor replacing emacs by gex
>
> --
> Laurent
>

[Coq-Club] external editor in coqide, Jeremy Dawson, 01/24/2019
- Re: [Coq-Club] external editor in coqide, Laurent Thery, 01/24/2019
  - Re: [Coq-Club] external editor in coqide, Théo Zimmermann, 01/24/2019
    - Re: [Coq-Club] external editor in coqide, Anders Lundstedt, 01/24/2019
  - Re: [Coq-Club] external editor in coqide, Jeremy Dawson, 01/29/2019
    - Re: [Coq-Club] external editor in coqide, Jason -Zhong Sheng- Hu, 01/29/2019
      - Re: [Coq-Club] external editor in coqide, Jeremy Dawson, 01/29/2019