Opened 17 years ago

Last modified 11 years ago

#12 new defect

Polish Proof Objects View; Link to Prover Knowledge

Reported by: David Aspinall <da+pgtrac@…> Owned by: David Aspinall
Priority: minor Milestone:
Component: 1:pg-eclipse Keywords:
Cc:

Description

Proof Objects view needs some polish:

  1. Glitch when editing theory box and dynamic update: can we position cursor at end of text, or not clear the text?
  2. Could populate the theory list on startup without need to
  3. Drag-n-drop for paste action would be good. Or copy-on-select.
  4. Something to inform the user (dialog/tooltip) that ProverKnowledge? needs to be enabled and a theory open for lookups to work. Better: implement a knowledge item that doesn't require this, for qualified names.

Also would be good to link this more strongly with the Prover Knowledge, e.g. so we have Dynamic update for theories-in-progress (names, etc, are replicated by outline, but display of the theorems without navigating in source would be good).

Change History (4)

comment:1 Changed 17 years ago by David Aspinall <da+pgtrac@…>

Owner: changed from David Aspinall to anonymous

Another glitch:

  1. Moving cursor down list can queue a long list of updates. We should only have one queued update at a time, and not spawn many.

This crops up in several places in the code, e.g. updating output views and queuing multiple refresh events. Pattern-based solution would be nice.

Another improvement:

  • Display multiple items when there are multiple selections

comment:2 Changed 17 years ago by David Aspinall <da+pgtrac@…>

Owner: changed from anonymous to David Aspinall

comment:3 Changed 17 years ago by David Aspinall <da+pgtrac@…>

I've updated the view again and the management of keywords inside ProverSyntax.

The current status in Isabelle is that Isabelle will send <setids> for theory names and theorem names:

  • Theory objtype with no context gives the top-level theories
  • Theory objtype with a theory name context gives nested "fake subtheories"
  • Theorem objtype with no context gives all theorems, with fully qualified names
  • Theorem objtype with a theory name context gives results that have the theory name trimmed and exclude faked "subtheories", i.e. those with names foo.bar, which appear in the fake theory T.foo

Inside Eclipse, responses are treated as if they are always unqualified. This means that there is some duplication in storing keywords in ProverSyntax (and unnecessary querying), but it should give a consistent view for users.

The current code (IdView.java) assumes that an <askids> request gives a unique single response that corresponds directly. That isn't right; it should be fixed so that the ProverSyntax has a listener which responds to <setids> and friends, and can in turn inform the IdView which may update itself accordingly. I've made Isabelle match this code for the time being, which is what forces the qualified names above in the single large response (previously several responses with abbreviated names and a context attribute). Another possibility would be to send several tables in a single response, which the schema allows, but the current code in IdView does not.

The super-query of all identifiers takes a good few seconds to process and should be cached.

comment:4 Changed 11 years ago by David Aspinall

Milestone: PG-Eclipse-1.1.0

Milestone PG-Eclipse-1.1.0 deleted

Note: See TracTickets for help on using tickets.