Re: [isabelle] isabelle/jedit



Welcome, Gergely,

Le Wed, 08 Aug 2012 09:03:43 +0200, Gergely Buday <gbuday at gmail.com> a écrit:

Hi,

at http://arxiv.org/pdf/1208.1368v1.pdf

Christian Sternagel writes:

4.3 Where have all the menus gone?

In Proof General many settings of Isabelle and diagnostic commands
could be con%0Cgured and
started via menus. This is currently not supported in Isabelle/jEdit.

---

Is there any technical reason for this?

- Gergely



If you don't mind about a tiny re-interpretation, I would say a more important question would be “is that really an issue?”. I believe there are many purely intuitionist proof by exposition of good artifacts, that the Isabelle jEdit tuple is a good one (teasing and playing with words).

Note that you have the option to set Isabelle's flag from within a theory file, ex. like writing “using [[simp_trace=true]]” in a proof body. You may hide from the produced PDF document, using a special comment syntax, like writing “(*<*)using [[simp_trace=true]](*>*)”. By the way, I believe there may be a tiny issue with the simp_trace flags, … will open a thread about it later.

Cheers


--
“Syntactic sugar causes cancer of the semi-colons.” [1]
“Structured Programming supports the law of the excluded muddle.” [1]
[1]: Epigrams on Programming — Alan J. — P. Yale University






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.