Difference between revisions of "Current Proof Tree Node in UI"

From Event-B
Jump to navigationJump to search
imported>Laurent
(New page: {{TOCright}} == Purpose == Two views (Proof Details and Type Environment) display some information which is associated to the current proof tree node, if any. However, in Rodin 2.3 these...)
 
imported>Laurent
Line 7: Line 7:
 
== Analysis ==
 
== Analysis ==
  
Here are some examples of the strange behavior of these views.
+
Here are some examples of the strange behavior of these views in Rodin 2.3+ (subversion r13884).
 
# Suppose one is performing an interactive proof of a sequent the goal of which is a universal predicate. The Type Environment view is open and displays the type environment of the sequent. The user launches the post-tactic which removes the forall from the goal. One would expect that the view would update and show the new variables that have been introduced by this proof-step.  This is not the case. The view does not refresh. One has to click on the current proof tree node in the Proof Tree view to force a refresh.
 
# Suppose one is performing an interactive proof of a sequent the goal of which is a universal predicate. The Type Environment view is open and displays the type environment of the sequent. The user launches the post-tactic which removes the forall from the goal. One would expect that the view would update and show the new variables that have been introduced by this proof-step.  This is not the case. The view does not refresh. One has to click on the current proof tree node in the Proof Tree view to force a refresh.
 
# In an interactive proof, two nodes are open in the Proof Tree view and carry different type environments. The user clicks on the red spanner in the Proof Control view to quickly move from one node to the other.  The contents of the Type Environment view does not refresh. The user has to click on the selected node in the Proof Tree view to force a refresh.
 
# In an interactive proof, two nodes are open in the Proof Tree view and carry different type environments. The user clicks on the red spanner in the Proof Control view to quickly move from one node to the other.  The contents of the Type Environment view does not refresh. The user has to click on the selected node in the Proof Tree view to force a refresh.
Line 15: Line 15:
 
A common pattern that occurs in these examples is that the view do refresh only on explicit clicks from the user in the Proof Tree or Proof Skeleton view. However, if the selection in these views is changed by external means (e.g., the Proof editor or the Event-B Explorer view), this change is ignored. Another pattern is that the Rule Details view (which is sensitive to the rule applied to a proof tree node) is not refreshed when the proof tree node changes status (e.g., from open to closed).
 
A common pattern that occurs in these examples is that the view do refresh only on explicit clicks from the user in the Proof Tree or Proof Skeleton view. However, if the selection in these views is changed by external means (e.g., the Proof editor or the Event-B Explorer view), this change is ignored. Another pattern is that the Rule Details view (which is sensitive to the rule applied to a proof tree node) is not refreshed when the proof tree node changes status (e.g., from open to closed).
  
Finally, another minor issue is when the view is displayed as a fast view.  Then, initially the view is empty. If one clicks on its icon to make it visible, the view gets displayed but without contents if the current global Eclipse selection is not exactly a proof tree node.
+
Finally, another minor issue is when the view is displayed as a fast view.  Then, after platform startup, the view is empty. If one clicks on its icon to make it visible, the view gets displayed but without contents if the current global Eclipse selection is not exactly a proof tree node.
  
 
== Design Decisions ==
 
== Design Decisions ==

Revision as of 18:14, 16 December 2011

Purpose

Two views (Proof Details and Type Environment) display some information which is associated to the current proof tree node, if any. However, in Rodin 2.3 these view do not always display the expected information. This entails that the end-user often has to click in several places to force a refresh of these views. We would like that these views behave more user-friendly and always display the expected information.

Analysis

Here are some examples of the strange behavior of these views in Rodin 2.3+ (subversion r13884).

  1. Suppose one is performing an interactive proof of a sequent the goal of which is a universal predicate. The Type Environment view is open and displays the type environment of the sequent. The user launches the post-tactic which removes the forall from the goal. One would expect that the view would update and show the new variables that have been introduced by this proof-step. This is not the case. The view does not refresh. One has to click on the current proof tree node in the Proof Tree view to force a refresh.
  2. In an interactive proof, two nodes are open in the Proof Tree view and carry different type environments. The user clicks on the red spanner in the Proof Control view to quickly move from one node to the other. The contents of the Type Environment view does not refresh. The user has to click on the selected node in the Proof Tree view to force a refresh.
  3. The proof tree contains one open node. The user launches a tactic that closes this node. The selected proof tree node is now closed. However, the Rule Details view does not show the rule that has been applied, it stays empty. The user has to click on the selected node in the Proof Tree view to force a refresh of the Rule Details view.
  4. The Proof Skeleton view is displayed. The user clicks on a proof obligation in the Event-B Explorer view. The proof skeleton gets refreshed by this action. However, neither the Type Environment, nor the Rule Details view get refreshed. The user has to click on a node of the Proof Skeleton view to force a refresh.

A common pattern that occurs in these examples is that the view do refresh only on explicit clicks from the user in the Proof Tree or Proof Skeleton view. However, if the selection in these views is changed by external means (e.g., the Proof editor or the Event-B Explorer view), this change is ignored. Another pattern is that the Rule Details view (which is sensitive to the rule applied to a proof tree node) is not refreshed when the proof tree node changes status (e.g., from open to closed).

Finally, another minor issue is when the view is displayed as a fast view. Then, after platform startup, the view is empty. If one clicks on its icon to make it visible, the view gets displayed but without contents if the current global Eclipse selection is not exactly a proof tree node.

Design Decisions

Implementation