On 04/18/2012 03:42 PM, Lawrence Paulson wrote:
How do you do “show me", “commands", “find theorem", “settings", etc? I believe
you're supposed to remember commands for all of those items and type them explicitly. That's not
what a user interface is supposed to do.
Actually I did never use these in emacs either... but I see your point
(which is of course valid).
A further problem is you cannot cut and paste between the “proof" window and
the main window, so good luck creating any structured proofs (unless you love typing
lots of formal text and never make mistakes). And on a Mac, the keyboard shortcuts
are different from the usual.
I don't get it. Copying and pasting between the output buffer and the
main buffer works just fine for me (a bit odd is that you have to use
Ctrl+C and Ctrl+V, since the linux-typical marking with mouse and middle
click does not work (yet (?))). But maybe this is different in Mac OS.
cheers
chris
Larry
On 18 Apr 2012, at 02:53, Christian Sternagel wrote:
Just for the record: I exclusively use jEdit for several weeks now and did
quite a lot of actual proofs. My personal opinion: the user experience is much
nicer than with emacs
* I did not have any complete hangs yet (as with emacs)
* the whole appearance is much nicer (remember, this is my personal
opinion): font, highlighting, ...
* not to forget the browsability (from constants to their
definitions; from ML functions to their modules)
* checking a single theory (in non-batch mode) is MUCH faster than
with emacs
I would not for the world go back to emacs. (Maybe I should mention that before Isabelle
I did not use emacs at all, so it was quite annoying to have to learn an "operating
system" when I just needed an editor ;)).
cheers
chris
On 04/18/2012 01:08 AM, Lawrence Paulson wrote:
I certainly care about it. Jedit is great for browsing existing theory
developments, but there is no support for actually doing proofs.
Larry
On 17 Apr 2012, at 16:56, Makarius wrote:
Anyway, who is maintaining Isabelle ProofGeneral now? The repository version
does not work with Emacs 23 for several months already. It seems that nobody
cares about it anymore.
For the release, I will package up official ProofGeneral-4.1 as last time. It
is then up to its users to test it and report problems in the usual testing
stage before the release.
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
