How to read Rodin projects and elements programmatically - Revision history

imported>Jrloria at 14:12, 30 May 2009

2009-05-30T14:12:55Z

← Older revision		Revision as of 14:12, 30 May 2009
Line 1:		Line 1:
			check also [[Database]]

	==How to read a Rodin Project==		==How to read a Rodin Project==
	You can access an existing Rodin project using <code>RodinCore.getRodinDB().getRodinProject("your_project_name")</code>. This returns a handle to an {{class\|IRodinProject}}. This project may or may not exist. Call {{ident\|exists}} on the resulting project to be sure.		You can access an existing Rodin project using <code>RodinCore.getRodinDB().getRodinProject("your_project_name")</code>. This returns a handle to an {{class\|IRodinProject}}. This project may or may not exist. Call {{ident\|exists}} on the resulting project to be sure.

imported>Mathieu: Use some typesetting templates

2008-10-28T14:54:29Z

Use some typesetting templates

← Older revision		Revision as of 14:54, 28 October 2008
Line 1:		Line 1:
	==How to read a Rodin Project==		==How to read a Rodin Project==
	You can access an existing Rodin project using <code>RodinCore.getRodinDB().getRodinProject("your_project_name")</code>. This returns a handle to an ~~<code>~~IRodinProject~~</code>~~. This project may or may not exist. Call ~~<code>~~exists~~</code>~~ on the resulting project to be sure.		You can access an existing Rodin project using <code>RodinCore.getRodinDB().getRodinProject("your_project_name")</code>. This returns a handle to an {{class\|IRodinProject}}. This project may or may not exist. Call {{ident\|exists}} on the resulting project to be sure.

	An other option is calling <code>RodinCore.getRodinDB().getRodinProjects</code>, which returns an array with of all existing ~~<code>~~IRodinProject~~</code>~~s.		An other option is calling <code>RodinCore.getRodinDB().getRodinProjects</code>, which returns an array with of all existing {{class\|IRodinProject}}s.

	==How to read a Machine or a Context==		==How to read a Machine or a Context==
	Machines and Contexts are accessed through ~~<code>~~IMachineRoot~~</code>~~ and ~~<code>~~IContextRoot~~</code>~~ respectively. Those roots are stored in ~~<code>~~IRodinFile~~</code>~~s.		Machines and Contexts are accessed through {{class\|IMachineRoot}} and {{class\|IContextRoot}} respectively. Those roots are stored in {{class\|IRodinFile}}s.

	The following method returns all existing ~~<code>~~IMachineRoot~~</code>~~s of a project:		The following method returns all existing {{class\|IMachineRoot}}s of a project:

	<code>		<code>
Line 24:		Line 24:
	</code>		</code>

	And this method returns all existing ~~<code>~~IContextRoot~~</code>~~s of a project:		And this method returns all existing {{class\|IContextRoot}}s of a project:

	<code>		<code>
Line 42:		Line 42:

	==How to read Invariants, Events, Theorems etc.==		==How to read Invariants, Events, Theorems etc.==
	Once you have obtained an ~~<code>~~IMachineRoot~~</code>~~ or an ~~<code>~~IContextRoot~~</code>~~ it is very easy to access its child elements. There exist functions such as <code>getInvariants()</code> to obtain an array of all existing ~~<code>~~IInvariants~~</code>~~. If you just want a specific element call a function of the form <code>getInvariant("your_invariant_name")</code>. Again this only returns a handle and does not guarantee that the element exists.		Once you have obtained an {{class\|IMachineRoot}} or an {{class\|IContextRoot}} it is very easy to access its child elements. There exist functions such as <code>getInvariants()</code> to obtain an array of all existing {{class\|IInvariants}}. If you just want a specific element call a function of the form <code>getInvariant("your_invariant_name")</code>. Again this only returns a handle and does not guarantee that the element exists.

	==How to read Proof Obligations==		==How to read Proof Obligations==

imported>Maria at 14:26, 28 October 2008

2008-10-28T14:26:45Z

← Older revision		Revision as of 14:26, 28 October 2008
Line 44:		Line 44:
	Once you have obtained an <code>IMachineRoot</code> or an <code>IContextRoot</code> it is very easy to access its child elements. There exist functions such as <code>getInvariants()</code> to obtain an array of all existing <code>IInvariants</code>. If you just want a specific element call a function of the form <code>getInvariant("your_invariant_name")</code>. Again this only returns a handle and does not guarantee that the element exists.		Once you have obtained an <code>IMachineRoot</code> or an <code>IContextRoot</code> it is very easy to access its child elements. There exist functions such as <code>getInvariants()</code> to obtain an array of all existing <code>IInvariants</code>. If you just want a specific element call a function of the form <code>getInvariant("your_invariant_name")</code>. Again this only returns a handle and does not guarantee that the element exists.

			==How to read Proof Obligations==
			For information on reading proof obligations, have a look at [[Accessing Proof Obligations]].

	[[Category:Developer documentation]]		[[Category:Developer documentation]]
	[[Category:Rodin Platform]]		[[Category:Rodin Platform]]

imported>Maria: /* How to read Invariants, Events, Theorems etc. */

2008-10-28T14:22:32Z

How to read Invariants, Events, Theorems etc.

← Older revision		Revision as of 14:22, 28 October 2008
Line 42:		Line 42:

	==How to read Invariants, Events, Theorems etc.==		==How to read Invariants, Events, Theorems etc.==
	Once you have obtained an <code>IMachineRoot</code> or an <code>IContextRoot</code> it is very easy to access its child elements. There exist functions such as <code>getInvariants()</code> to obtain an array of all existing <code>IInvariants</code>. If you just want a specific element ~~you~~ a function of the form <code>getInvariant("your_invariant_name")</code>. Again this only returns a handle and does not guarantee that the element exists.		Once you have obtained an <code>IMachineRoot</code> or an <code>IContextRoot</code> it is very easy to access its child elements. There exist functions such as <code>getInvariants()</code> to obtain an array of all existing <code>IInvariants</code>. If you just want a specific element call a function of the form <code>getInvariant("your_invariant_name")</code>. Again this only returns a handle and does not guarantee that the element exists.


	[[Category:Developer documentation]]		[[Category:Developer documentation]]
	[[Category:Rodin Platform]]		[[Category:Rodin Platform]]

imported>Maria at 14:20, 28 October 2008

2008-10-28T14:20:25Z

← Older revision		Revision as of 14:20, 28 October 2008
Line 40:		Line 40:
	}		}
	</code>		</code>

			==How to read Invariants, Events, Theorems etc.==
			Once you have obtained an <code>IMachineRoot</code> or an <code>IContextRoot</code> it is very easy to access its child elements. There exist functions such as <code>getInvariants()</code> to obtain an array of all existing <code>IInvariants</code>. If you just want a specific element you a function of the form <code>getInvariant("your_invariant_name")</code>. Again this only returns a handle and does not guarantee that the element exists.


	[[Category:Developer documentation]]		[[Category:Developer documentation]]
	[[Category:Rodin Platform]]		[[Category:Rodin Platform]]

imported>Maria: /* How to read a Machine or a Context */

2008-10-28T14:09:54Z

How to read a Machine or a Context

@@ Line 23: / Line 23: @@
+       }
 </code>
 [[Category:Developer documentation]]
 [[Category:Rodin Platform]]

imported>Maria: /* How to read a Machine or a Context */

2008-10-28T14:04:31Z

How to read a Machine or a Context

@@ Line 9: / Line 9: @@
 The following method returns all existing <code>IMachineRoot</code>s of a project:
 [[Category:Developer documentation]]
 [[Category:Rodin Platform]]

imported>Maria at 13:58, 28 October 2008

2008-10-28T13:58:19Z

← Older revision		Revision as of 13:58, 28 October 2008
Line 8:		Line 8:

	The following method returns all existing <code>IMachineRoot</code>s of a project:		The following method returns all existing <code>IMachineRoot</code>s of a project:


	[[Category:Developer documentation]]		[[Category:Developer documentation]]
	[[Category:Rodin Platform]]		[[Category:Rodin Platform]]

imported>Maria at 13:57, 28 October 2008

2008-10-28T13:57:36Z

← Older revision		Revision as of 13:57, 28 October 2008
Line 8:		Line 8:

	The following method returns all existing <code>IMachineRoot</code>s of a project:		The following method returns all existing <code>IMachineRoot</code>s of a project:

			[[Category:Developer documentation]]
			[[Category:Rodin Platform]]

imported>Maria at 13:53, 28 October 2008

2008-10-28T13:53:00Z

← Older revision		Revision as of 13:53, 28 October 2008
Line 2:		Line 2:
	You can access an existing Rodin project using <code>RodinCore.getRodinDB().getRodinProject("your_project_name")</code>. This returns a handle to an <code>IRodinProject</code>. This project may or may not exist. Call <code>exists</code> on the resulting project to be sure.		You can access an existing Rodin project using <code>RodinCore.getRodinDB().getRodinProject("your_project_name")</code>. This returns a handle to an <code>IRodinProject</code>. This project may or may not exist. Call <code>exists</code> on the resulting project to be sure.

	An other option is ~~to call~~ <code>RodinCore.getRodinDB().getRodinProjects</code>, which returns an array with of all existing <code>IRodinProject</code>s.		An other option is calling <code>RodinCore.getRodinDB().getRodinProjects</code>, which returns an array with of all existing <code>IRodinProject</code>s.

			==How to read a Machine or a Context==
			Machines and Contexts are accessed through <code>IMachineRoot</code> and <code>IContextRoot</code> respectively. Those roots are stored in <code>IRodinFile</code>s.

			The following method returns all existing <code>IMachineRoot</code>s of a project: