Re: [isabelle] isabelle/jedit
Le Wed, 08 Aug 2012 09:03:43 +0200, Gergely Buday
<gbuday at gmail.com> a écrit:
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?
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.
“Syntactic sugar causes cancer of the semi-colons.” 
“Structured Programming supports the law of the excluded muddle.” 
: Epigrams on Programming — Alan J. — P. Yale University
This archive was generated by a fusion of
Pipermail (Mailman edition) and