[isabelle-dev] jEdit Output Panel

[Christian Sternagel]

Dear Makarius,

I just started to play around with the latest and greatest 
Isabelle/jEdit (there have been several promising commits during my 
absence).


Now I wanted to file a bagatelle ;). (I'm on changeset 10b89c127153.) 
Minimal example:

 - start Isabelle/jEdit
 - type theory Scratch (observe the output panel while typing)
we get: Outer syntax error: keyword begin expected, but end-of-file 
was found

 - continue typing imports Main begin
we still have Outer syntax error: keyword begin expected, but 
end-of-file was found in the output panel (although no errors are 
indicated in the main buffer or the gutter anymore).


It seems as if the output panel is slightly out-of-sync w.r.t. the 
cursor.


cheers

chris
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Isabelle/jEdit: Feature Requests for Ctrl-Click

[Christian Sternagel]

I would also regard all of the below suggestions as rather convenient (I 
wanted to asked for 1 and 4 myself already several times, but somehow 
never got around). - cheers chris


On 08/13/2012 09:50 PM, Tjark Weber wrote:

Hi,

Ctrl-click in Isabelle/jEdit exposes additional information - about
the next best thing since sliced bread. I have a few suggestions for
related features that would be nice to have, in my opinion (provided
they are not too much implementation work):

1) In theory T imports A, I'd like to be able to Ctrl-click on A to
open the corresponding theory file.

2) In use filename, I'd like to be able to Ctrl-click on filename to
open the corresponding file.

3) In ML {* open Foo; *}, I'd like to be able to Ctrl-click on Foo to
see its definition.

4) Ctrl-click on an ML identifier takes me to its declaration (typically
in some signature). Wouldn't it be more useful to be taken to its
definition (i.e., the actual implementation, typically in a structure)?

Best regards,
Tjark



___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev