Email Gateway (Aug 22 2022 at 14:35): Email Gateway (Aug 22 2022 at 14:35):From: Mathias Fleury <mathias.fleury12@gmail.com>
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?
Mathias
Email Gateway (Aug 22 2022 at 14:35):From: Makarius <makarius@sketis.net>
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
https://bitbucket.org/isabelle_project/isabelle-release/commits/c40c2975fb02
Makarius
Last updated: Apr 25 2024 at 16:19 UTC