diff --git a/de.prob.ui/plugin.xml b/de.prob.ui/plugin.xml
index d1b07bd82110aa5b4467bc12b6c9d1cb75165606..31a3a0a82deaec1c94bd4eea20d9cfd4df7530db 100644
--- a/de.prob.ui/plugin.xml
+++ b/de.prob.ui/plugin.xml
@@ -284,6 +284,12 @@
<state class="org.eclipse.jface.commands.ToggleState"
id="de.prob.ui.stateview.duplicateFilterState" />
</command>
+ <command
+ id="de.prob.ui.history.toggleShowParameters"
+ name="Show event parameters">
+ <state class="org.eclipse.jface.commands.ToggleState"
+ id="de.prob.ui.history.showParametersState" />
+ </command>
<command
id="de.prob.ui.show_parameter_dialog"
name="Show Parameter Dialog">
@@ -608,6 +614,20 @@
</with>
</enabledWhen>
</handler>
+ <handler
+ commandId="de.prob.ui.history.toggleShowParameters">
+ <class
+ class="de.prob.ui.historyview.ToggleShowParametersHandler">
+ </class>
+ <enabledWhen>
+ <with
+ variable="de.prob.core.model_loaded">
+ <equals
+ value="enabled">
+ </equals>
+ </with>
+ </enabledWhen>
+ </handler>
<handler
commandId="de.prob.ui.show_parameter_dialog">
<class
@@ -790,6 +810,15 @@
style="push">
</command>
</menuContribution>
+ <menuContribution
+ locationURI="toolbar:de.prob.ui.HistoryView">
+ <command
+ commandId="de.prob.ui.history.toggleShowParameters"
+ icon="icons/filter_ps.gif"
+ label="Show Parameters"
+ style="toggle">
+ </command>
+ </menuContribution>
<menuContribution
locationURI="toolbar:de.prob.ui.OperationView">
diff --git a/de.prob.ui/src/de/prob/ui/historyview/HistoryEventLabelProvider.java b/de.prob.ui/src/de/prob/ui/historyview/HistoryEventLabelProvider.java
index f407ed98c034bc03d58546d176b7347400f68b28..8f3a80100bec876443f07a8ad0c8866b5066b8a8 100644
--- a/de.prob.ui/src/de/prob/ui/historyview/HistoryEventLabelProvider.java
+++ b/de.prob.ui/src/de/prob/ui/historyview/HistoryEventLabelProvider.java
@@ -1,5 +1,6 @@
package de.prob.ui.historyview;
+import java.util.Collection;
import java.util.List;
import de.prob.core.domainobjects.Operation;
@@ -27,10 +28,16 @@ class HistoryEventLabelProvider extends HistoryLabelProvider {
if (operation != null) {
List<EventStackElement> stack = operation.getEventStack();
if (stack != null) {
- result = eventStackPosition < stack.size() ? stack.get(
- eventStackPosition).getEventName() : null;
+ if (eventStackPosition < stack.size()) {
+ EventStackElement stackElem = stack.get(eventStackPosition);
+ result = printEventWithParameters(stackElem.getEventName(),
+ stackElem.getParameters());
+ } else {
+ result = null;
+ }
} else {
- result = eventStackPosition == 0 ? operation.getName() : null;
+ result = eventStackPosition == 0 ? printEventWithParameters(
+ operation.getName(), operation.getArguments()) : null;
}
} else {
result = eventStackPosition == 0 ? HistoryViewStrings.uninitialisedState
@@ -39,4 +46,27 @@ class HistoryEventLabelProvider extends HistoryLabelProvider {
return result == null ? "" : result;
}
+ private String printEventWithParameters(final String name,
+ final Collection<String> parameters) {
+ final String result;
+ if (!showParameters || parameters.isEmpty()) {
+ result = name;
+ } else {
+ StringBuilder sb = new StringBuilder();
+ sb.append(name);
+ sb.append('(');
+ boolean isFirst = true;
+ for (final String param : parameters) {
+ if (!isFirst) {
+ sb.append(',');
+ }
+ sb.append(param);
+ isFirst = false;
+ }
+ sb.append(')');
+ result = sb.toString();
+ }
+ return result;
+ }
+
}
\ No newline at end of file
diff --git a/de.prob.ui/src/de/prob/ui/historyview/HistoryLabelProvider.java b/de.prob.ui/src/de/prob/ui/historyview/HistoryLabelProvider.java
index 950d972b0f8b6b732e0bf5c5f2033f0d18e4263b..818e3e2bea695445c1ac6f19f0e9c0bd8abc3e79 100644
--- a/de.prob.ui/src/de/prob/ui/historyview/HistoryLabelProvider.java
+++ b/de.prob.ui/src/de/prob/ui/historyview/HistoryLabelProvider.java
@@ -24,6 +24,8 @@ public abstract class HistoryLabelProvider extends CellLabelProvider {
final Font bold = JFaceResources.getFontRegistry().getBold(
JFaceResources.BANNER_FONT);
+ protected boolean showParameters;
+
@Override
public void update(final ViewerCell cell) {
final Object element = cell.getElement();
@@ -51,4 +53,8 @@ public abstract class HistoryLabelProvider extends CellLabelProvider {
protected Color getForeground(final HistViewItem item) {
return null;
}
+
+ public void setShowParameters(final boolean show) {
+ showParameters = show;
+ }
}
diff --git a/de.prob.ui/src/de/prob/ui/historyview/HistoryView.java b/de.prob.ui/src/de/prob/ui/historyview/HistoryView.java
index 1b07a0246949381fe9abf814674c00133517f4d5..b6dd099a042da661381d6295ff864e791e9fccd5 100644
--- a/de.prob.ui/src/de/prob/ui/historyview/HistoryView.java
+++ b/de.prob.ui/src/de/prob/ui/historyview/HistoryView.java
@@ -3,6 +3,7 @@
*/
package de.prob.ui.historyview;
+import java.util.ArrayList;
import java.util.Collection;
import org.apache.commons.lang.ArrayUtils;
@@ -54,6 +55,7 @@ public class HistoryView extends StateBasedViewPart {
public static final String VIEW_ID = "de.prob.ui.HistoryView";
private TableViewer tableViewer;
+ private Collection<HistoryLabelProvider> labelProviders;
@Override
protected Control createStatePartControl(final Composite parent) {
@@ -164,21 +166,23 @@ public class HistoryView extends StateBasedViewPart {
private void createColumns(final Composite composite) {
final Animator animator = Animator.getAnimator();
- MachineDescription machineDescription = animator.getMachineDescription();
+ MachineDescription machineDescription = animator
+ .getMachineDescription();
String[] models = new String[0];
if (machineDescription != null) {
- models = machineDescription
- .getModelNames().toArray(new String[0]);
+ models = machineDescription.getModelNames().toArray(new String[0]);
ArrayUtils.reverse(models);
}
final TableColumnLayout layout = new TableColumnLayout();
composite.setLayout(layout);
+ labelProviders = new ArrayList<HistoryLabelProvider>();
if (models.length > 0) {
int pos = 0;
for (final String model : models) {
final boolean isFirst = pos == 0;
- createColumn(layout, model, new HistoryEventLabelProvider(pos),
- isFirst);
+ final HistoryEventLabelProvider labelProvider = new HistoryEventLabelProvider(
+ pos);
+ createColumn(layout, model, labelProvider, isFirst);
pos++;
}
} else {
@@ -200,6 +204,7 @@ public class HistoryView extends StateBasedViewPart {
final ColumnWeightData weightData = setMinimumSize ? new ColumnWeightData(
1, 100) : new ColumnWeightData(1);
layout.setColumnData(column, weightData);
+ labelProviders.add(labelProvider);
}
@Override
@@ -320,4 +325,19 @@ public class HistoryView extends StateBasedViewPart {
}
}
+ public void setShowParameters(boolean show) {
+ if (labelProviders != null) {
+ for (HistoryLabelProvider provider : labelProviders) {
+ provider.setShowParameters(show);
+ }
+ }
+ final Runnable runnable = new Runnable() {
+ @Override
+ public void run() {
+ tableViewer.refresh();
+ }
+ };
+ Display.getDefault().asyncExec(runnable);
+ }
+
}
diff --git a/de.prob.ui/src/de/prob/ui/historyview/ToggleShowParametersHandler.java b/de.prob.ui/src/de/prob/ui/historyview/ToggleShowParametersHandler.java
new file mode 100644
index 0000000000000000000000000000000000000000..b907bac3bdeb47b30fb724d337fd6db154bf6d33
--- /dev/null
+++ b/de.prob.ui/src/de/prob/ui/historyview/ToggleShowParametersHandler.java
@@ -0,0 +1,79 @@
+/**
+ *
+ */
+package de.prob.ui.historyview;
+
+import java.util.Map;
+
+import org.eclipse.core.commands.AbstractHandler;
+import org.eclipse.core.commands.Command;
+import org.eclipse.core.commands.ExecutionEvent;
+import org.eclipse.core.commands.ExecutionException;
+import org.eclipse.core.commands.IHandler;
+import org.eclipse.core.commands.State;
+import org.eclipse.ui.IWorkbenchPage;
+import org.eclipse.ui.PlatformUI;
+import org.eclipse.ui.commands.ICommandService;
+import org.eclipse.ui.commands.IElementUpdater;
+import org.eclipse.ui.menus.UIElement;
+import org.eclipse.ui.services.IServiceLocator;
+
+import de.prob.ui.stateview.StateViewPart;
+
+/**
+ * @author plagge
+ *
+ */
+public class ToggleShowParametersHandler extends AbstractHandler implements
+ IHandler, IElementUpdater {
+ private static final String COMMAND_ID = "de.prob.ui.history.toggleShowParameters";
+ private static final String STATE_ID = "de.prob.ui.history.showParametersState";
+
+ @Override
+ public Object execute(ExecutionEvent event) throws ExecutionException {
+ final State state = event.getCommand().getState(STATE_ID);
+ if (state != null) {
+ final boolean newFilterValue = toggleState(state);
+ setShowParameters(newFilterValue);
+ } else
+ throw new ExecutionException("Command state " + STATE_ID
+ + " not found");
+ return null;
+ }
+
+ private boolean toggleState(final State state) {
+ final Boolean show = (Boolean) state.getValue();
+ state.setValue(!show);
+ return !show;
+ }
+
+ private void setShowParameters(final boolean show)
+ throws ExecutionException {
+ final IWorkbenchPage page = PlatformUI.getWorkbench()
+ .getActiveWorkbenchWindow().getActivePage();
+ final HistoryView view = (HistoryView) page
+ .findView(HistoryView.VIEW_ID);
+ if (view != null) {
+ view.setShowParameters(show);
+ } else
+ throw new ExecutionException("View " + StateViewPart.STATE_VIEW_ID
+ + " not found");
+ }
+
+ @Override
+ public void updateElement(UIElement element,
+ @SuppressWarnings("rawtypes") Map parameters) {
+ final State state = getCurrentState(element.getServiceLocator());
+ final Boolean filterSet = (Boolean) state.getValue();
+ element.setChecked(filterSet);
+ }
+
+ private static State getCurrentState(final IServiceLocator locator) {
+ final ICommandService service = (ICommandService) locator
+ .getService(ICommandService.class);
+ final Command command = service.getCommand(COMMAND_ID);
+ final State state = command.getState(STATE_ID);
+ return state;
+ }
+
+}