Email Gateway (Aug 19 2022 at 10:41): Email Gateway (Aug 19 2022 at 10:41):From: Makarius <makarius@sketis.net>
On Tue, 26 Feb 2013, Avi Knoll wrote:
Regarding the Isabelle/Scala API: Does anyone know how I might use
session.update (or any other method call) to apply edits to a previous
Document.Version, or alternately how to move the session to a different
Document.Version so I can then apply updates from that point?
The Document.update operation works with explicit ids for the old and new
version, but this functional update model is not continued in
Session.update, which is presently the main way you access the PIDE
document model.
The Session module (in Scala) essentially models an editor-like session,
as later used for Isabelle/jEdit. Such editors work in an old-school
stateful way, which also causes problems in different areas, outside the
scope of this thread. Thus there is a certain bias in
Session.global_state to move forward in a certain manner, never backwards.
Instead of navigating the history in a way you would expect from purely
functional content, I would say it is easier to move forward and apply
inverted edits. In other words you remove what you've inserted before.
The document model will clear out old stuff at some point; this can be
also configured in the Session.prune parameters, if you setup your own
Session instance in Scala.
The context is straightforward: I would like to apply a change, and then
revert it (i.e. 'undo') if the prover fails after the change. I would
like to do this without starting a new session, as that seems
unnecessary.
I can't say much at this level of abstraction. It feels a bit too
synchronous to me, to await a certain result from the prover, and then
produce further edits.
It might be easier to internalize this logic of trying something into the
prover commands that you are running.
The PIDE document model usually works in a "streaming" fashion: you throw
a lot of commands at the prover at the same time, without waiting for
anything, and later visualize results incrementally as they arrive.
Makarius
Last updated: Apr 24 2024 at 01:07 UTC