Difference between revisions of "Index Query"
imported>Mathieu m (Category:Developer documentation is parent category of Design) |
imported>Nicolas |
||
| Line 5: | Line 5: | ||
==Performing requests== | ==Performing requests== | ||
| − | The indexer contents is not directly accessible to other plug-ins. | + | The indexer contents is not directly accessible to other plug-ins. Queries are sent through a {{class|IIndexQuery}} object provided by the RodinCore plug-in. |
===What to request ?=== | ===What to request ?=== | ||
| − | + | Two types of information can be queried : | |
| − | * | + | * declarations ({{class|IDeclaration}}) |
| − | * | + | * occurrences ({{class|IOccurrence}}) |
| − | + | A declaration is the unique identifier of an entity in the index repository. | |
| − | + | It consists in a handle of the element itself plus its user-defined name. | |
| + | An occurrence always refers to one single declaration. | ||
| + | Several query types can be performed, depending on the starting point : | ||
| + | * getting the declaration of a given element (as {{class|IInternalElement}}) | ||
| + | * getting the declarations of elements that match a given user-defined name (as {{class|String}}) in a given file | ||
| + | * getting the declarations of elements that occur, or could occur, in a given file | ||
| + | * getting occurrences of a given declaration (this declaration has been retrieved from a previous query) | ||
| + | * getting occurrences of a given declaration using propagation ([[#Propagation]]) | ||
| − | + | Thus, a declaration is the key to retrieve occurrences. | |
| + | |||
| + | As the result might be too coarse, queries can be filtered out using various criterias (see {{class|IIndexQuery}} interface for more details). | ||
===Occurrences=== | ===Occurrences=== | ||
| Line 29: | Line 38: | ||
Occurrence kinds are contributed by indexers, no kinds are defined at the indexing system level. | Occurrence kinds are contributed by indexers, no kinds are defined at the indexing system level. | ||
| + | See more in [[Event-B Indexers]]. | ||
| + | |||
| + | ===Propagation=== | ||
| + | |||
| + | Propagation is a way to get occurrences of several declarations, starting from one single declaration. In particular, it addresses cases where various declarations represent the same entity. The problem is that each declaration has separate occurrences. The propagation mechanism allows to get all occurrences of the entity, whatever the underlying declaration. | ||
| + | |||
| + | For example, in Event-B, a variable can be redeclared in a refining machine. In the index repository, each variable has a separate declaration and separate occurrences. However, it might be interesting in some cases to consider occurrences of the concrete variable as a subset of occurrences of the abstract one. The concept here is to 'propagate' the query about the abstract variable to occurrences of the concrete one. This is achievable in this case thanks to event-b propagators. | ||
| + | |||
| + | See more in [[Event-B Indexers]]. | ||
| + | |||
===Getting a valid result=== | ===Getting a valid result=== | ||
| Line 34: | Line 53: | ||
The indexing system data is constantly evolving, as long as files get modified. Furthermore, as indexing is performed as a background operation, one cannot guess whether the indexing has completed or not. The system may also be updating its data, making it temporarily incoherent. Thus, the problem arises to ensure that the data is valid and up-to-date. | The indexing system data is constantly evolving, as long as files get modified. Furthermore, as indexing is performed as a background operation, one cannot guess whether the indexing has completed or not. The system may also be updating its data, making it temporarily incoherent. Thus, the problem arises to ensure that the data is valid and up-to-date. | ||
| − | To that end, a method is provided by the {{class| | + | To that end, a method is provided by the {{class|IIndexQuery}}, that blocks the current thread until all planned files are indexed. Requests performed after that will thus return a valid result and benefit from the most up-to-date version of the data. |
[[Category:Design]] | [[Category:Design]] | ||
Revision as of 10:29, 2 March 2009
Contents
Purpose
The purpose of the Rodin index manager is to store in a uniform way the entities that are declared in the database together with their occurrences. This central repository of declarations and occurrences will allow for fast implementations of various refactoring mechanisms (such as renaming) and support for searching models or browsing them.
Performing requests
The indexer contents is not directly accessible to other plug-ins. Queries are sent through a IIndexQuery object provided by the RodinCore plug-in.
What to request ?
Two types of information can be queried :
- declarations (IDeclaration)
- occurrences (IOccurrence)
A declaration is the unique identifier of an entity in the index repository. It consists in a handle of the element itself plus its user-defined name. An occurrence always refers to one single declaration.
Several query types can be performed, depending on the starting point :
- getting the declaration of a given element (as IInternalElement)
- getting the declarations of elements that match a given user-defined name (as String) in a given file
- getting the declarations of elements that occur, or could occur, in a given file
- getting occurrences of a given declaration (this declaration has been retrieved from a previous query)
- getting occurrences of a given declaration using propagation (#Propagation)
Thus, a declaration is the key to retrieve occurrences.
As the result might be too coarse, queries can be filtered out using various criterias (see IIndexQuery interface for more details).
Occurrences
An occurrence (IOccurrence) describes a location (IRodinLocation) and a kind of occurrence (IOccurrenceKind) of an element (referred to through its IDeclaration). For example, in Event-B, an occurrence could be:
- location
- in IAxiom 'a' (handle), in the PREDICATE_ATTRIBUTE, between characters 7 and 12
- kind
- REFERENCE
- declaration
- the ICarrierSet 's' (handle), named "set1"
Occurrence kinds are contributed by indexers, no kinds are defined at the indexing system level. See more in Event-B Indexers.
Propagation
Propagation is a way to get occurrences of several declarations, starting from one single declaration. In particular, it addresses cases where various declarations represent the same entity. The problem is that each declaration has separate occurrences. The propagation mechanism allows to get all occurrences of the entity, whatever the underlying declaration.
For example, in Event-B, a variable can be redeclared in a refining machine. In the index repository, each variable has a separate declaration and separate occurrences. However, it might be interesting in some cases to consider occurrences of the concrete variable as a subset of occurrences of the abstract one. The concept here is to 'propagate' the query about the abstract variable to occurrences of the concrete one. This is achievable in this case thanks to event-b propagators.
See more in Event-B Indexers.
Getting a valid result
The indexing system data is constantly evolving, as long as files get modified. Furthermore, as indexing is performed as a background operation, one cannot guess whether the indexing has completed or not. The system may also be updating its data, making it temporarily incoherent. Thus, the problem arises to ensure that the data is valid and up-to-date.
To that end, a method is provided by the IIndexQuery, that blocks the current thread until all planned files are indexed. Requests performed after that will thus return a valid result and benefit from the most up-to-date version of the data.
