Extending the Index Manager - Revision history

imported>Nicolas: /* Implementing an indexer */ added constraint: an element cannot be declared with an empty name

2009-05-29T13:17:15Z

Implementing an indexer: added constraint: an element cannot be declared with an empty name

← Older revision		Revision as of 13:17, 29 May 2009
Line 58:		Line 58:

	* an element cannot have an occurrence if it has not been declared before		* an element cannot have an occurrence if it has not been declared before
			* an element cannot be declared with an empty name
	* an element cannot be declared more than once		* an element cannot be declared more than once
	* declared elements must be local to the file		* declared elements must be local to the file
Line 64:		Line 65:

	The first constraint is implicitly held by the fact that occurrences are added by giving the declaration of the occurring element.		The first constraint is implicitly held by the fact that occurrences are added by giving the declaration of the occurring element.
	Breaking one of the ~~three~~ next ones will result in a {{class\|IllegalArgumentException}} being thrown.		Breaking one of the four next ones will result in a {{class\|IllegalArgumentException}} being thrown.
	Finally, when file indexing completes, declared elements with no occurrences are simply ignored (not put into index tables).		Finally, when file indexing completes, declared elements with no occurrences are simply ignored (not put into index tables).

imported>Nicolas at 16:40, 3 March 2009

2009-03-03T16:40:49Z

imported>Nicolas at 13:32, 3 March 2009

2009-03-03T13:32:10Z

← Older revision		Revision as of 13:32, 3 March 2009
Line 3:		Line 3:

	So, along with existing Event-B model indexers, it is possible to have indexers for other target types, or even indexers for Event-B models that record additional information.		So, along with existing Event-B model indexers, it is possible to have indexers for other target types, or even indexers for Event-B models that record additional information.

			The extension point for indexers is '''org.rodinp.core.indexers'''.

	Making your own indexer and integrating it to the indexing system can be achieved in the following way.		Making your own indexer and integrating it to the indexing system can be achieved in the following way.
Line 19:		Line 21:
	For instance, Event-B indexer plug-in declares kinds DECLARATION, REFERENCE and MODIFICATION, to qualify the various occurrences of variables, carrier sets, ..., in model files (of course, not all occurrence kinds can apply to all elements !).		For instance, Event-B indexer plug-in declares kinds DECLARATION, REFERENCE and MODIFICATION, to qualify the various occurrences of variables, carrier sets, ..., in model files (of course, not all occurrence kinds can apply to all elements !).

	Occurrence kind declaration is achieved through an extension point. ~~{{TODO\|name the extension point}}~~		Occurrence kind declaration is achieved through extension point '''org.rodinp.core.occurrenceKind'''.


Line 82:		Line 84:

	The main interest of that feature is to get declarations from previous indexers({{method\|IIndexingToolkit#getDeclarations()}}). It is then possible to add your own specific occurrences of the elements subject of these declarations ({{method\|IIndexingToolkit#addOccurrence()}} as usual).		The main interest of that feature is to get declarations from previous indexers({{method\|IIndexingToolkit#getDeclarations()}}). It is then possible to add your own specific occurrences of the elements subject of these declarations ({{method\|IIndexingToolkit#addOccurrence()}} as usual).

			==Existing Indexers==

			Indexers already exist for Event-B, they are described in [[Event-B Indexers]]. They can be a source of inspiration for other indexers, but also a base for new indexers depending on existing ones.

	[[Category:Developer documentation]]		[[Category:Developer documentation]]

imported>Mathieu: /* Implementing an indexer */

2008-12-22T12:29:47Z

Implementing an indexer

imported>Nicolas: /* Implementing an indexer */

2008-12-19T18:19:54Z

Implementing an indexer

← Older revision		Revision as of 18:19, 19 December 2008
Line 33:		Line 33:
	* {{method\|getId()}}		* {{method\|getId()}}
	* {{method\|getDependencies(IInternalElement)}}		* {{method\|getDependencies(IInternalElement)}}
	* {{method\|index(~~IIndexingToolkit~~)}}		* {{method\|index(IIndexingBridge)}}

	The first one merely gives the unique identifier of the indexer.		The first one merely gives the unique identifier of the indexer.
Line 47:		Line 47:


	Here comes the {{method\|index}} method and the {{class\|~~IIndexingToolkit~~}} object.		Here comes the {{method\|index}} method and the {{class\|IIndexingBridge}} object.
	This object has various functions. First, it gives the root element of the file to index. The file can be assumed to be of one of the types the indexer registered for.		This object has various functions. First, it gives the root element of the file to index. The file can be assumed to be of one of the types the indexer registered for.
	It also gives the declarations of imported elements (if any): these are the elements that were declared in files on which the current one depends, that may occur in it.		It also gives the declarations of imported elements (if any): these are the elements that were declared in files on which the current one depends, that may occur in it.
	If your indexer depends on others (see below), you can also get the result of their work.		If your indexer depends on others (see below), you can also get the result of their work.

	So the {{class\|~~IIndexingToolkit~~}} gives input data, but it also gets the output of your indexer.		So the {{class\|IIndexingBridge}} gives input data, but it also gets the output of your indexer.
	This is achieved through its {{method\|declare()}} and {{method\|addOccurrences()}} methods.		This is achieved through its {{method\|declare()}} and {{method\|addOccurrences()}} methods.

	The imports received come from previous exportations. If elements are to be visible to indexers of dependent files (including your indexer), they must be exported before returning.		The imports received come from previous exportations. If elements are to be visible to indexers of dependent files (including your indexer), they must be exported before returning.

			Please note the following indexing constraints:

	Indexing is run as a Job, so it can be canceled. Indexers are expected to check regularly for cancellation ({{method\|~~IIndexingToolkit~~#isCanceled()}}) and return as soon as possible when it is requested.		* an element cannot have an occurrence if it has not been declared before
			* an element cannot be declared more than once
			* declared elements must be local to the file
			* occurring elements must be either local or imported
			* declared elements should have one or more occurrences when indexing completes

			The first constraint is implicitly held by the fact that occurrences are added by giving the declaration of the occurring element.
			Breaking one of the three next ones will result in a {{class\|IllegalArgumentException}} being thrown.
			Finally, when file indexing completes, declared elements with no occurrences are simply ignored (not put into index tables).


			Indexing is run as a Job, so it can be canceled. Indexers are expected to check regularly for cancellation ({{method\|IIndexingBridge#isCanceled()}}) and return as soon as possible when it is requested.

	==Depending on other indexers==		==Depending on other indexers==

imported>Mathieu: {{TOCright}}

2008-12-11T22:09:51Z

← Older revision		Revision as of 22:09, 11 December 2008
Line 1:		Line 1:
			{{TOCright}}
	The indexing system, that stores the data and answers requests, is separated from the indexers, that actually do the job of scanning files and adding occurrences.		The indexing system, that stores the data and answers requests, is separated from the indexers, that actually do the job of scanning files and adding occurrences.

imported>Mathieu: /* Implementing an indexer */ typo

2008-12-11T22:09:23Z

Implementing an indexer: typo

← Older revision		Revision as of 22:09, 11 December 2008
Line 28:		Line 28:


	Indexers must implement the {{class\|IIndexer}}} interface.		Indexers must implement the {{class\|IIndexer}} interface.
	This interface consists in 3 methods		This interface consists in 3 methods
	* {{method\|getId()}}		* {{method\|getId()}}
Line 58:		Line 58:

	Indexing is run as a Job, so it can be canceled. Indexers are expected to check regularly for cancellation ({{method\|IIndexingToolkit#isCanceled()}}) and return as soon as possible when it is requested.		Indexing is run as a Job, so it can be canceled. Indexers are expected to check regularly for cancellation ({{method\|IIndexingToolkit#isCanceled()}}) and return as soon as possible when it is requested.



	==Depending on other indexers==		==Depending on other indexers==

imported>Mathieu: use of some commn typestting templates for class and methods

2008-12-11T22:09:04Z

use of some commn typestting templates for class and methods

← Older revision		Revision as of 22:09, 11 December 2008
Line 10:		Line 10:
	We are speaking here of making a single indexer, but you may as well develop several indexers, each one specialized in one or more file types.		We are speaking here of making a single indexer, but you may as well develop several indexers, each one specialized in one or more file types.

	Later, to make the indexing system aware of your indexer, you will have to register it (''RodinIndexer#register()''), specifying the file types you are interested in. Then, each time a file of one of these types gets modified, the indexing system will call the indexer on this file.		Later, to make the indexing system aware of your indexer, you will have to register it ({{method\|RodinIndexer#register()}}), specifying the file types you are interested in. Then, each time a file of one of these types gets modified, the indexing system will call the indexer on this file.

	==Declaring custom occurrence kinds==		==Declaring custom occurrence kinds==
Line 28:		Line 28:


	Indexers must implement the ~~'''~~IIndexer~~'''~~ interface.		Indexers must implement the {{class\|IIndexer}}} interface.
	This interface consists in 3 methods		This interface consists in 3 methods
	* ''getId()''		* {{method\|getId()}}
	* ''getDependencies(IInternalElement)''		* {{method\|getDependencies(IInternalElement)}}
	* ''index(IIndexingToolkit)''		* {{method\|index(IIndexingToolkit)}}

	The first one merely gives the unique identifier of the indexer.		The first one merely gives the unique identifier of the indexer.
Line 43:		Line 43:
	As the indexing system has no sense of how to understand file contents, stating file dependencies is delegated to indexers (however, if it is already done by indexers that run before yours, there is no need to do it twice, simply return an empty array; see next section).		As the indexing system has no sense of how to understand file contents, stating file dependencies is delegated to indexers (however, if it is already done by indexers that run before yours, there is no need to do it twice, simply return an empty array; see next section).

	The indexing system gathers file dependencies and computes the order in which they must be indexed. If cycles are detected, they are arbitrarily broken. If no dependencies are specified, all files are indexed in no special order. Once the order is decided, the indexing system actually calls ''IIndexer#index()''.		The indexing system gathers file dependencies and computes the order in which they must be indexed. If cycles are detected, they are arbitrarily broken. If no dependencies are specified, all files are indexed in no special order. Once the order is decided, the indexing system actually calls {{method\|IIndexer#index()}}.


	Here comes the 'index' method and the ~~'''~~IIndexingToolkit~~'''~~ object.		Here comes the {{method\|index}} method and the {{class\|IIndexingToolkit}} object.
	This object has various functions. First, it gives the root element of the file to index. The file can be assumed to be of one of the types the indexer registered for.		This object has various functions. First, it gives the root element of the file to index. The file can be assumed to be of one of the types the indexer registered for.
	It also gives the declarations of imported elements (if any): these are the elements that were declared in files on which the current one depends, that may occur in it.		It also gives the declarations of imported elements (if any): these are the elements that were declared in files on which the current one depends, that may occur in it.
	If your indexer depends on others (see below), you can also get the result of their work.		If your indexer depends on others (see below), you can also get the result of their work.

	So the ~~'''~~IIndexingToolkit~~'''~~ gives input data, but it also gets the output of your indexer.		So the {{class\|IIndexingToolkit}} gives input data, but it also gets the output of your indexer.
	This is achieved through its ''declare()'' and ''addOccurrences()'' methods.		This is achieved through its {{method\|declare()}} and {{method\|addOccurrences()}} methods.

	The imports received come from previous exportations. If elements are to be visible to indexers of dependent files (including your indexer), they must be exported before returning.		The imports received come from previous exportations. If elements are to be visible to indexers of dependent files (including your indexer), they must be exported before returning.


	Indexing is run as a Job, so it can be canceled. Indexers are expected to check regularly for cancellation (''IIndexingToolkit#isCanceled()'') and return as soon as possible when it is requested.		Indexing is run as a Job, so it can be canceled. Indexers are expected to check regularly for cancellation ({{method\|IIndexingToolkit#isCanceled()}}) and return as soon as possible when it is requested.


Line 73:		Line 73:


	The main interest of that feature is to get declarations from previous indexers(''IIndexingToolkit#getDeclarations()''). It is then possible to add your own specific occurrences of the elements subject of these declarations (''IIndexingToolkit#addOccurrence()'' as usual).		The main interest of that feature is to get declarations from previous indexers({{method\|IIndexingToolkit#getDeclarations()}}). It is then possible to add your own specific occurrences of the elements subject of these declarations ({{method\|IIndexingToolkit#addOccurrence()}} as usual).

	[[Category:Developer documentation]]		[[Category:Developer documentation]]

imported>Mathieu: Category:Developer documentation

2008-12-11T22:01:31Z

Category:Developer documentation

← Older revision		Revision as of 22:01, 11 December 2008
Line 74:		Line 74:

	The main interest of that feature is to get declarations from previous indexers(''IIndexingToolkit#getDeclarations()''). It is then possible to add your own specific occurrences of the elements subject of these declarations (''IIndexingToolkit#addOccurrence()'' as usual).		The main interest of that feature is to get declarations from previous indexers(''IIndexingToolkit#getDeclarations()''). It is then possible to add your own specific occurrences of the elements subject of these declarations (''IIndexingToolkit#addOccurrence()'' as usual).

			[[Category:Developer documentation]]

imported>Nicolas: New page: The indexing system, that stores the data and answers requests, is separated from the indexers, that actually do the job of scanning files and adding occurrences. So, along with existing...

2008-12-05T10:48:59Z

New page: The indexing system, that stores the data and answers requests, is separated from the indexers, that actually do the job of scanning files and adding occurrences. So, along with existing...

New page

The indexing system, that stores the data and answers requests, is separated from the indexers, that actually do the job of scanning files and adding occurrences.

So, along with existing Event-B model indexers, it is possible to have indexers for other target types, or even indexers for Event-B models that record additional information.

Making your own indexer and integrating it to the indexing system can be achieved in the following way.

==Defining target file types==

The first task is to define which file types your indexer will be able to index.
We are speaking here of making a single indexer, but you may as well develop several indexers, each one specialized in one or more file types.

Later, to make the indexing system aware of your indexer, you will have to register it (''RodinIndexer#register()''), specifying the file types you are interested in. Then, each time a file of one of these types gets modified, the indexing system will call the indexer on this file.

==Declaring custom occurrence kinds==

Depending on the type of information your indexer will have to retrieve, you may need to define your own occurrence kinds.

For instance, Event-B indexer plug-in declares kinds DECLARATION, REFERENCE and MODIFICATION, to qualify the various occurrences of variables, carrier sets, ..., in model files (of course, not all occurrence kinds can apply to all elements !).

Occurrence kind declaration is achieved through an extension point. {{TODO|name the extension point}}

==Implementing an indexer==

Now, getting further towards the code, what is an indexer required to do ?

An indexer's fundamental task consists in scanning a file, declaring elements, and adding occurrences.

Indexers must implement the '''IIndexer''' interface.
This interface consists in 3 methods
* ''getId()''
* ''getDependencies(IInternalElement)''
* ''index(IIndexingToolkit)''

The first one merely gives the unique identifier of the indexer.
The other two will do a more complex job.

Dependencies occur between files when there can be occurrences of an element outside the file of its declaration.
For example, in Event-B, a carrier set can be declared in a context and referenced in a machine that sees it.
In this case, it is necessary to index the declaring one before the referencing one, because an element can ever have an occurrence stored only if it has been declared before.
As the indexing system has no sense of how to understand file contents, stating file dependencies is delegated to indexers (however, if it is already done by indexers that run before yours, there is no need to do it twice, simply return an empty array; see next section).

The indexing system gathers file dependencies and computes the order in which they must be indexed. If cycles are detected, they are arbitrarily broken. If no dependencies are specified, all files are indexed in no special order. Once the order is decided, the indexing system actually calls ''IIndexer#index()''.

Here comes the 'index' method and the '''IIndexingToolkit''' object.
This object has various functions. First, it gives the root element of the file to index. The file can be assumed to be of one of the types the indexer registered for.
It also gives the declarations of imported elements (if any): these are the elements that were declared in files on which the current one depends, that may occur in it.
If your indexer depends on others (see below), you can also get the result of their work.

So the '''IIndexingToolkit''' gives input data, but it also gets the output of your indexer.
This is achieved through its ''declare()'' and ''addOccurrences()'' methods.

The imports received come from previous exportations. If elements are to be visible to indexers of dependent files (including your indexer), they must be exported before returning.

Indexing is run as a Job, so it can be canceled. Indexers are expected to check regularly for cancellation (''IIndexingToolkit#isCanceled()'') and return as soon as possible when it is requested.

==Depending on other indexers==

The architecture has been thought in order to allow several indexers to work sequentially on the same file, letting the last ones benefit from the results of the first ones.
To do this, simply indicate in the indexer extension point after which indexers yours should be run.
It will then be called to get file dependencies and index file elements.

If file dependencies are well specified by indexers yours depends on, there is no need to specify them again, you can just return an empty result in the corresponding method.

However, it is possible to add other dependencies. All dependencies will be taken into account together to compute the order in which files will be indexed.

The main interest of that feature is to get declarations from previous indexers(''IIndexingToolkit#getDeclarations()''). It is then possible to add your own specific occurrences of the elements subject of these declarations (''IIndexingToolkit#addOccurrence()'' as usual).

← Older revision		Revision as of 16:40, 3 March 2009
Line 1:		Line 1:
	{{TOCright}}		{{TOCright}}
	The indexing system, that stores the data and answers ~~requests~~, is separated from the indexers, that actually do the job of scanning files and adding occurrences.		The indexing system, that stores the data and answers queries, is separated from the indexers, that actually do the job of scanning files and adding occurrences.

	So, along with existing Event-B model indexers, it is possible to have indexers for other target types, or even indexers for Event-B models that record additional information.		So, along with existing Event-B model indexers, it is possible to have indexers for other target types, or even indexers for Event-B models that record additional information.

	~~The extension point for indexers is '''org.rodinp.core.indexers'''.~~

	Making your own indexer and integrating it to the indexing system can be achieved in the following way.		Making your own indexer and integrating it to the indexing system can be achieved in the following way.
Line 13:		Line 11:
	We are speaking here of making a single indexer, but you may as well develop several indexers, each one specialized in one or more file types.		We are speaking here of making a single indexer, but you may as well develop several indexers, each one specialized in one or more file types.

	Later, to make the indexing system aware of your indexer, you will have to register it ~~({{method\|RodinIndexer#register()}})~~, specifying the file types you are interested in. Then, each time a file of one of these types gets modified, the indexing system will call the indexer on this file.		Later, to make the indexing system aware of your indexer, you will have to register it through the '''org.rodinp.core.indexers''' extension point, specifying the file types you are interested in. Then, each time a file of one of these types gets modified, the indexing system will call the indexer on this file.

	==Declaring custom occurrence kinds==		==Declaring custom occurrence kinds==
Line 21:		Line 19:
	For instance, Event-B indexer plug-in declares kinds DECLARATION, REFERENCE and MODIFICATION, to qualify the various occurrences of variables, carrier sets, ..., in model files (of course, not all occurrence kinds can apply to all elements !).		For instance, Event-B indexer plug-in declares kinds DECLARATION, REFERENCE and MODIFICATION, to qualify the various occurrences of variables, carrier sets, ..., in model files (of course, not all occurrence kinds can apply to all elements !).

	Occurrence kind ~~declaration~~ is achieved through extension point '''org.rodinp.core.occurrenceKind'''.		Occurrence kind registration is achieved through extension point '''org.rodinp.core.occurrenceKind'''.


Line 47:		Line 45:


	Here comes the {{method\|index}} method and the {{class\|IIndexingBridge}} object.		Here comes the {{method\|index()}} method and the {{class\|IIndexingBridge}} object.
	This object has various functions. ~~First~~, it gives the root element of the file to index. The file can be assumed to be of one of the types the indexer registered for.		This object has various functions. Firstly, it gives the root element of the file to index. The file can be assumed to be of one of the types the indexer registered for.
	It also gives the declarations of imported elements (if any): these are the elements that were declared in files on which the current one depends, that may occur in it.		It also gives the declarations of imported elements (if any): these are the elements that were declared in files on which the current one depends, that may occur in it.
	If your indexer depends on others (see below), you can also get the result of their work.		If your indexer depends on others (see below), you can also get the result of their work.

← Older revision		Revision as of 12:29, 22 December 2008
Line 27:		Line 27:

	An indexer's fundamental task consists in scanning a file, declaring elements, and adding occurrences.		An indexer's fundamental task consists in scanning a file, declaring elements, and adding occurrences.


	Indexers must implement the {{class\|IIndexer}} interface.		Indexers must implement the {{class\|IIndexer}} interface.
Line 37:		Line 36:
	The first one merely gives the unique identifier of the indexer.		The first one merely gives the unique identifier of the indexer.
	The other two will do a more complex job.		The other two will do a more complex job.


	Dependencies occur between files when there can be occurrences of an element outside the file of its declaration.		Dependencies occur between files when there can be occurrences of an element outside the file of its declaration.
Line 59:		Line 57:
	Please note the following indexing constraints:		Please note the following indexing constraints:

	* an element cannot have an occurrence if it has not been declared before		* an element cannot have an occurrence if it has not been declared before
	* an element cannot be declared more than once		* an element cannot be declared more than once
	* declared elements must be local to the file		* declared elements must be local to the file
	* occurring elements must be either local or imported		* occurring elements must be either local or imported
	* declared elements should have one or more occurrences when indexing completes		* declared elements should have one or more occurrences when indexing completes

	The first constraint is implicitly held by the fact that occurrences are added by giving the declaration of the occurring element.		The first constraint is implicitly held by the fact that occurrences are added by giving the declaration of the occurring element.
	Breaking one of the three next ones will result in a {{class\|IllegalArgumentException}} being thrown.		Breaking one of the three next ones will result in a {{class\|IllegalArgumentException}} being thrown.
	Finally, when file indexing completes, declared elements with no occurrences are simply ignored (not put into index tables).		Finally, when file indexing completes, declared elements with no occurrences are simply ignored (not put into index tables).


	Indexing is run as a Job, so it can be canceled. Indexers are expected to check regularly for cancellation ({{method\|IIndexingBridge#isCanceled()}}) and return as soon as possible when it is requested.		Indexing is run as a Job, so it can be canceled. Indexers are expected to check regularly for cancellation ({{method\|IIndexingBridge#isCanceled()}}) and return as soon as possible when it is requested.