From mboxrd@z Thu Jan 1 00:00:00 1970 Path: news.gmane.org!not-for-mail From: =?UTF-8?Q?Andreas_R=c3=b6hler?= Newsgroups: gmane.emacs.devel Subject: Re: Emacs and jEdit Date: Mon, 18 Jul 2016 19:09:38 +0200 Message-ID: <7af0c6b4-22be-7b0d-7ffa-c2a429e8a7d4@online.de> References: <611049b7-d084-cace-1e9d-513122d4bf97@online.de> <930040a6-f778-ad44-2b61-0b60af9c6398@online.de> NNTP-Posting-Host: plane.gmane.org Mime-Version: 1.0 Content-Type: text/plain; charset=windows-1252; format=flowed Content-Transfer-Encoding: 7bit X-Trace: ger.gmane.org 1468862199 27764 80.91.229.3 (18 Jul 2016 17:16:39 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Mon, 18 Jul 2016 17:16:39 +0000 (UTC) To: emacs-devel@gnu.org Original-X-From: emacs-devel-bounces+ged-emacs-devel=m.gmane.org@gnu.org Mon Jul 18 19:16:30 2016 Return-path: Envelope-to: ged-emacs-devel@m.gmane.org Original-Received: from lists.gnu.org ([208.118.235.17]) by plane.gmane.org with esmtp (Exim 4.69) (envelope-from ) id 1bPC9a-0001R3-Vi for ged-emacs-devel@m.gmane.org; Mon, 18 Jul 2016 19:16:27 +0200 Original-Received: from localhost ([::1]:49124 helo=lists.gnu.org) by lists.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1bPC9a-000063-3p for ged-emacs-devel@m.gmane.org; Mon, 18 Jul 2016 13:16:26 -0400 Original-Received: from eggs.gnu.org ([2001:4830:134:3::10]:43866) by lists.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1bPBy0-0003CO-F8 for emacs-devel@gnu.org; Mon, 18 Jul 2016 13:04:29 -0400 Original-Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1bPBxv-0006ON-CC for emacs-devel@gnu.org; Mon, 18 Jul 2016 13:04:27 -0400 Original-Received: from mout.kundenserver.de ([212.227.17.13]:58008) by eggs.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1bPBxv-0006OG-2o for emacs-devel@gnu.org; Mon, 18 Jul 2016 13:04:23 -0400 Original-Received: from [192.168.178.35] ([77.12.45.54]) by mrelayeu.kundenserver.de (mreue103) with ESMTPSA (Nemesis) id 0M3MGG-1b7nfh40iu-00qzbE for ; Mon, 18 Jul 2016 19:04:22 +0200 User-Agent: Mozilla/5.0 (X11; Linux i686; rv:45.0) Gecko/20100101 Icedove/45.1.0 In-Reply-To: X-Provags-ID: V03:K0:krVFeBOvClJ5CA8qZGthrpPIP/0R9Y42uFILOLi53mSzj/nJiRj pvMfTVBW0BuaXHBuJQ4f7k39opb7Tcm8koCWJOBgm5ohIp02bbRO9yiD05SlySJfiUR21wW IMUtFbPZy5luYQDKcAYmoWPWLYgTbBzHbdWY8AzHleyhTUgHn0SHePJsaS40RokKGXcCZTE 56YdGOtqOYeXf2OUGi7qA== X-UI-Out-Filterresults: notjunk:1;V01:K0:9uU00mCa6OY=:wu59BP4S4tIXnC74rlaCOl RPvApnY2wjZyyj3xG8WxW9Eo24O2glCKRnV5zydzHz+0lyy//fwdPjmPheU64Ce5vYdDFIeW/ zT1ptLnq1em8fuTWzIUKKoVjMHsDS3rEPX2cF6vUfocY8R4LiGIEGyExvaRSYlE/pqugyzuit NM2letmhLEby35Nm831saw4EMUlE7sOMsbYTyWzRIGuL43N6F/VuISmFYcX1SNjcNMAWAB7Mt e6feeWudAb78xCFxVQC+7tYPG2gT+PsCj/Js24jzjrwV6u3MaA6PUmD2tWA1eFv4cjM5kIS89 wO/Bwhd1YA9KmpmOBRO8Lk4q1KjIeJTJ0ja1Pthi5Gts6UJGxXXD9NBN7tHv2epOqQ45QGscw WYAky3/mGW9nmXKn5ViIYMXEKIZKaFluui30mSnJS9q4sTJXu5Ptu9IqUfLK+Fxl61nfczoiU C64XP++NCU//vrGtq0UFUiRT7fb99cDPaRuTvgNGey039Lrsvvh1frv+NiC5hvRlC0jPMpl7H OaAj4vFJA6XgD+b/yvxMQPCeNEflfxDyXvYD2dfuezKcVfXKp37IPjFTl8VEt7X9BRdRmB0jF 7W3NSMqZmgQX4CfNwdXP79CCvvQ2jk2l++GqAb+vCQ+xmkQJKXdlo5O9tozux+4U+YyxgPriz p/Z+XgNaa0T0mThZeqFdh8ARgHbag2Pj/un3ydN8J+aTbtKbId+bU+4iGX4RMZIRdYBSAgDgG EHG173asB0axja5/ X-detected-operating-system: by eggs.gnu.org: GNU/Linux 2.2.x-3.x [generic] X-Received-From: 212.227.17.13 X-BeenThere: emacs-devel@gnu.org X-Mailman-Version: 2.1.21 Precedence: list List-Id: "Emacs development discussions." List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: emacs-devel-bounces+ged-emacs-devel=m.gmane.org@gnu.org Original-Sender: "Emacs-devel" Xref: news.gmane.org gmane.emacs.devel:205816 Archived-At: On 18.07.2016 16:56, Stefan Monnier wrote: >> It was supported inside proof-general. But support was withdrawn from >> Isabelle/HOL's side, going frustrated by ongoing difficulties IIUC. > Huh? Isabelle/HOL developed a fancier protocol/interface for its > various IDEs. Noone was interested in updating the Emacs-side support > (within Proof-General) to use this new protocol (it required > a significant rewrite because the new protocol works completely > differently). Then Isabelle/HOL decided to drop support for the old > protocol (at that point only used for Emacs, and the lack of interest in > adapting Emacs's support to the new protocol being taken as a sign that > there weren't enough Emacs users to bother maintaining support for the > old protocol inside Isabelle/HOL). > > I can't see any "ongoing difficulties" there. > > FWIW, Coq has introduced similarly fancier protocols and since there are > more Emacs+Coq users, some people have taken on the task of updating > Emacs's support (in Proof-General) to use that new protocol (still > ongoing work, AFAIK). And that work might actually prove useful to > re-introduce Isabelle/HOL support in there, tho that will depend on > whether there's enough motivation for someone to do that part of > the work. > > > Stefan > > Correction taken WRT protocol, thanks. Being interested to take part delivering a new port. Beside sml-mode.el seems to have some issues. IMO one reason is smie introducing complexity.