[isabelle-dev] <-> and <-->

[Christian Sternagel]

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-dev at in.tum.de
>>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>>
>> _______________________________________________
>> isabelle-dev mailing list
>> isabelle-dev at in.tum.de
>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>