coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] external editor in coqide

From: Jeremy Dawson <Jeremy.Dawson AT anu.edu.au>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: [Coq-Club] external editor in coqide
Date: Thu, 24 Jan 2019 05:44:40 +0000
Accept-language: en-US
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=Jeremy.Dawson AT anu.edu.au; spf=Pass smtp.mailfrom=Jeremy.Dawson AT anu.edu.au; spf=Pass smtp.helo=postmaster AT AUS01-SY3-obe.outbound.protection.outlook.com
Ironport-phdr: 9a23:ILTZDxDrfG2m+QzYZn01UyQJP3N1i/DPJgcQr6AfoPdwSPX7pcbcNUDSrc9gkEXOFd2Cra4c26yO6+jJYi8p2d65qncMcZhBBVcuqP49uEgeOvODElDxN/XwbiY3T4xoXV5h+GynYwAOQJ6tL1LdrWev4jEMBx7xKRR6JvjvGo7Vks+7y/2+94fcbglUhzexe69+IAmrpgjNq8cahpdvJLwswRXTuHtIfOpWxWJsJV2Nmhv3+9m98p1+/SlOovwt78FPX7n0cKQ+VrxYES8pM3sp683xtBnMVhWA630BWWgLiBVIAgzF7BbnXpfttybxq+Rw1DWGMcDwULs5Xymp4aV2Rx/ykCoJNyA3/nzLisJ+j6xboQ6uqRNwzIPPfIGaL+Bzcr/Bcd8GR2dMWNtaWSxbAoO7aosCF+4PMvhCr4bjolsPrQa1Cwe2C+Lh0T9IgXn21rA93uolDw7GxhIvH9cOsXjOotv6LqkTUfuyzKnO1jjMdfVW2Srn5IfWbx8hvOuAUqhtccfIz0QkCg3LjlKVqYP/PjOV0PwAs2md7+p6VOKgkXQrqw9rojWp28wiiZHJi5oax1zY7yl13Zo5KN+iREJmb9OpEoFcuiWHO4duX88vQ31ktDwkxrEat5O3ZjYGxIk7yxLFdvCKfYyF7grtVOmPIjp0mHdodbe7ihux6ketxejxWtS63VlUsyVIl9fMuW4O2hDP78WLVOBy/kmu1DuJygvd8PtLIVoumqreM5MhwqA/lp4UsUnbAiL5llj4gLOLekk95+an6erqbqzhppCHKYB4kAb+MrkymsOkBuQ4Lw4OUHWB9eSkzr3j+lH5T6tWgf0qk6nZt5baKd4cpq6kHw9V1oEj6xG8Dzu8zNsYmnwHIEpEeBKBkYfpJ0nDLf/kAfulnligjDVmy+rbMrDvAJjBNHzOnKr5cbZ48UFcyQ4zzd5F55JTD7EMOPb9VVHrtNPGCx84Mxa4zej9B9RzzYMeXmSPD7SDP6PUrF+E/PwgLPSRZIMPojn9NuAp5+Tygn8hhV8dYa6p0IMLZ3C/B/RqOlmWYX7xgtgaCmoKpQo/TOnyiFKYSzJTZnCyX7g95j4hEo6mA53DFciRh+nL1yCiW5ZSe2puC1aWEH6ueZ/OE6MHbzvXKct8mBQFU6KgQskvz0f9mhX9zu9FI/DZ/zxQmZv8z99zr7nxmAs/8C0yI82CyGaLZ2hygyUFSyJw1b0p8h818UuKzaUt268QLtdU/f4cCl5rZ66Z9PRzDpXJYiyEe96ITFi8RdD/W2M4SM93ztMTJU9gSYz70kLzmhGyCrpQrISlQYQu+/uGjXH3OoBwx2uA3bRz1wB7EPsKDnWvg+tEzyaWB4PNlBnGxY+XTvxFmRX8ryKEx2fIu1xEWgltV6mDRWoYekbdsdX+4AXFUqOqDrMkdABGzJzbJw==
Spamdiagnosticmetadata: NSPM
Spamdiagnosticoutput: 1:99

Hi,

the documentation at
https://coq.inria.fr/distrib/current/refman/practical-tools/coqide.html
says

CoqIDE offers only basic editing commands, so if you need more complex
editing commands, you may launch your favorite text editor on the
current buffer, using the Edit/External Editor menu.

But I find the Edit/External Editor menu simply starts up another window
which seems to be something to do with emacs.

So how do I start up my usual text editor (vi) while using coqide?

Thanks,

Jeremy

[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