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 sketis.net
>> <mailto:makarius at sketis.net>> 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 https://isabelle.in.tum.de/repos/isabelle/rev/60916 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
https://isabelle.in.tum.de/repos/isabelle/log/857acb970dfa/src/Tools/jEdit/etc/options

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
outright.


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.


	Makarius





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