Index Query
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. Requests are sent through a IIndexRequester object provided by the indexer plug-in.
What to request ?
Mainly, two starting points are considered:
- either you start from an element (as IInternalElement)
- or you have a user-defined name (as String), possibly parsed from a file or as a user input
In both cases, the requester will return declarations (IDeclaration), which consist in the element itself plus its user-defined name. The main difference is that a given user-defined name may be associated with several declarations (homonyms), whereas a given element has a unique declaration.
Declaration is the input argument to other requests, such as occurrence retrieval.
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.
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 IIndexRequester, 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.
