From bc7eafab00b8cf517f65807d4031fc0e06d81470 Mon Sep 17 00:00:00 2001
From: dgelessus <dgelessus@users.noreply.github.com>
Date: Thu, 2 Jul 2020 19:26:42 +0200
Subject: [PATCH] Display pretty operation names in operation execution output
---
notebooks/tests/animate.ipynb | 12 ++++++------
src/main/java/de/prob2/jupyter/ProBKernel.java | 2 +-
2 files changed, 7 insertions(+), 7 deletions(-)
diff --git a/notebooks/tests/animate.ipynb b/notebooks/tests/animate.ipynb
index 68fef0d..15c0a4c 100644
--- a/notebooks/tests/animate.ipynb
+++ b/notebooks/tests/animate.ipynb
@@ -281,7 +281,7 @@
{
"data": {
"text/plain": [
- "Executed operation: $setup_constants()"
+ "Executed operation: SETUP_CONSTANTS()"
]
},
"execution_count": 11,
@@ -391,7 +391,7 @@
{
"data": {
"text/plain": [
- "Executed operation: $initialise_machine()"
+ "Executed operation: INITIALISATION()"
]
},
"execution_count": 16,
@@ -734,7 +734,7 @@
{
"data": {
"text/plain": [
- "Executed operation: $setup_constants()"
+ "Executed operation: SETUP_CONSTANTS()"
]
},
"execution_count": 31,
@@ -754,7 +754,7 @@
{
"data": {
"text/plain": [
- "Executed operation: $initialise_machine()"
+ "Executed operation: INITIALISATION()"
]
},
"execution_count": 32,
@@ -906,7 +906,7 @@
{
"data": {
"text/plain": [
- "Executed operation: $setup_constants()"
+ "Executed operation: SETUP_CONSTANTS()"
]
},
"execution_count": 38,
@@ -949,7 +949,7 @@
{
"data": {
"text/plain": [
- "Executed operation: $initialise_machine()"
+ "Executed operation: INITIALISATION()"
]
},
"execution_count": 40,
diff --git a/src/main/java/de/prob2/jupyter/ProBKernel.java b/src/main/java/de/prob2/jupyter/ProBKernel.java
index 3d3f24a..9f852d1 100644
--- a/src/main/java/de/prob2/jupyter/ProBKernel.java
+++ b/src/main/java/de/prob2/jupyter/ProBKernel.java
@@ -319,7 +319,7 @@ public final class ProBKernel extends BaseKernel {
this.animationSelector.changeCurrentAnimation(trace.add(op));
trace.getStateSpace().evaluateTransitions(Collections.singleton(op), FormulaExpand.TRUNCATE);
- return new DisplayData(String.format("Executed operation: %s", op.getRep()));
+ return new DisplayData(String.format("Executed operation: %s", op.getPrettyRep()));
}
@Override
--
GitLab