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