[isabelle] Isabelle2016-1-RC2 cartouche vs quotation mark ML_file

Dear Isabelle list,

I am a heavy cartouche user. However, they behave differently for arguments of ML_file: ML_file "path/to/file.ML" allows to open the SML file when clicking on the quoted part, while ML_file âpath/to/file.MLâ does not.

Moreover, with the cartouches the dependencies are not tracked; i.e., when I change the SML file, the theory that imports the file (opened in a second buffer) is not automatically reprocessed.

Is there any technical reason?


> On 6 Nov 2016, at 21:32, Makarius <makarius at sketis.net> wrote:
> Dear Isabelle users,
> a bit more than 1 week after the first release candidate for
> Isabelle2016-1 (December 2016) there is now
> http://isabelle.in.tum.de/website-Isabelle2016-1-RC2. Changes wrt. RC1
> are relatively small, see the Mercurial history for details.
> The corresponding repository versions of Isabelle and AFP are
> https://bitbucket.org/isabelle_project/isabelle-release/commits/91c98a58985b
> and https://bitbucket.org/isa-afp/afp-devel/commits/0f8371312d71
> The website, NEWS, ANNOUNCE etc. are up-to-date, but some
> documentation is still lagging behind.
> It is also possible to follow nightly development snapshots from
> http://isabelle.in.tum.de/devel although they might be somewhat erratic.
> When discussing problems, observations, suggestions, etc. the mail
> subject line should be changed to something informative, and the
> particular Isabelle version given in the message body.
> The Isabelle release process is subject to the laws of causality:
> release candidates can be modified, but the final release remains final.
> Testing needs to happen in the weeks before the final release, not after it.
> 	Makarius

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