Re: [isabelle] the Query panel



On Tue, 20 Jan 2015, Buday Gergely wrote:

I tried to find the theorem whose name is left_neutral so opened the Query dialog and wrote

   name: "left_neutral"

Now the star-shaped widget beside the Apply button runs infinitely showing that the system works.

This "spinning disk" icon can actually have various different states. The tooltip tells more, e.g. it could be "Waiting for evaluation of context ...". Sometimes there is just a user confusion about that.

Nonetheless, there could be a genuine problem, e.g. a deadlock. If such a problem is recurrent, it usually helps to look very closely what really happens, and tell me about it. People have also made informative screencasts, leading to successful improvements of the situation eventually.


Is the above query wrong?

The query is OK. If it were somehow malformed, there should be an explicit error.


And, how could I stop this thread and start a new query?

It is unrealistic to manage threads manually -- the system mainly works with future tasks anyway. The Monitor panel might provide some clues what the system is up to, but it is also hard to interpret the situation.


	Makarius





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