Single View Design

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: All projects, files and folder (keep this one checked!).
• Working Sets: Allows you to see the working sets as top level elements.
• Simple Context Structure: Lists all contexts of a project.
• Complex Context Structure: Lists all contexts of a project. Contexts that extend another context are attached to it as children in the tree. Contexts that are seen by a machine are attached to the machine as children. Choose either the complex or the simple structure. It is not recommended to have both active at the same time.
• Simple Machines Structure: Lists all machines of a project.
• Complex Context Structure: Lists all machines of a project. Machines that refine another machine are attached to it as children in the tree. Choose either the complex or the simple structure. It is not recommended to have both active at the same time.
• Carrier Sets
• Constants
• Variables
• Axioms
• Invariants
• Theorems
• Events
• Proof Obligations: All proof obligations of a machine, context, axiom, invariant, theorem or event.

Filters

The filters let you choose what to hide in the navigator.

• File extensions: There are various filters to hide certain types of files.
• All files and folders: Hides all files and subfolders
• Non Rodin Projects: Hides all non Rodin projects. Also hides closed Rodin Projects.
• Closed Projects: Hides all closed projects.

There are some additional filters that can be found on top of the navigator:

Enter a text into the field and only proof obligations containing the string will be shown. If you push the green button, all discharged proof obligations will be hidden.