Index Query: Difference between revisions
imported>Nicolas m Index Requester moved to Index Query: Better name. Follows code renaming. |
imported>Mathieu m Category:Design + some common typesetting templates |
||
| Line 5: | Line 5: | ||
==Performing requests== | ==Performing requests== | ||
The indexer contents is not directly accessible to other plug-ins. Requests are sent through a | The indexer contents is not directly accessible to other plug-ins. Requests are sent through a {{class|IIndexRequester}} object provided by the indexer plug-in. | ||
===What to request ?=== | ===What to request ?=== | ||
Mainly, two starting points are considered: | Mainly, two starting points are considered: | ||
* either you start from an element (as | * either you start from an element (as {{class|IInternalElement}}) | ||
* or you have a user-defined name (as | * or you have a user-defined name (as {{class|String}}), possibly parsed from a file or as a user input | ||
In both cases, the requester will return declarations ( | In both cases, the requester will return declarations ({{class|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. | 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. | ||
| Line 21: | Line 21: | ||
===Occurrences=== | ===Occurrences=== | ||
An occurrence ( | An occurrence ({{class|IOccurrence}}) describes a location ({{class|IRodinLocation}}) and a kind of occurrence ({{class|IOccurrenceKind}}) of an element (referred to through its {{class|IDeclaration}}). | ||
For example, in Event-B, an occurrence could be: | For example, in Event-B, an occurrence could be: | ||
| Line 34: | Line 34: | ||
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 | To that end, a method is provided by the {{class|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. | ||
[[Category:Design]] | |||
Revision as of 22:30, 11 December 2008
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.
