Commit 0c852f45 authored by Sarah Grebing's avatar Sarah Grebing

Added new Dilaogtype for end of script

parent 445f6a6d
Pipeline #17142 passed with stages
in 15 minutes and 8 seconds
......@@ -91,12 +91,17 @@ public class PTreeNode<T> {
}
public String getSingleRepresentation() {
if (getStatement().getStartPosition() != null)
return String.format("%d: %s",
getStatement().getStartPosition().getLineNumber(),
getStatement().accept(new ShortCommandPrinter()));
else
if (getStatement().getStartPosition() != null) {
if (getStatement().getStartPosition().getLineNumber() >= 0) {
return String.format("%d: %s",
getStatement().getStartPosition().getLineNumber(),
getStatement().accept(new ShortCommandPrinter()));
} else {
return "End of Script";
}
} else {
return (String) getStatement().accept(new ShortCommandPrinter());
}
}
@Override
......
......@@ -531,7 +531,13 @@ public class DebuggerMain implements Initializable {
assert statePointer != null;
State<KeyData> lastState = statePointer.getStateAfterStmt();
getInspectionViewsController().getActiveInspectionViewTab().activate(statePointer, lastState);
if (lastState.getGoals().isEmpty()) {
statusBar.setNumberOfGoals(0);
Utils.showClosedProofDialog("the script " + scriptController.getMainScript().getScriptName());
} else {
Utils.showOpenProofNotificationDialog(lastState.getGoals().size());
//(lastState.getGoals().size());
}
});
}
......
......@@ -48,7 +48,7 @@ public class DebuggerStatusBar extends StatusBar {
private IntegerProperty numberOfGoals = new SimpleIntegerProperty(0);
private Label lblCurrentNodes = new Label("#nodes: %s");
private Label lblCurrentNodes = new Label("#open goals: " + numberOfGoals.intValue());
private Label lblMainscript = new Label();
......@@ -68,10 +68,11 @@ public class DebuggerStatusBar extends StatusBar {
lblMainscript,
new Separator(),
interpreterStatusView
//lblCurrentNodes,
//lblCurrentNodes
//progressIndicator
);
interpreterStatusModel.addListener((p, o, n) -> {
interpreterStatusView.setIcon(n.getIcon());
if (n == InterpreterThreadState.ERROR)
......@@ -81,7 +82,11 @@ public class DebuggerStatusBar extends StatusBar {
});
numberOfGoals.addListener((observable, oldValue, newValue) -> {
lblCurrentNodes.setText("#nodes: " + newValue);
if (newValue.intValue() > 0) {
lblCurrentNodes.setText("#open Goals: " + newValue);
} else {
lblCurrentNodes.setText("No open goals");
}
});
mainScriptIdentifier.addListener((ov, o, n) -> {
......
package edu.kit.iti.formal.psdbg.gui.controls;
import de.jensd.fx.glyphs.materialdesignicons.MaterialDesignIcon;
import de.jensd.fx.glyphs.materialdesignicons.MaterialDesignIconView;
import de.uka.ilkd.key.logic.op.IProgramMethod;
import de.uka.ilkd.key.pp.ProgramPrinter;
import de.uka.ilkd.key.speclang.Contract;
......@@ -11,13 +13,14 @@ import javafx.beans.value.ChangeListener;
import javafx.beans.value.ObservableValue;
import javafx.collections.ObservableList;
import javafx.fxml.FXMLLoader;
import javafx.scene.control.Alert;
import javafx.scene.control.Label;
import javafx.scene.control.TextArea;
import javafx.scene.control.*;
import javafx.scene.input.Clipboard;
import javafx.scene.input.DataFormat;
import javafx.scene.layout.GridPane;
import javafx.scene.layout.Pane;
import javafx.scene.layout.Priority;
import javafx.scene.layout.VBox;
import javafx.util.Pair;
import org.antlr.v4.runtime.CharStreams;
import org.antlr.v4.runtime.Token;
import org.apache.logging.log4j.LogManager;
......@@ -269,6 +272,37 @@ public class Utils {
alert.showAndWait();
}
public static void showOpenProofNotificationDialog(int noOfGoals) {
Dialog<Pair<String, String>> dialog = new Dialog<>();
dialog.setTitle("Interpreter Finished Successfully");
dialog.setHeaderText("Interactive Mode Possible");
dialog.setGraphic(new MaterialDesignIconView(MaterialDesignIcon.HAND_POINTING_RIGHT, "24.0"));
ButtonType okButtonType = new ButtonType("OK", ButtonBar.ButtonData.OK_DONE);
dialog.getDialogPane().getButtonTypes().addAll(okButtonType);
GridPane grid = new GridPane();
grid.setHgap(10);
grid.setVgap(10);
// grid.setPadding(new Insets(20, 150, 10, 10));
grid.add(new Label("Interpreter finished successfully"), 0, 0);
String msg = String.format("%s %d %s ", "There were still", noOfGoals,
"open goals.");
String msg2 = "You can continue the proof interactively by using the interactive button.\n This enables to point and click onto the sequents and apply rules";
grid.add(new Label(msg), 0, 1);
grid.add(new MaterialDesignIconView(MaterialDesignIcon.HAND_POINTING_RIGHT, "24.0"), 1, 1);
//dialog.getDialogPane().setContent(grid);
Label ta = new Label(msg2);
ta.setWrapText(true);
Pane p = new VBox(grid, ta);
dialog.getDialogPane().setContent(p);
dialog.showAndWait();
}
public static void intoClipboard(String s) {
Map<DataFormat, Object> map = Collections.singletonMap(DataFormat.PLAIN_TEXT, s);
Clipboard.getSystemClipboard().setContent(map);
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment