Event-B XText Front-end - Revision history

imported>Son at 23:20, 21 July 2017

2017-07-21T23:20:48Z

← Older revision		Revision as of 23:20, 21 July 2017
Line 1:		Line 1:
	{{TOCright}}		{{TOCright}}
	Return to [[Rodin Plug-ins]]		Return to [[Rodin Plug-ins]]

			'''IMPORTANT''': Event-B XText Front-end is now developed into [[XEvent-B\| ''extended Event-B (XEvent-B)'']].

	The Event-B XText front-end provides text editors for XContexts and and XMachines which then compiled automatically to Event-B contexts and machines.		The Event-B XText front-end provides text editors for XContexts and and XMachines which then compiled automatically to Event-B contexts and machines.

imported>Son: /* Current version */

2017-01-28T19:02:17Z

Current version

← Older revision		Revision as of 19:02, 28 January 2017
Line 9:		Line 9:

	=== Current version ===		=== Current version ===
	The Event-B XText front-end 0.0.2 is available as a separate plug-in from the main Rodin update site (under the Editor category).		The Event-B XText front-end 0.0.5 is available as a separate plug-in from the main Rodin update site (under the Editor category).

	=== Principles ===		=== Principles ===
	The Event-B XText editors (i.e., XContext and XMachine editors) do not work directly on the Rodin files. Instead, they operate on the separate XContext and XMachine and they are compiled to the Rodin files.		The Event-B XText editors (i.e., XContext and XMachine editors) do not work directly on the Rodin files. Instead, they operate on the separate XContext and XMachine and they are compiled to the Rodin files.

imported>Son at 07:06, 23 November 2016

2016-11-23T07:06:03Z

← Older revision		Revision as of 07:06, 23 November 2016
Line 13:		Line 13:
	=== Principles ===		=== Principles ===
	The Event-B XText editors (i.e., XContext and XMachine editors) do not work directly on the Rodin files. Instead, they operate on the separate XContext and XMachine and they are compiled to the Rodin files.		The Event-B XText editors (i.e., XContext and XMachine editors) do not work directly on the Rodin files. Instead, they operate on the separate XContext and XMachine and they are compiled to the Rodin files.

	~~=== A basic overview ===~~

	~~[[Category:Plugin]]~~
	~~[[Category:User documentation]]~~

imported>Son: /* Current version */

2016-11-04T17:34:41Z

Current version

← Older revision		Revision as of 17:34, 4 November 2016
Line 9:		Line 9:

	=== Current version ===		=== Current version ===
	The Event-B XText front-end is available as a separate plug-in from the main Rodin update site (under the Editor category).		The Event-B XText front-end 0.0.2 is available as a separate plug-in from the main Rodin update site (under the Editor category).


	=== Principles ===		=== Principles ===

imported>Son at 17:34, 4 November 2016

2016-11-04T17:34:25Z

← Older revision		Revision as of 17:34, 4 November 2016
Line 1:		Line 1:
	{{TOCright}}		{{TOCright}}
	Return to [[Rodin Plug-ins]]		Return to [[Rodin Plug-ins]]

	~~[[Image:RodinEditor_basicView1.png\|450px\|left\|a basic view of the XContext Editor on a context]]~~

	The Event-B XText front-end provides text editors for XContexts and and XMachines which then compiled automatically to Event-B contexts and machines.		The Event-B XText front-end provides text editors for XContexts and and XMachines which then compiled automatically to Event-B contexts and machines.

imported>Son: /* A basic overview */

2016-11-04T15:33:48Z

A basic overview

@@ Line 18: / Line 18: @@
 === A basic overview ===
 [[Category:Plugin]]
 [[Category:User documentation]]

imported>Son: /* Principles */

2016-11-04T15:32:33Z

Principles

@@ Line 15: / Line 15: @@
 === Principles ===
-'''The component contents are displayed as text.''' Once you component opened with the Rodin Editor, its contents are printed as text inside the Rodin Editor. However, as said, the Rodin Editor is not a text editor, and even if the component you edit is streamlined to basic text, what you edit is stored in an underlying database. That's the reason why you can not type text at any place at any moment. (i.e. there is no parsing of text file: what you see is a text component based form editor).
+The Event-B XText editors (i.e., XContext and XMachine editors) do not work directly on the Rodin files. Instead, they operate on the separate XContext and XMachine and they are compiled to the Rodin files.
 === A basic overview ===

imported>Son at 15:21, 4 November 2016

2016-11-04T15:21:49Z

← Older revision		Revision as of 15:21, 4 November 2016
Line 1:		Line 1:
	This ~~page~~ is ~~maintained~~		{{TOCright}}
			Return to [[Rodin Plug-ins]]

			[[Image:RodinEditor_basicView1.png\|450px\|left\|a basic view of the XContext Editor on a context]]

			The Event-B XText front-end provides text editors for XContexts and and XMachines which then compiled automatically to Event-B contexts and machines.

			<br style="clear: both" />

			Please have a look also at the [[Event-B XText Front-end User Guide]].

			=== Current version ===
			The Event-B XText front-end is available as a separate plug-in from the main Rodin update site (under the Editor category).


			=== Principles ===
			'''The component contents are displayed as text.''' Once you component opened with the Rodin Editor, its contents are printed as text inside the Rodin Editor. However, as said, the Rodin Editor is not a text editor, and even if the component you edit is streamlined to basic text, what you edit is stored in an underlying database. That's the reason why you can not type text at any place at any moment. (i.e. there is no parsing of text file: what you see is a text component based form editor).

			'''There are two types of edition possible.''' Because Rodin manipulates Event-B elements and their attributes, the Rodin Editor provides two ways to modify Event-B models:
			* you can navigate through the model contents and do things on the Event-B elements (e.g. add/remove/move/etc.) with the right-click actions or the keyboard shortcuts, depending on where is your cursor, or what you selected,
			* you can edit the Event-B element's attributes by entering the "edition" mode provided by the overlay editor. This is detailed here-after.

			'''An overlay editor displays over the text to edit element's attributes''' The basic idea is: ''"when I want to edit some contents, I should open the overlay editor that will allow me to modify its value"''.

			'''Everything happens where I click, or where my text caret is.''' The caret position, also set when the user left-clicks in the editor, is the base for component modifications:
			* if you click an editable attribute, the overlay editor opens on it and you are able to modify the attribute. The same action is possible if you press "Backspace" if the caret is on an editable attribute,
			* if you click on non editable places of the editor, you just move the text caret to the pointed position.

			'''Implicit elements are displayed in grayed colors.''' The elements that are implicit at the current level of edition are not editable, and displayed in grayed colors. (See the figure below)
			[[Image:RodinEditor_basicView4.png\|500px\|center]]

			=== A basic overview ===
			The Rodin Editor might not be the 'preferred' editor that Rodin uses to open your Event-B models.<br>
			Thus, to open a component (e.g. a machine, a context, etc.), '''right-click''' on it and select '''Open with''' > '''Rodin Editor'''.<br>
			The context component is then opened with the Rodin Editor.<br>

			[[Image:RodinEditor_basicView2.png\|600px]]

			On the figure above, you see the context component.<br>
			* The user is editing the axiom ''axm8'' and we see that the text is black and the background is grayed. This is the actually the overlay editor, that is open to edit the predicate contained by the axiom ''axm8''.
			* There are buttons in the left ruler to fold some elements.
			* The comments are preceeded by the character ' › ' to indicate where to click for edition.
			* The other attributes are inlined as grayed text.
			** Note that : some attributes have type boolean, thus change value on click, and some attributes are choice attributes thus display a list of clickable values (see the image below) on click.

			[[Image:RodinEditor_basicView3.png\|center]]

			For more details, please go to the [[Rodin_Editor_User_Guide\| Rodin Editor User Guide]].

			[[Category:Plugin]]
			[[Category:User documentation]]

imported>Son: Created page with "This page is maintained"

2016-11-04T15:07:26Z

Created page with "This page is maintained"

New page

This page is maintained