Current Proof Tree Node in UI

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

The actual issue is to display information which is meaningful to the user. For this, we need to know on which proof tree node the user is focusing, so that we can show the information associated to this node.

In the Eclipse GUI, there is the notion of an active part (i.e., view or editor). The best design is then to refresh the Rule Details and Type environment views based on the active part, which is a clear vector of the user focus.

Some parts which have an associated proof tree node are currently :

• the Proof Tree and Proof Skeleton views (it is their selection),
• the Hypotheses, Goal and ProofControl parts (it is the current proof tree node of the user support).

Some other parts do not have any associated proof tree node, such as a model editor or the Event-B Explorer view. The Rule Details and Type environment views should then refresh based on the latest active part that has an associated proof tree node.