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

On 07/11/16 13:55, Mathias Fleury wrote:
> 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.

This is merely an omission.

3 months ago, I allowed cartouches for file/path specifications in
Isabelle/ML (5a7c919a4ada), but forgot to do the same in Isabelle/Scala.
This is now done in


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