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

[Christian Sternagel]

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