Milan Tom (May 12 2025 at 09:04): Milan Tom (May 12 2025 at 09:04):I have produced a program that uses Isabelle/Scala to provide a REPL-like interface to Isabelle. It can send snippets and receive outputs and errors as they would be seen in Isabelle/jEdit. I have made several Isabelle/ML utility functions that extract things like current proof state and my current mode of invoking these functions is by inserting ML_val snippets directly into the proof document.
I know there is support for invoking Isabelle/Scala functions from Isabelle/ML via antiquotations. Is the way I am invoking Isabelle/ML from Isabelle/Scala the best way or is there some other way I can do it without incurring the overhead of sending the edits for these function calls?
Last updated: Jun 08 2025 at 08:25 UTC