[isabelle-dev] performance problems

[Makarius]

On 07/09/18 17:51, Manuel Eberl wrote:
> 
> Basically, what happens is that occasionally, the IDE "freezes" in the
> sense that no new changes to the document are processed. I can still
> view the output of all the processed commands, but there is a certain
> position in the document underneath which all the text is red, and it
> never because not red. If I change anything in the text before that, it
> also becomes red forever.
> 
> It seems to me that this is particularly triggered by non-terminating
> invocations of simp/auto/etc., even if I abort them after a fraction of
> a second.

On 07/09/18 19:19, Fabian Immler wrote:
> I experienced the same issues: Importing Pure (e50312982ba0) the
> following "freezes" the IDE in the sense Manuel described.
>
> lemma "PROP P"
>   apply (rule ?)+

Thanks for reporting the problem and pinning it down precisely. See now:

changeset:   68930:fc5763d000e8
user:        wenzelm
date:        Fri Sep 07 19:49:26 2018 +0200
files:       src/Pure/PIDE/command.ML
description:
proper tast_context (amending 5f44ad150ed8);


	Makarius