On 04/18/2012 03:56 PM, Christian Sternagel wrote:
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...
Just to be clear: I did of course use these commands, but not from the
emacs menue.
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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
