Layout improvements in the event-B editor: Difference between revisions

From Event-B
Jump to navigationJump to search
imported>Laurent
Added one suggestion
imported>Mathieu
 
Line 26: Line 26:


For instance, if an event has no abstraction (no refines clause), then the witness section is useless and need not be displayed.
For instance, if an event has no abstraction (no refines clause), then the witness section is useless and need not be displayed.
[[category:Work in progress]]

Latest revision as of 12:08, 12 August 2009

The intention of this page is to collect and discuss possible improvements of the layout in the event-B editor (edit tab).

Problem

In a user feedback report posted on the Deploy WP9 mailing list, Michael Leuschel reported the following facts:

In the newer version of Rodin (with included witnesses) the editor consumes even more space than before. Even on simple examples, one is lost (we had to copy the celebrity model on the whiteboard to get an overview). As an example, for Celebrity0 we have

  • Text representation : 149 Pixels high;
  • Rodin Pretty Printer 650 Pixels high (4.3 X);
  • Rodin Editor Expanded: 1512 Pixels high (10 X)

So, the Rodin Editor expanded takes up 10 times more space than a classical textual representation; the pretty print still over 4 times. This is a problem already for small models, which we need to fix quickly.

In an answer to this post, Christophe Ponsard wrote:

Besides all the scrolling required, another issue is the amount of folding/unfolding operations you have to do. The icons are fancy but also visually distracting due to the large amount of them.


Possible Improvements

Do not display unused sections

For instance, if an event has no abstraction (no refines clause), then the witness section is useless and need not be displayed.