Re: [isabelle] Updating to a previous Document.Version using Isabelle/Scala



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






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.