Difference between pages "Proof Skeleton View" and "Providing help for your plug-in (How to extend Rodin Tutorial)"

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>Mathieu
 
imported>Pascal
 
Line 1: Line 1:
−
==Purpose==
+
{{Navigation|Previous= [['''FIXME'''|Extending the Proof Obligation Generator]]|Next=[['''FIXME'''|Extending the structured editor]] | Up= [[Plug-in_Tutorial|How to extend Rodin Tutorial (Index)]]}}
  
−
The Proof Skeleton View gives the user the ability to quickly browse the skeleton of a proof, without having to prove it anew. Furthermore, it is intended to be a convenient way to display rules and sequents together in the same view.
+
=== Providing Help Contents ===
 +
Each plug-in that contributes help files shall extend the <tt>org.eclipse.help.toc</tt> extension point and create the TOC files that describe the table of contents for the help and the topic interleaving.
  
−
==The Proof Skeleton View==
+
==== Creating the Help Plug-in ====
 +
Let's first create such a plug-in. It will only contain documentation files, and the "Create Java Project" option (tag 1) do not need to be checked.
  
−
===Showing the View===
+
[[Image:help_project.png]]
  
−
The Proof Skeleton View is available as other views in the
+
Then, the easiest way to proceed for beginners is to start from the available template:
−
Window > Show View > Other > Event-B > Proof Skeleton View
 
−
menu.
 
  
−
To watch a proof skeleton, simply select a proved predicate in the obligation explorer, or a proof file in the editor.
+
[[Image:help_project_template.png]]
  
−
===View Interpretation===
+
[[Image:help_project_toc.png]]
  
−
Proof skeletons are displayed in a two-part view. On the left hand side is the tree structure of rules applied in the proof. On the other side stands the sequent on which the currently selected rule is applied.
+
==== Examining the Help Files ====
 +
[[Image:help_files.png | right]]
 +
Three .xml files have been created:
 +
# plugin.xml
 +
# testToc.xml
 +
# toc.xml
  
−
[[Image:proofSkeletonView.jpg]]
+
When opening the plugin.xml file, we can see that the testToc.xml file is a primary file, i.e. it contains the master table of contents; toc.xml is not primary, but is integrated into this table of contents.
  
−
The tree can be expanded or collapsed by using [+] and [-] buttons on the upper right corner.
+
[[Image:help_plugin_file.png]]
  
 +
=== Option 1: Writing the Help Files ===
  
−
[[Category:User Documentation]]
+
=== Option 2: Generating the Help Files ===
 +
 
 +
 
 +
 
 +
{{Navigation|Previous= [['''FIXME'''|Extending the Proof Obligation Generator]]|Next= [['''FIXME'''|Extending the structured editor]] | Up= [[Plug-in_Tutorial|How to extend Rodin Tutorial (Index)]]}}
 +
 
 +
[[Category:Developer documentation|*Index]]
 +
[[Category:Rodin Platform|*Index]]
 +
[[Category:Tutorial|*Index]]

Revision as of 12:08, 23 August 2010

<prev: Extending the Proof Obligation Generator >next: Extending the structured editor ^up: How to extend Rodin Tutorial (Index)

Providing Help Contents

Each plug-in that contributes help files shall extend the org.eclipse.help.toc extension point and create the TOC files that describe the table of contents for the help and the topic interleaving.

Creating the Help Plug-in

Let's first create such a plug-in. It will only contain documentation files, and the "Create Java Project" option (tag 1) do not need to be checked.

Help project.png

Then, the easiest way to proceed for beginners is to start from the available template:

Help project template.png

Help project toc.png

Examining the Help Files

Help files.png

Three .xml files have been created:

  1. plugin.xml
  2. testToc.xml
  3. toc.xml

When opening the plugin.xml file, we can see that the testToc.xml file is a primary file, i.e. it contains the master table of contents; toc.xml is not primary, but is integrated into this table of contents.

Help plugin file.png

Option 1: Writing the Help Files

Option 2: Generating the Help Files

<prev: Extending the Proof Obligation Generator >next: Extending the structured editor ^up: How to extend Rodin Tutorial (Index)
Retrieved from ‘https://wiki.event-b.org/index.php?title=Proof_Skeleton_View&oldid=6645’