rework on script area

src/main/java/edu/kit/formal/gui/controller/DebuggerMainWindowController.java

@@ -166,14 +166,11 @@ public class DebuggerMainWindowController implements Initializable {
         inspectionViewTabPane.createNewInspectionViewTab(model, true);
 
 
-        tabPane.getActiveScriptAreaTab().getScriptArea().getMarkedLines().addListener(new SetChangeListener<Integer>() {
-
-            @Override
-            public void onChanged(Change<? extends Integer> change) {
-                blocker.getBreakpoints().clear();
-                blocker.getBreakpoints().addAll(change.getSet());
-            }
-        });
+        //TODO this does not work any more
+        /*tabPane.getActiveScriptAreaTab().getScriptArea().getMarkedLines().addListener((SetChangeListener<Integer>) change -> {
+            blocker.getBreakpoints().clear();
+            blocker.getBreakpoints().addAll(change.getSet());
+        });*/
 
         blocker.currentGoalsProperty().addListener((o, old, fresh) -> {
             model.currentGoalNodesProperty().setAll(fresh);
@@ -199,9 +196,7 @@ public class DebuggerMainWindowController implements Initializable {
         int line = lm.getLine(scriptArea.getCaretPosition());
         int inLine = lm.getCharInLine(scriptArea.getCaretPosition());
 */
-        ib.ignoreLinesUntil(tabPane.getActiveScriptAreaTab().getScriptArea().getCaretPosition());
-
-
+        ib.ignoreLinesUntil(tabPane.getSelectedScriptArea().getCaretPosition());
         executeScript(ib, true);
     }
 
@@ -222,7 +217,7 @@ public class DebuggerMainWindowController implements Initializable {
         blocker.deinstall();
         statusBar.publishMessage("Parse ...");
         try {
-            List<ProofScript> scripts = Facade.getAST(tabPane.getActiveScriptAreaTab().getScriptArea().getText());
+            List<ProofScript> scripts = Facade.getAST(tabPane.getSelectedScriptArea().getText());
             statusBar.publishMessage("Creating new Interpreter instance ...");
             ib.setScripts(scripts);
             ib.captureHistory();
@@ -235,7 +230,7 @@ public class DebuggerMainWindowController implements Initializable {
             blocker.install(currentInterpreter);
 
             System.out.println("Start of Script in: " + scripts.get(0).getStartPosition());
-            tabPane.getActiveScriptAreaTab().getScriptArea().setDebugMark(scripts.get(0).getStartPosition().getLineNumber());
+            tabPane.getSelectedScriptArea().setDebugMark(scripts.get(0).getStartPosition().getLineNumber());
 
             interpreterService.interpreter.set(currentInterpreter);
             interpreterService.mainScript.set(scripts.get(0));
@@ -271,9 +266,9 @@ public class DebuggerMainWindowController implements Initializable {
 
     private void saveScript(File scriptFile) {
         try {
-            FileUtils.write(scriptFile, tabPane.getActiveScriptAreaTab().getScriptArea().getText(), Charset.defaultCharset());
+            FileUtils.write(scriptFile, tabPane.getSelectedScriptArea().getText(), Charset.defaultCharset());
         } catch (IOException e) {
-            showExceptionDialog("Could not save file", "blubb", "...fsfsfsf fsa", e);
+            showExceptionDialog("Could not save sourceName", "blubb", "...fsfsfsf fsa", e);
         }
     }
 
@@ -289,19 +284,18 @@ public class DebuggerMainWindowController implements Initializable {
         assert scriptFile != null;
         try {
             String code = FileUtils.readFileToString(scriptFile, Charset.defaultCharset());
-            tabPane.createNewTab(scriptFile.getAbsolutePath());
-            openScript(code, tabPane.getActiveScriptAreaTab().getScriptArea());
+            ScriptArea area = tabPane.createNewTab(scriptFile);
+            openScript(code, area);
             model.setScriptFile(scriptFile);
         } catch (IOException e) {
             showExceptionDialog("Exception occured", "",
-                    "Could not load file " + scriptFile, e);
+                    "Could not load sourceName " + scriptFile, e);
         }
     }
 
     private void openScript(String code, ScriptArea area) {
         model.setScriptFile(null);
-        if (area.textProperty().getValue() != "") {
-            System.out.println(area.textProperty().getValue());
+        if (!area.textProperty().getValue().isEmpty()) {
             area.deleteText(0, area.textProperty().getValue().length());
         }
         area.setText(code);
@@ -315,13 +309,13 @@ public class DebuggerMainWindowController implements Initializable {
         if (keyFile != null) {
             Task<Void> task = facade.loadKeyFileTask(keyFile);
             task.setOnSucceeded(event -> {
-                statusBar.publishMessage("Loaded key file: %s", keyFile);
+                statusBar.publishMessage("Loaded key sourceName: %s", keyFile);
                 model.getCurrentGoalNodes().setAll(facade.getPseudoGoals());
             });
 
             task.setOnFailed(event -> {
                 event.getSource().exceptionProperty().get();
-                showExceptionDialog("Could not load file", "Key file loading error", "",
+                showExceptionDialog("Could not load sourceName", "Key sourceName loading error", "",
                         (Throwable) event.getSource().exceptionProperty().get()
                 );
             });
@@ -353,12 +347,12 @@ public class DebuggerMainWindowController implements Initializable {
      *
      * @param title       of the dialog
      * @param description of the files
-     * @param fileEndings file that should be shown
+     * @param fileEndings sourceName that should be shown
      * @return
      */
     private File openFileChooserSaveDialog(String title, String description, String... fileEndings) {
         FileChooser fileChooser = getFileChooser(title, description, fileEndings);
-        // File file = fileChooser.showSaveDialog(inspectionViewTabPane.getInspectionViewTab().getGoalView().getScene().getWindow());
+        // File sourceName = fileChooser.showSaveDialog(inspectionViewTabPane.getInspectionViewTab().getGoalView().getScene().getWindow());
         File file = fileChooser.showOpenDialog(statusBar.getScene().getWindow());
         if (file != null) initialDirectory = file.getParentFile();
         return file;
@@ -366,7 +360,7 @@ public class DebuggerMainWindowController implements Initializable {
 
     private File openFileChooserOpenDialog(String title, String description, String... fileEndings) {
         FileChooser fileChooser = getFileChooser(title, description, fileEndings);
-        //File file = fileChooser.showOpenDialog(inspectionViewTabPane.getInspectionViewTab().getGoalView().getScene().getWindow());
+        //File sourceName = fileChooser.showOpenDialog(inspectionViewTabPane.getInspectionViewTab().getGoalView().getScene().getWindow());
         File file = fileChooser.showOpenDialog(statusBar.getScene().getWindow());
         if (file != null) initialDirectory = file.getParentFile();
         return file;

src/main/java/edu/kit/formal/gui/controls/InspectionViewTab.java

@@ -75,7 +75,7 @@ public class InspectionViewTab extends Tab {
                 setClosable(true);
             }
         });
-        mode.set(Mode.POSTMORTEM);
+
 
         showCode.addListener(o -> {
             if (showCode.get())

src/main/java/edu/kit/formal/gui/controls/ScriptAreaTab.java

-package edu.kit.formal.gui.controls;
-
-import javafx.beans.NamedArg;
-import javafx.fxml.FXML;
-import javafx.fxml.FXMLLoader;
-import javafx.scene.control.Tab;
-
-import java.io.IOException;
-import java.io.UTFDataFormatException;
-
-/**
- * Tab with a ScriptArea
- */
-public class ScriptAreaTab extends Tab {
-    @FXML
-    private ScriptArea scriptArea;
-
-    public ScriptAreaTab(@NamedArg("text") String title) {
-        super(title);
-        Utils.createWithFXML(this);
-    }
-
-    public ScriptArea getScriptArea() {
-        return scriptArea;
-    }
-}

src/main/java/edu/kit/formal/gui/controls/ScriptTabPane.java

 package edu.kit.formal.gui.controls;
 
-import com.google.common.collect.BiMap;
-import com.google.common.collect.HashBiMap;
+import edu.kit.formal.gui.model.Breakpoint;
+import edu.kit.formal.gui.model.MainScriptIdentifier;
+import javafx.beans.property.ObjectProperty;
 import javafx.beans.property.SimpleObjectProperty;
-import javafx.beans.property.SimpleStringProperty;
-import javafx.beans.property.StringProperty;
 import javafx.scene.control.Tab;
 import javafx.scene.control.TabPane;
 import org.apache.logging.log4j.LogManager;
 import org.apache.logging.log4j.Logger;
 
-import java.nio.file.Paths;
-import java.util.Iterator;
+import java.io.File;
+import java.util.HashSet;
+import java.util.Set;
 
 /**
  * Controller for TabPane
@@ -20,22 +20,10 @@ import java.util.Iterator;
  */
 public class ScriptTabPane extends TabPane {
     private static Logger logger = LogManager.getLogger(ScriptTabPane.class);
-
-    /**
-     * String is filepath; if string already exists if new tab should be created nothing happens
-     * If wished for, instead of filepath an object with more script information may be used
-     */
-    private BiMap<String, ScriptAreaTab> mappingOfTabs = HashBiMap.create();
-
-    private SimpleObjectProperty<Tab> activeTab = new SimpleObjectProperty<>();
-    private StringProperty activeScriptPath = new SimpleStringProperty();
+    private ObjectProperty<MainScriptIdentifier> mainScript = new SimpleObjectProperty<>();
 
     public ScriptTabPane() {
         Utils.createWithFXML(this);
-        activeTab.bind(this.getSelectionModel().selectedItemProperty());
-        activeTab.addListener(o -> {
-            activeScriptPath.set(mappingOfTabs.inverse().get(activeTab.get()));
-        });
     }
 
     /**
@@ -43,62 +31,51 @@ public class ScriptTabPane extends TabPane {
      *
      * @param
      */
-    public void createNewTab(String filePath) {
-        if (!mappingOfTabs.containsKey(filePath)) {
-            ScriptAreaTab newTab = new ScriptAreaTab(Paths.get(filePath).getFileName().toString());
-            mappingOfTabs.put(filePath, newTab);
-            this.getTabs().add(newTab);
-            this.getSelectionModel().select(mappingOfTabs.get(filePath));
+    public ScriptArea createNewTab(String filePath) {
+        return createNewTab(new File(filePath));
+    }
 
+    public ScriptArea createNewTab(File filePath) {
+        filePath = filePath.getAbsoluteFile();
+        if (findTabForFile(filePath) == null) {
+            Tab newTab = new Tab(filePath.getName());
+            ScriptArea area = new ScriptArea();
+            newTab.setContent(area);
+            area.mainScriptProperty().bindBidirectional(mainScript);
+            area.setFilePath(filePath);
+            this.getTabs().add(newTab);
+            return area;
         } else {
             logger.info("File already exists. Will not load it again");
-            this.getSelectionModel().select(mappingOfTabs.get(filePath));
-        }
-    }
-
-    /**
-     * Get the tab with the specified filename as title
-     *
-     * @param title
-     * @return
-     */
-    public ScriptArea getTabContent(String title) {
-        Iterator<Tab> iter = this.getTabs().iterator();
-        while (iter.hasNext()) {
-            ScriptAreaTab currentTab = (ScriptAreaTab) iter.next();
-            if (currentTab.getText().equals(title)) {
-                return currentTab.getScriptArea();
-            }
+            return findScriptAreaForFile(filePath);
         }
-        return null;
-    }
-
-    public ScriptAreaTab getActiveScriptAreaTab() {
-        return (ScriptAreaTab) activeTab.get();
-    }
-
-
-    public Tab getActiveTab() {
-        return activeTab.get();
-    }
-
-    public SimpleObjectProperty<Tab> activeTabProperty() {
-        return activeTab;
     }
 
-    public void setActiveTab(Tab activeTab) {
-        this.activeTab.set(activeTab);
+    public Set<Breakpoint> getBreakpoints() {
+        HashSet<Breakpoint> breakpoints = new HashSet<>();
+        getTabs().forEach(tab ->
+                breakpoints.addAll(((ScriptArea) tab.getContent()).getBreakpoints())
+        );
+        return breakpoints;
     }
 
-    public String getActiveScriptPath() {
-        return activeScriptPath.get();
+    public ScriptArea findScriptAreaForFile(File filePath) {
+        Tab t = findTabForFile(filePath);
+        if (t == null) return null;
+        return ((ScriptArea) t.getContent());
     }
 
-    public StringProperty activeScriptPathProperty() {
-        return activeScriptPath;
+    public Tab findTabForFile(File filePath) {
+        return getTabs().stream()
+                .filter(tab -> {
+                    File path = ((ScriptArea) tab.getContent()).getFilePath();
+                    return filePath.equals(path);
+                })
+                .findAny()
+                .orElse(null);
     }
 
-    public void setActiveScriptPath(String activeScriptPath) {
-        this.activeScriptPath.set(activeScriptPath);
+    public ScriptArea getSelectedScriptArea() {
+        return (ScriptArea) getSelectionModel().getSelectedItem().getContent();
     }
 }

src/main/java/edu/kit/formal/gui/model/Breakpoint.java

+package edu.kit.formal.gui.model;
+
+import lombok.Data;
+import lombok.EqualsAndHashCode;
+import lombok.RequiredArgsConstructor;
+import lombok.ToString;
+
+import java.io.File;
+
+/**
+ * @author Alexander Weigl
+ * @version 1 (21.06.17)
+ */
+@Data
+@RequiredArgsConstructor
+@ToString
+@EqualsAndHashCode
+public class Breakpoint {
+    private final File file;
+    private final int lineNumber;
+}

src/main/java/edu/kit/formal/gui/model/ConditionalBreakpoint.java

+package edu.kit.formal.gui.model;
+
+/**
+ * @author Alexander Weigl
+ * @version 1 (21.06.17)
+ */
+public class ConditionalBreakpoint {
+}

src/main/java/edu/kit/formal/gui/model/MainScriptIdentifier.java

+package edu.kit.formal.gui.model;
+
+import edu.kit.formal.gui.controls.ScriptArea;
+import edu.kit.formal.proofscriptparser.ast.ProofScript;
+import lombok.AllArgsConstructor;
+import lombok.Data;
+import lombok.RequiredArgsConstructor;
+import lombok.ToString;
+
+import java.util.Collection;
+import java.util.Optional;
+
+/**
+ * This class holds information to identify the main script (entry point) in a
+ * set of {@link edu.kit.formal.proofscriptparser.ast.ProofScript}s.
+ *
+ * @author Alexander Weigl
+ */
+@Data
+@RequiredArgsConstructor
+@AllArgsConstructor
+@ToString
+public class MainScriptIdentifier {
+    private String sourceName;
+    private int lineNumber;
+    private String scriptName;
+    private ScriptArea scriptArea;
+
+
+    /**
+     * Returns the main proof script identified by this instance in the given collection of {@link ProofScript}s
+     * <p>
+     * Strategy: Find by name, then by line number.
+     * Update name, if line number triggers.
+     *
+     * @param scripts
+     * @return
+     */
+    public Optional<ProofScript> find(Collection<ProofScript> scripts) {
+        Optional<ProofScript> byName = byName(scripts);
+        Optional<ProofScript> byLine = byLine(scripts);
+        ProofScript script = byName.orElseGet(() -> byLine.orElse(null));
+        if (script == null) return null;
+        lineNumber = script.getStartPosition().getLineNumber();
+        scriptName = script.getName();
+        return Optional.of(script);
+    }
+
+    public Optional<ProofScript> byLine(Collection<ProofScript> scripts) {
+        if (lineNumber < 0)
+            return Optional.empty();
+
+        return scripts.stream()
+                .filter(ps -> ps.getOrigin().equals(sourceName))
+                .filter(ps -> ps.getStartPosition().getLineNumber() == lineNumber)
+                .findFirst();
+    }
+
+    public Optional<ProofScript> byName(Collection<ProofScript> scripts) {
+        if (scriptName == null)
+            return Optional.empty();
+
+        return scripts.stream()
+                .filter(ps -> ps.getOrigin().equals(sourceName))
+                .filter(ps -> ps.getName().equals(scriptName))
+                .findFirst();
+    }
+}
\ No newline at end of file

src/main/java/edu/kit/formal/interpreter/Execute.java

@@ -74,7 +74,7 @@ public class Execute {
         options.addOption("h", "--help", false, "print help text");
         options.addOption("p", "--script-path", true, "include folder for scripts");
         options.addOption("l", "--linter", false, "run linter before execute");
-        options.addOption("s", "--script", true, "script file");
+        options.addOption("s", "--script", true, "script sourceName");
         return options;
     }
 }

src/main/java/edu/kit/formal/interpreter/HistoryListener.java

@@ -53,7 +53,7 @@ public class HistoryListener extends DefaultASTVisitor<Void> {
         int nearestFoundCaret = -1;
 
         for (int i = 0; i < queueNode.size(); i++) {
-            int currentPos = queueNode.get(i).getRuleCtx().start.getStartIndex();
+            int currentPos = queueNode.get(i).getRuleContext().start.getStartIndex();
             if (currentPos > nearestFoundCaret && currentPos <= caret) {
                 list.clear();
                 nearestFoundCaret = currentPos;

src/main/java/edu/kit/formal/interpreter/InterpreterBuilder.java

@@ -172,7 +172,7 @@ public class InterpreterBuilder {
         CommandHandler<KeyData> ignoreHandler = new CommandHandler<KeyData>() {
             @Override
             public boolean handles(CallStatement call) throws IllegalArgumentException {
-                return call.getRuleCtx().getStart().getStartIndex() < caretPosition;
+                return call.getRuleContext().getStart().getStartIndex() < caretPosition;
             }
 
             @Override

src/main/java/edu/kit/formal/interpreter/KeYProofFacade.java

@@ -80,7 +80,7 @@ public class KeYProofFacade {
     //endregion
 
     /**
-     * Build the KeYInterpreter that handles the execution of the loaded key problem file
+     * Build the KeYInterpreter that handles the execution of the loaded key problem sourceName
      *
      * @param keYFile
      * @param scriptText

src/main/java/edu/kit/formal/interpreter/funchdl/MacroCommandHandler.java

@@ -39,7 +39,7 @@ public class MacroCommandHandler implements CommandHandler {
         Parameters p = new Parameters();
         p.put(new Variable("#2"), new StringLiteral(call.getCommand()));
         CallStatement macroCall = new CallStatement("macro", p);
-        macroCall.setRuleContext(call.getRuleContext().get());
+        macroCall.setRuleContext(call.getRuleContext());
         //macro proofscript command
         interpreter.getFunctionLookup().callCommand(interpreter, call, params);
         //TODO change MacroCommand.Parameters to public

src/main/java/edu/kit/formal/proofscriptparser/ast/ASTNode.java

@@ -25,34 +25,53 @@ package edu.kit.formal.proofscriptparser.ast;
 
 import edu.kit.formal.proofscriptparser.Visitable;
 import edu.kit.formal.proofscriptparser.Visitor;
+import lombok.Getter;
 import org.antlr.v4.runtime.ParserRuleContext;
 
-import java.util.Optional;
-
 /**
  * @author Alexander Weigl
  * @version 1 (27.04.17)
  */
 public abstract class ASTNode<T extends ParserRuleContext>
         implements Visitable, Copyable<ASTNode<T>> {
+    /**
+     * The corresponding parse rule context
+     */
     protected T ruleContext;
+
+    /**
+     *
+     */
+    @Getter
     protected Position startPosition = new Position();
+
+    /**
+     *
+     */
+    @Getter
     protected Position endPosition = new Position();
 
-    public void setRuleContext(T c) {
-        startPosition = Position.from(c.getStart());
-        endPosition = Position.from(c.getStop());
-        ruleContext = c;
+    /**
+     * Returns the sourceName which defined this ast node or null
+     *
+     * @return
+     */
+    public String getOrigin() {
+        if (ruleContext != null) {
+            String src = ruleContext.getStart().getInputStream().getSourceName();
+            return src;
+        }
+        return null;
     }
 
-    public T getRuleCtx() {
+    public T getRuleContext() {
         return ruleContext;
     }
 
-    public Optional<T> getRuleContext() {
-        if (ruleContext == null)
-            return Optional.empty();
-        return Optional.of(ruleContext);
+    public void setRuleContext(T c) {
+        startPosition = Position.from(c.getStart());
+        endPosition = Position.from(c.getStop());
+        ruleContext = c;
     }
 
     public Position getStartPosition() {

src/main/java/edu/kit/formal/proofscriptparser/ast/Literal.java

@@ -54,7 +54,7 @@ public abstract class Literal extends Expression<ParserRuleContext> {
      * @return always {@link Optional#empty()}
      */
     @Override
-    public Optional<ParserRuleContext> getRuleContext() {
-        return Optional.empty();
+    public ParserRuleContext getRuleContext() {
+        return null;
     }
 }

src/main/java/edu/kit/formal/proofscriptparser/lint/LintProblem.java

@@ -89,7 +89,7 @@ public class LintProblem {
 
     public <T extends ParserRuleContext> LintProblem nodes(ASTNode<T>... nodes) {
         for (ASTNode n : nodes) {
-            ParserRuleContext ctx = n.getRuleCtx();
+            ParserRuleContext ctx = n.getRuleContext();
             if (ctx != null)
                 markTokens.add(ctx.getStart());
         }

src/main/java/edu/kit/formal/proofscriptparser/lint/checkers/EqualScriptNames.java

@@ -28,10 +28,10 @@ public class EqualScriptNames implements LintRule {
                 if (scripts.containsKey(proofScript.getName())) {
                     problems.add(LintProblem.create(ISSUE,
                             scripts.get(proofScript.getName()),
-                            proofScript.getRuleContext().get().name));
+                            proofScript.getRuleContext().name));
                 }
                 scripts.put(proofScript.getName(),
-                        proofScript.getRuleContext().get().name);
+                        proofScript.getRuleContext().name);
             }
         }
     }

src/main/resources/edu/kit/formal/gui/controls/ScriptAreaContextMenu.fxml

+<?xml version="1.0" encoding="UTF-8"?>
+
+<?import edu.kit.formal.gui.controls.*?>
+<?import javafx.scene.control.MenuItem?>
+<fx:root type="edu.kit.formal.gui.controls.ScriptArea.ScriptAreaContextMenu"
+         xmlns="http://javafx.com/javafx"
+         xmlns:fx="http://javafx.com/fxml" >
+<items>
+    <MenuItem text="show post mortem" onAction="#showPostMortem"/>
+    <MenuItem text="Set main script" onAction="#setMainScript"/>
+</items>
+
+</fx:root>

src/main/resources/edu/kit/formal/gui/controls/ScriptAreaTab.fxml

-<?xml version="1.0" encoding="UTF-8"?>
-
-<?import edu.kit.formal.gui.controls.ScriptArea?>
-<?import edu.kit.formal.gui.controls.ScriptAreaTab?>
-<fx:root xmlns:fx="http://javafx.com/fxml"
-         xmlns="http://javafx.com/javafx"
-         type="edu.kit.formal.gui.controls.ScriptAreaTab">
-    <content>
-        <ScriptArea fx:id="scriptArea"/>
-    </content>
-</fx:root>
\ No newline at end of file

src/main/resources/edu/kit/formal/gui/controls/ScriptTabPane.fxml

 <?xml version="1.0" encoding="UTF-8"?>
 
-<?import edu.kit.formal.gui.controls.ScriptAreaTab?>
 <?import edu.kit.formal.gui.controls.ScriptTabPane?>
 <fx:root xmlns:fx="http://javafx.com/fxml/1" prefHeight="100" prefWidth="250" styleClass="tab-pane"
          type="ScriptTabPane" xmlns="http://javafx.com/javafx/8.0.112">
     <!--  <VBox> -->
-    <ScriptAreaTab text="Untitled"/>
-
     <!--        <TabPane fx:id="tabPane" side="left"
                      tabClosingPolicy="SELECTED_TAB" VBox.vgrow="ALWAYS">
                 <tabs>