Re: Emacs and jEdit

["Andreas Röhler" <andreas.roehler@online.de>]

[-- Attachment #1: Type: text/plain, Size: 1586 bytes --]



On 18.07.2016 14:11, Kaushal Modi wrote:
> Hi Andreas,
>
> I didn't quite follow that email.
>
> What is Isabelle/HOL?

Isabelle/HOL is a theorem prover, used to prove the correctness of code 
for example.
Like Coq or ACL2.


> Do the screenshots illustrate that jEdit can render Isabelle files 
> fine, but emacs does not?

To the extend shown, that's the purpose.

>
> Is this a request for a new major mode in emacs to support Isabelle?

It is an renewed alert. Already mentioned circular dependencies related 
to syntax-propertize for example, which make this section hard to debug 
and maintain. Also think the smie-stuff might be considered as failing.

>
> Or was this supported earlier and is now broken?

It was supported inside proof-general. But support was withdrawn from 
Isabelle/HOL's side, going frustrated by ongoing difficulties IIUC.


>
> On Mon, Jul 18, 2016, 6:17 AM Andreas Röhler 
> <andreas.roehler@online.de <mailto:andreas.roehler@online.de>> wrote:
>
>     Hi all,
>
>     mentioned the switch of Isabelle/HOL from Emacs to jEdit.
>
>     Attach a showcase displaying a portion of source in Emacs and jEdit,
>     which should illustrate the matter. 
>
>
>
>     sml.png refers to sml-mode.el from
>     Melpa.
>
>
> I'll assume that the emacs screenshot is sml.png :)

Right.

> I do not see that file names in my email client, just the images 
> directly. So the sml-mode was supposed to render the tags in that file 
> properly?
>
> -- 
>
> Kaushal Modi
>

Yes. Isabelle/HOL uses an dialect of SML internally, files are indicated 
by the ending ".thy"

[-- Attachment #2: Type: text/html, Size: 4149 bytes --]