Re: Emacs and jEdit

[Andreas Röhler]

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 <address@hidden> 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"