Add proof object search facilities to IdView

[David Aspinall <da+pgtrac@…>]

Add a proof object search facility to IdView, similar to the Open Type dialog in Java, so we can find names dynamically. A more advanced facility would be to search on object contents.

This may require using prover-side search, and/or interfacing with ProverKnowledge.

[David Aspinall <da+pgtrac@…>]

Regular expression name searching has now been added to IdView, and the ProverSyntax datastructures storing names have been overhauled. This works pretty well, although there are a few quirks to sort out:

• Statements can't be loaded until Isar has a theory context. Might be solved by using PGIP idshow instead (although that probably needs tuning).

• Keeping qualified names: these clutter the display a bit, so we could strip them on display but recover the full names for passing to Prover Knowledge for lookup. Needs an extra field containing fully qualified name shadow of items, or an index into allitems.

• Regexp search: this updates on every change which makes it a bit slow. Simplest to change to use another event (focus leaving? return pressed?). More sophisticated would be to set/reset a short timer after the change, and update only after the timer has expired.

• Possible race condition somewhere seems to sometimes prevent description text from being updated, with response "Could not load statement" when statement was in fact loaded (next view succeeds). Perhaps race is in Prover Knowledge.

[David Aspinall <da+pgtrac@…>]

Further remark on "Statement could not be loaded":

• Also seen (repeatedly) on theorem lookups that return multiple results/format that confuses ProverKnowledge, e.g. IntDef?.int_distrib. This produces a response but PK reports could not be loaded.

Although this may be an inconsistency in Isabelle's name reporting, perhaps: it uses synthesised names for individual theorems with sets of theorems (int_distrib_1, etc). We don't want to see these, I'm fixing this now.

[David Aspinall]

Most desirable next improvement for next version:

• Use glob search instead of regexp search on names.

Otherwise support is OK for now.

[David Aspinall]

Milestone PG-Eclipse-1.1.0 deleted