Difference between revisions of "Single View Design"

From Event-B
Jump to navigationJump to search
imported>Maria
imported>Maria
Line 8: Line 8:
 
*A complex structure where the machines and contexts are presented as a tree. Thus dependencies between machines and contexts (like ''refines'' or ''sees'') are made visible.
 
*A complex structure where the machines and contexts are presented as a tree. Thus dependencies between machines and contexts (like ''refines'' or ''sees'') are made visible.
  
−
==The Content Providers==
+
 
 +
===The Content Providers===
 
There's a number of content providers to choose from:
 
There's a number of content providers to choose from:
−
*Projects: This content provider shows all open rodin projects. Closed projects are currently not shown. If this content provider is not selected the navigator is empty.
 
−
*Simple Machine and Context Structure: This content provider shows all machines and contexts in a simple way.
 
−
*Complex Machine and Context Structure: This content provider shows all machines and contexts in a complex way (dependencies made visible).
 
−
*Invariants, Events etc: There's a content provider for each of those elements. It shows all invariants (or any other chosen type) of a machine.
 
−
*Proof Obligations: This content provider shows all Proof Obligations.
 
  
−
===The Actions===
 
−
The following actions are available in the navigator:
 
−
*Projects: Delete, Rename, Copy
 
−
*Machines: Delete, Rename, Refine, Prove interactively
 
−
*Contexts: Delete, Extend, Prove interactively
 
−
*Proof Obligations: Retry Auto Provers, Recalculate Auto Status
 
−
*Globally: New Project, New Component
 
  
−
On double click each element is opened in an editor.
+
==User guide==
 +
===Customizing the Navigator===
 +
Click on the little triangle in the upper right corner of the navigator view and select ''Customize View''. This opens a dialog that allows you to choose ''Filters'' and ''Content''.
 +
 
 +
====Content====
 +
Here you can choose what content should be shown in the navigator.
 +
*'''Resources''': It is strongly recommended to keep this one checked, otherwise the navigator will be empty. This content providers populates the navigator with all projects, files and folder in the workspace.
 +
*'''Working Sets''': This content provider allows you to see the working sets.
 +
 
 +
 
  
−
===The Filters===
 
−
The following filters are available in the navigator:
 
−
*A filter that hides discharged proof obligations.
 
−
*A filter that hides all proof obligations that don't contain a given string in their name.
 
  
 
[[Category:Work in progress]]
 
[[Category:Work in progress]]

Revision as of 15:54, 2 October 2008

Purpose

The Purpose of the Single View Design is to present everything in a single view in Rodin.

Specification

The Navigator

The navigator presents all projects and their contents. The users can choose between to ways how the machines and contexts will be presented:

  • A simple structure where all machines and contexts are presented on the same level
  • A complex structure where the machines and contexts are presented as a tree. Thus dependencies between machines and contexts (like refines or sees) are made visible.


The Content Providers

There's a number of content providers to choose from:


User guide

Customizing the Navigator

Click on the little triangle in the upper right corner of the navigator view and select Customize View. This opens a dialog that allows you to choose Filters and Content.

Content

Here you can choose what content should be shown in the navigator.

  • Resources: It is strongly recommended to keep this one checked, otherwise the navigator will be empty. This content providers populates the navigator with all projects, files and folder in the workspace.
  • Working Sets: This content provider allows you to see the working sets.
Retrieved from ‘https://wiki.event-b.org/index.php?title=Single_View_Design&oldid=9416’