Merge lp:~tapaal-contributor/tapaal/manual-edit-error-messages into lp:tapaal

[Lena Ernstsen]

The error found during parsing manually edited queries is shown to the user

[lp:~tapaal-contributor/tapaal/manual-edit-error-messages]

1138. By <email address hidden> on 2021-09-11

fixed spacing between "placeswere used"

[Jiri Srba (srba)]

review: Approve

=== modified file 'src/pipe/gui/widgets/QueryDialog.java'
--- src/pipe/gui/widgets/QueryDialog.java	2021-08-12 08:28:49 +0000
+++ src/pipe/gui/widgets/QueryDialog.java	2021-09-11 17:12:22 +0000
@@ -2293,15 +2293,28 @@
 					TCTLAbstractProperty newQuery = null;
 
 					try {
-					    if (lens.isTimed()) {
+					    if (queryField.getText().trim().equals("<*>")) {
+                            int choice = JOptionPane.showConfirmDialog(
+                                CreateGui.getApp(),
+                                "It is not possible to parse an empty query.\nThe specified query has not been saved. Do you want to edit it again?",
+                                "Error Parsing Query",
+                                JOptionPane.YES_NO_OPTION,
+                                JOptionPane.ERROR_MESSAGE);
+                            if (choice == JOptionPane.NO_OPTION)
+                                returnFromManualEdit(null);
+                            else
+                                return;
+                        } else if (lens.isTimed()) {
                             newQuery = TAPAALQueryParser.parse(queryField.getText());
                         } else {
 						    newQuery = TAPAALCTLQueryParser.parse(queryField.getText());
                         }
 					} catch (Throwable ex) {
+					    String message = ex.getMessage() == null ? "TAPAAL encountered an error while trying to parse the specified query\n" :
+                            "TAPAAL encountered the following error while trying to parse the specified query:\n\n"+ex.getMessage();
 						int choice = JOptionPane.showConfirmDialog(
 								CreateGui.getApp(),
-								"TAPAAL encountered an error trying to parse the specified query.\n\nWe recommend using the query construction buttons unless you are an experienced user.\n\n The specified query has not been saved. Do you want to edit it again?",
+								message+"\nWe recommend using the query construction buttons unless you are an experienced user.\n\n The specified query has not been saved. Do you want to edit it again?",
 								"Error Parsing Query",
 								JOptionPane.YES_NO_OPTION,
 								JOptionPane.ERROR_MESSAGE);
@@ -2309,7 +2322,6 @@
 							returnFromManualEdit(null);
 						else
 							return;
-
 					}
 
 					if (newQuery != null) // new query parsed successfully
@@ -2343,7 +2355,7 @@
 						if (isResultFalse) {
 							StringBuilder s = new StringBuilder();
 							s.append("The following places" + (lens.isTimed() ? "" : " or transitions") +
-                                "were used in the query, but are not present in your model:\n\n");
+                                " were used in the query, but are not present in your model:\n\n");
 
 							for (String placeName : c.getIncorrectPlaceNames()) {
 								s.append(placeName);