Jedit setup line endings how to#
The remaining problem is how to do that systematically, without having to specify and implement complex protocols for prover interaction.This is the point where we introduce the new Isabelle/Scala layer, which is meant to expose certain aspects of Isabelle/ML to the outside world.
After some recent reworking of Isabelle internals, to support parallel processing of theories and proofs, the original idea of structured document processing has surfaced again.Isabelle versions from 2009 or later already provide some support for interactive proof documents with asynchronous checking, which awaits to be connected to a suitable editor framework or full-scale IDE. Can we do better than that?Ten years ago, the Isabelle/Isar proof language already emphasized the idea of proof document (structured text) instead of proof script (sequence of commands), although the implementation was still emulating TTY interaction in order to be able to work with the then emerging Proof General interface. There have been some attempts to re-implement prover interfaces in big IDE frameworks, while keeping the old interaction model. Even well-known Emacs modes for such provers follow this synchronous model based on single commands with immediate response, meaning that the editor waits for the prover after each command. After several decades, most proof assistants are still centered around TTY-based interaction in a tight read-eval-print loop.
0 kommentar(er)
