Re: [isabelle] Isabelle2014-RC0 available for testing



>
> And another thing worth noting, although already present in the 2013
> release: When jumping to a file that is loaded as part of the loaded
> heap (e.g. Set), there is an error at the theory command: “Cannot update
> finished theory "Set"”. That makes sense to me, but I don’t plan to
> update the theory, I just want to navigate it. Currently, this prevents
> me from using Ctrl-Click on definitions in that file to navigate
> further.


I consider this a major drawback of previous Isabelle/jEdit releases.

Best!


On Tue, Jul 8, 2014 at 11:46 AM, Joachim Breitner <breitner at kit.edu> wrote:

>
> Hi,
>
> thanks for the RC!
>
> Am Samstag, den 05.07.2014, 20:04 +0200 schrieb Makarius:
> > This is an opportunity to look how things will presumably be in the
> > release, and to report problems, either on the isabelle-users mailing
> list
> > or via private mail.
>
> I tried to collect my minor observations, but it turns out that all of
> them have been reported before. Anyways, here are those collected today:
>
>
>  * I just observed an error message in the output window:
>         Undefined constant: "list.size"⌂
>   And I wonder what the ⌂ is about.
>
>
>   * The spellchecker doesn’t know about a few probably Isabelle specific
>     words such as “instantiation”. Maybe these should be added?
>
>
>   * Messages like „Metis: Unused theorems:“ appear below the goal state
>     in the output panel, which is less convenient than the previous
>     order.
>
>   * It is irritating that auto-completion does not work when there is a
>     letter following the cursor. But maybe I just need to get used to
>     that.
>
>   * No select-to-clipboard in the output window under Linux.
>
> And another thing worth noting, although already present in the 2013
> release: When jumping to a file that is loaded as part of the loaded
> heap (e.g. Set), there is an error at the theory command: “Cannot update
> finished theory "Set"”. That makes sense to me, but I don’t plan to
> update the theory, I just want to navigate it. Currently, this prevents
> me from using Ctrl-Click on definitions in that file to navigate
> further.
>
> Greetings and thanks,
> Joachim
>
> --
> Dipl.-Math. Dipl.-Inform. Joachim Breitner
> Wissenschaftlicher Mitarbeiter
> http://pp.ipd.kit.edu/~breitner
>



-- 
Alfio Ricardo Martini
PhD in Computer Science (TU Berlin)
Associate Professor at Faculty of Informatics (PUCRS)
www.inf.pucrs.br/alfio
Av. Ipiranga, 6681 - Prédio 32 - Faculdade de Informática
90619-900 -Porto Alegre - RS - Brasil



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.