Re: [isabelle] Isabelle2016-1-RC1 processing theories twice

On 08/11/16 08:13, Mathias Fleury wrote:
>> On 1 Nov 2016, at 22:32, Makarius <makarius at
>> <mailto:makarius at>> wrote:
>> If it is reliably reproducible for you, you can also make a bisection on
>> the repository to see where the problem is located in the history.
> I've finally done it and the issue is much older than had I expected: it
> goes back to
> commit and more
> precisely to the following part of the change:
> - if (change.deps_changed && PIDE.options.bool("jedit_auto_load"))
> PIDE.deps_changed() + if (PIDE.options.bool("jedit_auto_load") &&
> change.deps_changed || + PIDE.options.bool("jedit_auto_resolve") &&
> change.version.nodes.undefined_blobs.nonEmpty) + PIDE.deps_changed()
> jedit_auto_resolve is activated (both in this version by default and in
> my setup). If there are non-processed blobs (i.e. a lot of SML files
> here) and I click in the List buffer, the processing restarts. I have no
> idea why the reprocessing happens only once (i.e. there are no
> undefined_blobs anymoreâ).

Thanks for doing the bisection.

The change above is from August 2015. There are more changes where
jedit_auto_resolve fluctuates back and forth, without clear conclusion:
see occurrences of "auto" in

It is a genuine "feature": something added on the spot, without being
properly thought out. I had it on my list over some months in 2015, but
did not revisit it.

I will make one round of looking carefully how it behaves at the moment,
and then see if it is put into proper shape for the release, or removed

There is a bigger plan in the pipeline, to reform the management of all
source files for a PIDE session. When that happens, both jedit_auto_load
and jedit_auto_resolve become obsolete.


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