Commit d23745c6 authored by Alexander Weigl's avatar Alexander Weigl

Verbesserung an der ScriptArea

* Ctrl+Enter for formatting
* no jumping
* no exception
parent 10f6693e
Pipeline #16063 passed with stages
in 9 minutes and 50 seconds
package edu.kit.iti.formal.psdbg.gui.controls;
import com.google.common.base.Strings;
import de.jensd.fx.glyphs.materialdesignicons.MaterialDesignIcon;
import de.jensd.fx.glyphs.materialdesignicons.MaterialDesignIconView;
import edu.kit.iti.formal.psdbg.gui.controller.Events;
......@@ -14,16 +15,20 @@ import javafx.beans.InvalidationListener;
import javafx.beans.Observable;
import javafx.beans.binding.BooleanBinding;
import javafx.beans.property.*;
import javafx.beans.value.ChangeListener;
import javafx.beans.value.ObservableValue;
import javafx.collections.FXCollections;
import javafx.collections.ObservableList;
import javafx.collections.ObservableSet;
import javafx.event.ActionEvent;
import javafx.fxml.FXML;
import javafx.geometry.Bounds;
import javafx.geometry.Insets;
import javafx.geometry.Point2D;
import javafx.scene.Node;
import javafx.scene.control.*;
import javafx.scene.input.ContextMenuEvent;
import javafx.scene.input.KeyCode;
import javafx.scene.input.MouseButton;
import javafx.scene.input.MouseEvent;
import javafx.scene.layout.*;
......@@ -31,7 +36,9 @@ import javafx.scene.paint.Color;
import javafx.scene.paint.Paint;
import javafx.scene.text.Font;
import javafx.scene.text.FontPosture;
import javafx.scene.text.TextFlow;
import lombok.Data;
import lombok.Getter;
import lombok.RequiredArgsConstructor;
import org.antlr.v4.runtime.CharStream;
import org.antlr.v4.runtime.CharStreams;
......@@ -40,26 +47,33 @@ import org.antlr.v4.runtime.Token;
import org.apache.logging.log4j.LogManager;
import org.apache.logging.log4j.Logger;
import org.controlsfx.control.PopOver;
import org.fxmisc.richtext.CharacterHit;
import org.fxmisc.richtext.CodeArea;
import org.fxmisc.flowless.VirtualizedScrollPane;
import org.fxmisc.richtext.*;
import org.fxmisc.richtext.event.MouseOverTextEvent;
import org.fxmisc.richtext.model.StyleSpans;
import org.fxmisc.richtext.model.*;
import org.fxmisc.undo.UndoManager;
import org.reactfx.EventStream;
import org.reactfx.SuspendableNo;
import org.reactfx.collection.LiveList;
import org.reactfx.util.Tuple2;
import org.reactfx.value.Val;
import org.reactfx.value.Var;
import java.io.File;
import java.time.Duration;
import java.util.*;
import java.util.function.BiConsumer;
import java.util.function.Consumer;
import java.util.function.IntFunction;
import java.util.function.UnaryOperator;
import java.util.regex.Pattern;
/**
* ScriptArea is the {@link CodeArea} for writing Proof Scripts.
* <p>
* It displays the script code and allows highlighting of lines and setting of breakpoints
*/
public class ScriptArea extends CodeArea {
public class ScriptArea extends BorderPane {
public static final Logger LOGGER = LogManager.getLogger(ScriptArea.class);
public static final String EXECUTION_MARKER = "\u2316";
......@@ -84,6 +98,12 @@ public class ScriptArea extends CodeArea {
*/
private final ObjectProperty<MainScriptIdentifier> mainScript = new SimpleObjectProperty<>();
@Getter
private CodeArea codeArea = new CodeArea();
@Getter
private VirtualizedScrollPane<CodeArea> scrollPane = new VirtualizedScrollPane<>(codeArea);
private GutterFactory gutter;
private ANTLR4LexerHighlighter highlighter;
......@@ -97,33 +117,58 @@ public class ScriptArea extends CodeArea {
private Consumer<Token> onPostMortem = token -> {
};
private int getTextWithoutMarker;
public ScriptArea() {
init();
}
public static <S> Node createStyledTextNode(StyledSegment<String, S> seg, BiConsumer<? super TextExt, S> applyStyle) {
return StyledTextArea.createStyledTextNode(seg, applyStyle);
}
public static <S> Node createStyledTextNode(String text, S style, BiConsumer<? super TextExt, S> applyStyle) {
return StyledTextArea.createStyledTextNode(text, style, applyStyle);
}
private void init() {
this.setWrapText(true);
codeArea.setAutoScrollOnDragDesired(false);
codeArea.setOnKeyReleased(event -> {
if (event.isControlDown() && event.getCode() == KeyCode.ENTER)
simpleReformat();
});
setCenter(scrollPane);
scrollPane.setVbarPolicy(ScrollPane.ScrollBarPolicy.ALWAYS);
scrollPane.widthProperty().addListener((a, b, c) -> {
codeArea.setMinSize(scrollPane.getWidth(), scrollPane.getHeight());
});
scrollPane.estimatedScrollYProperty().addListener(new ChangeListener<Double>() {
@Override
public void changed(ObservableValue<? extends Double> observable, Double oldValue, Double newValue) {
System.out.println("SCROLL:" + newValue);
}
});
codeArea.setWrapText(true);
gutter = new GutterFactory();
highlighter = new ANTLR4LexerHighlighter(
(String val) -> new ScriptLanguageLexer(CharStreams.fromString(val)));
this.setParagraphGraphicFactory(gutter);
codeArea.setParagraphGraphicFactory(gutter);
getStyleClass().add("script-area");
installPopup();
// setOnMouseClicked(this::showContextMenu);
setContextMenu(contextMenu);
codeArea.setContextMenu(contextMenu);
textProperty().addListener((prop, oldValue, newValue) -> {
codeArea.textProperty().addListener((prop, oldValue, newValue) -> {
dirty.set(true);
if (newValue.isEmpty()) {
LOGGER.debug("text cleared");
} else {
updateMainScriptMarker();
updateHighlight();
highlightProblems();
highlightNonExecutionArea();
//highlightProblems();
//highlightNonExecutionArea();
}
});
......@@ -143,8 +188,8 @@ public class ScriptArea extends CodeArea {
}).subscribe(s -> setStyleSpans(0, s));*/
this.addEventHandler(MouseEvent.MOUSE_PRESSED, (MouseEvent e) -> {
CharacterHit hit = this.hit(e.getX(), e.getY());
currentMouseOver.set(this.hit(e.getX(), e.getY()));
CharacterHit hit = codeArea.hit(e.getX(), e.getY());
currentMouseOver.set(codeArea.hit(e.getX(), e.getY()));
int characterPosition = hit.getInsertionIndex();
//System.out.println("characterPosition = " + characterPosition);
// move the caret to that character's position
......@@ -156,7 +201,7 @@ public class ScriptArea extends CodeArea {
private void installPopup() {
javafx.stage.Popup popup = new javafx.stage.Popup();
setMouseOverTextDelay(Duration.ofSeconds(1));
codeArea.setMouseOverTextDelay(Duration.ofSeconds(1));
addEventHandler(MouseOverTextEvent.MOUSE_OVER_TEXT_BEGIN, e -> {
int chIdx = e.getCharacterIndex();
popup.getContent().setAll(
......@@ -181,7 +226,7 @@ public class ScriptArea extends CodeArea {
if (ms != null && filePath.get().getAbsolutePath().equals(ms.getSourceName())) {
System.out.println(ms);
CharStream stream = CharStreams.fromString(getText(), filePath.get().getAbsolutePath());
CharStream stream = CharStreams.fromString(codeArea.getText(), filePath.get().getAbsolutePath());
Optional<ProofScript> ps = ms.find(Facade.getAST(stream));
if (ps.isPresent()) {
......@@ -195,25 +240,65 @@ public class ScriptArea extends CodeArea {
}
private void updateHighlight() {
String newValue = getText();
String newValue = codeArea.getText();
if (newValue.length() != 0) {
clearStyle(0, newValue.length());
//weigl: resets the text position
StyleSpans<? extends Collection<String>> spans = highlighter.highlight(newValue);
double x = scrollPane.getEstimatedScrollX();
double y = scrollPane.getEstimatedScrollY();
//codeArea.clearStyle(0, newValue.length());
if (spans != null) setStyleSpans(0, spans);
StyleSpans<? extends Collection<String>> spans = highlighter.highlight(newValue);
if (spans != null) codeArea.setStyleSpans(0, spans);
markedRegions.forEach(reg -> {
Collection<String> list = new HashSet<>();
list.add(reg.clazzName);
try {
setStyle(reg.start, reg.stop, list);
codeArea.setStyle(reg.start, reg.stop, list);
} catch (IndexOutOfBoundsException e) {
//weigl silently ignore
}
});
scrollPane.estimatedScrollXProperty().setValue(x);
scrollPane.estimatedScrollYProperty().setValue(y);
codeArea.estimatedScrollYProperty().setValue(y);
//System.out.println(y + ":" + scrollPane.estimatedScrollYProperty().getValue());
}
}
private void simpleReformat() {
Pattern spacesAtLineEnd = Pattern.compile("[\t ]+\n", Pattern.MULTILINE);
String text = getText();
text = spacesAtLineEnd.matcher(text).replaceAll("\n");
ScriptLanguageLexer lexer = new ScriptLanguageLexer(CharStreams.fromString(text));
int nested = 0;
StringBuilder builder = new StringBuilder();
List<? extends Token> tokens = lexer.getAllTokens();
for (int i = 0; i < tokens.size(); i++) {
Token tok = tokens.get(i);
if (tok.getType() == ScriptLanguageLexer.INDENT)
nested++;
if (i + 1 < tokens.size() &&
tokens.get(i + 1).getType() == ScriptLanguageLexer.DEDENT)
nested--;
if (tok.getType() == ScriptLanguageLexer.WS && tok.getText().startsWith("\n")) {
builder.append(
tok.getText().replaceAll("\n[ \t]*",
"\n" + Strings.repeat(" ", nested * 4)));
} else {
builder.append(tok.getText());
}
}
int pos = getCaretPosition();
setText(builder.toString());
moveTo(pos);
}
private void highlightProblems() {
......@@ -224,7 +309,7 @@ public class ScriptArea extends CodeArea {
for (Token tok : p.getMarkTokens()) {
Set<String> problem = new HashSet<>();
problem.add("problem");
setStyle(tok.getStartIndex(),
codeArea.setStyle(tok.getStartIndex(),
tok.getStopIndex() + 1, problem);
}
}
......@@ -248,7 +333,7 @@ public class ScriptArea extends CodeArea {
}
};
setStyleSpans(0, getStyleSpans(0, getExecutionMarkerPosition()).mapStyles(styleMapper));
codeArea.setStyleSpans(0, codeArea.getStyleSpans(0, getExecutionMarkerPosition()).mapStyles(styleMapper));
//this results in a NotSupportedOperation Exception because the add to an immutable list is not allowed
......@@ -411,17 +496,11 @@ public class ScriptArea extends CodeArea {
return dirty;
}
public void removeExecutionMarker() {
setText(getTextWithoutMarker());
//Events.unregister(this);
}
public void setText(String text) {
clear();
insertText(0, text);
}
private String getTextWithoutMarker() {
return getText().replace("" + EXECUTION_MARKER, "");
}
......@@ -438,12 +517,895 @@ public class ScriptArea extends CodeArea {
setText(text.substring(0, pos) + EXECUTION_MARKER + text.substring(pos));
}
public CodePointCharStream getStream() {
return CharStreams.fromString(getText(), getFilePath().getAbsolutePath());
}
public String getText() {
return codeArea.getText();
}
public void setText(String text) {
codeArea.clear();
codeArea.insertText(0, text);
}
public void insertText(int index, String s) {
codeArea.insertText(index, s);
}
public ObservableValue<String> textProperty() {
return codeArea.textProperty();
}
public void deleteText(int i, int length) {
codeArea.deleteText(i, length);
}
public void setStyleClass(int from, int to, String styleClass) {
getCodeArea().setStyleClass(from, to, styleClass);
}
public BooleanProperty editableProperty() {
return getCodeArea().editableProperty();
}
public BooleanProperty wrapTextProperty() {
return getCodeArea().wrapTextProperty();
}
public UndoManager getUndoManager() {
return getCodeArea().getUndoManager();
}
public void setUndoManager(UndoManager undoManager) {
getCodeArea().setUndoManager(undoManager);
}
public ObjectProperty<Duration> mouseOverTextDelayProperty() {
return getCodeArea().mouseOverTextDelayProperty();
}
public ObjectProperty<IntFunction<? extends Node>> paragraphGraphicFactoryProperty() {
return getCodeArea().paragraphGraphicFactoryProperty();
}
public ObjectProperty<ContextMenu> contextMenuObjectProperty() {
return getCodeArea().contextMenuObjectProperty();
}
public DoubleProperty contextMenuXOffsetProperty() {
return getCodeArea().contextMenuXOffsetProperty();
}
public DoubleProperty contextMenuYOffsetProperty() {
return getCodeArea().contextMenuYOffsetProperty();
}
public BooleanProperty useInitialStyleForInsertionProperty() {
return getCodeArea().useInitialStyleForInsertionProperty();
}
public void setStyleCodecs(Codec<Collection<String>> paragraphStyleCodec, Codec<StyledSegment<String, Collection<String>>> styledSegCodec) {
getCodeArea().setStyleCodecs(paragraphStyleCodec, styledSegCodec);
}
public Optional<Tuple2<Codec<Collection<String>>, Codec<StyledSegment<String, Collection<String>>>>> getStyleCodecs() {
return getCodeArea().getStyleCodecs();
}
public Var<Double> estimatedScrollXProperty() {
return getCodeArea().estimatedScrollXProperty();
}
public Var<Double> estimatedScrollYProperty() {
return getCodeArea().estimatedScrollYProperty();
}
public ObjectProperty<Consumer<MouseEvent>> onOutsideSelectionMousePressProperty() {
return getCodeArea().onOutsideSelectionMousePressProperty();
}
public ObjectProperty<Consumer<MouseEvent>> onInsideSelectionMousePressReleaseProperty() {
return getCodeArea().onInsideSelectionMousePressReleaseProperty();
}
public ObjectProperty<Consumer<Point2D>> onNewSelectionDragProperty() {
return getCodeArea().onNewSelectionDragProperty();
}
public ObjectProperty<Consumer<MouseEvent>> onNewSelectionDragEndProperty() {
return getCodeArea().onNewSelectionDragEndProperty();
}
public ObjectProperty<Consumer<Point2D>> onSelectionDragProperty() {
return getCodeArea().onSelectionDragProperty();
}
public ObjectProperty<Consumer<MouseEvent>> onSelectionDropProperty() {
return getCodeArea().onSelectionDropProperty();
}
public BooleanProperty autoScrollOnDragDesiredProperty() {
return getCodeArea().autoScrollOnDragDesiredProperty();
}
public StyledDocument<Collection<String>, String, Collection<String>> getDocument() {
return getCodeArea().getDocument();
}
public CaretSelectionBind<Collection<String>, String, Collection<String>> getCaretSelectionBind() {
return getCodeArea().getCaretSelectionBind();
}
public ObservableValue<Integer> lengthProperty() {
return getCodeArea().lengthProperty();
}
public LiveList<Paragraph<Collection<String>, String, Collection<String>>> getParagraphs() {
return getCodeArea().getParagraphs();
}
public LiveList<Paragraph<Collection<String>, String, Collection<String>>> getVisibleParagraphs() {
return getCodeArea().getVisibleParagraphs();
}
public SuspendableNo beingUpdatedProperty() {
return getCodeArea().beingUpdatedProperty();
}
public Val<Double> totalWidthEstimateProperty() {
return getCodeArea().totalWidthEstimateProperty();
}
public Val<Double> totalHeightEstimateProperty() {
return getCodeArea().totalHeightEstimateProperty();
}
public EventStream<PlainTextChange> plainTextChanges() {
return getCodeArea().plainTextChanges();
}
public EventStream<RichTextChange<Collection<String>, String, Collection<String>>> richChanges() {
return getCodeArea().richChanges();
}
public EventStream<?> viewportDirtyEvents() {
return getCodeArea().viewportDirtyEvents();
}
public EditableStyledDocument<Collection<String>, String, Collection<String>> getContent() {
return getCodeArea().getContent();
}
public Collection<String> getInitialTextStyle() {
return getCodeArea().getInitialTextStyle();
}
public Collection<String> getInitialParagraphStyle() {
return getCodeArea().getInitialParagraphStyle();
}
public BiConsumer<TextFlow, Collection<String>> getApplyParagraphStyle() {
return getCodeArea().getApplyParagraphStyle();
}
public boolean isPreserveStyle() {
return getCodeArea().isPreserveStyle();
}
public SegmentOps<String, Collection<String>> getSegOps() {
return getCodeArea().getSegOps();
}
public double getViewportHeight() {
return getCodeArea().getViewportHeight();
}
public Optional<Integer> allParToVisibleParIndex(int allParIndex) {
return getCodeArea().allParToVisibleParIndex(allParIndex);
}
public int visibleParToAllParIndex(int visibleParIndex) {
return getCodeArea().visibleParToAllParIndex(visibleParIndex);
}
public CharacterHit hit(double x, double y) {
return getCodeArea().hit(x, y);
}
public int lineIndex(int paragraphIndex, int columnPosition) {
return getCodeArea().lineIndex(paragraphIndex, columnPosition);
}
public int getParagraphLinesCount(int paragraphIndex) {
return getCodeArea().getParagraphLinesCount(paragraphIndex);
}
public Optional<Bounds> getCharacterBoundsOnScreen(int from, int to) {
return getCodeArea().getCharacterBoundsOnScreen(from, to);
}
public String getText(int start, int end) {
return getCodeArea().getText(start, end);
}
public String getText(int paragraph) {
return getCodeArea().getText(paragraph);
}
public String getText(IndexRange range) {
return getCodeArea().getText(range);
}
public StyledDocument<Collection<String>, String, Collection<String>> subDocument(int start, int end) {
return getCodeArea().subDocument(start, end);
}
public StyledDocument<Collection<String>, String, Collection<String>> subDocument(int paragraphIndex) {
return getCodeArea().subDocument(paragraphIndex);
}
public IndexRange getParagraphSelection(Selection selection, int paragraph) {
return getCodeArea().getParagraphSelection(selection, paragraph);
}
public Collection<String> getStyleOfChar(int index) {
return getCodeArea().getStyleOfChar(index);
}
public Collection<String> getStyleAtPosition(int position) {
return getCodeArea().getStyleAtPosition(position);
}
public IndexRange getStyleRangeAtPosition(int position) {
return getCodeArea().getStyleRangeAtPosition(position);
}
public StyleSpans<Collection<String>> getStyleSpans(int from, int to) {
return getCodeArea().getStyleSpans(from, to);
}
public Collection<String> getStyleOfChar(int paragraph, int index) {
return getCodeArea().getStyleOfChar(paragraph, index);
}
public Collection<String> getStyleAtPosition(int paragraph, int position) {
return getCodeArea().getStyleAtPosition(paragraph, position);
}
public IndexRange getStyleRangeAtPosition(int paragraph, int position) {
return getCodeArea().getStyleRangeAtPosition(paragraph, position);
}
public StyleSpans<Collection<String>> getStyleSpans(int paragraph) {
return getCodeArea().getStyleSpans(paragraph);
}
public StyleSpans<Collection<String>> getStyleSpans(int paragraph, int from, int to) {
return getCodeArea().getStyleSpans(paragraph, from, to);
}
public int getAbsolutePosition(int paragraphIndex, int columnIndex) {
return getCodeArea().getAbsolutePosition(paragraphIndex, columnIndex);
}
public TwoDimensional.Position position(int row, int col) {
return getCodeArea().position(row, col);
}
public TwoDimensional.Position offsetToPosition(int charOffset, TwoDimensional.Bias bias) {
return getCodeArea().offsetToPosition(charOffset, bias);
}
public Bounds getVisibleParagraphBoundsOnScreen(int visibleParagraphIndex) {
return getCodeArea().getVisibleParagraphBoundsOnScreen(visibleParagraphIndex);
}
public Optional<Bounds> getParagraphBoundsOnScreen(int paragraphIndex) {
return getCodeArea().getParagraphBoundsOnScreen(paragraphIndex);
}
public Optional<Bounds> getCaretBoundsOnScreen(int paragraphIndex) {
return getCodeArea().getCaretBoundsOnScreen(paragraphIndex);
}
public void scrollXToPixel(double pixel) {
getCodeArea().scrollXToPixel(pixel);
}
public void scrollYToPixel(double pixel) {
getCodeArea().scrollYToPixel(pixel);
}
public void scrollXBy(double deltaX) {
getCodeArea().scrollXBy(deltaX);
}
public void scrollYBy(double deltaY) {
getCodeArea().scrollYBy(deltaY);
}
public void scrollBy(Point2D deltas) {
getCodeArea().scrollBy(deltas);
}
public void showParagraphInViewport(int paragraphIndex) {
getCodeArea().showParagraphInViewport(paragraphIndex);
}
public void showParagraphAtTop(int paragraphIndex) {
getCodeArea().showParagraphAtTop(paragraphIndex);
}
public void showParagraphAtBottom(int paragraphIndex) {
getCodeArea().showParagraphAtBottom(paragraphIndex);
}
public void showParagraphRegion(int paragraphIndex, Bounds region) {
getCodeArea().showParagraphRegion(paragraphIndex, region);
}
public void requestFollowCaret() {
getCodeArea().requestFollowCaret();
}
public void lineStart(NavigationActions.SelectionPolicy policy) {
getCodeArea().lineStart(policy);
}
public void lineEnd(NavigationActions.SelectionPolicy policy) {
getCodeArea().lineEnd(policy);
}
public void prevPage(NavigationActions.SelectionPolicy selectionPolicy) {
getCodeArea().prevPage(selectionPolicy);
}
public void nextPage(NavigationActions.SelectionPolicy selectionPolicy) {
getCodeArea().nextPage(selectionPolicy);
}
public void displaceCaret(int pos) {
getCodeArea().displaceCaret(pos);
}
public void setStyle(int from, int to, Collection<String> style) {
getCodeArea().setStyle(from, to, style);
}
public void setStyle(int paragraph, Collection<String> style) {
getCodeArea().setStyle(paragraph, style);
}
public void setStyle(int paragraph, int from, int to, Collection<String> style) {
getCodeArea().setStyle(paragraph, from, to, style);
}
public void setStyleSpans(int from, StyleSpans<? extends Collection<String>> styleSpans) {
getCodeArea().setStyleSpans(from, styleSpans);
}
public void setStyleSpans(int paragraph, int from, StyleSpans<? extends Collection<String>> styleSpans) {
getCodeArea().setStyleSpans(paragraph, from, styleSpans);
}
public void setParagraphStyle(int paragraph, Collection<String> paragraphStyle) {
getCodeArea().setParagraphStyle(paragraph, paragraphStyle);
}
public Collection<String> getTextStyleForInsertionAt(int pos) {
return getCodeArea().getTextStyleForInsertionAt(pos);
}
public Collection<String> getParagraphStyleForInsertionAt(int pos) {
return getCodeArea().getParagraphStyleForInsertionAt(pos);
}
public void replaceText(int start, int end, String text) {
getCodeArea().replaceText(start, end, text);
}