MDS/openide
1
0
Fork 0
mirror of https://gitflic.ru/project/openide/openide.git synced 2026-09-27 10:03:11 +07:00
Code Issues Packages Projects Releases Wiki Activity

js repl: fix layout

Browse Source
This commit is contained in:
Vladimir Krivosheev
2014-02-19 14:09:55 +01:00
parent 76637d30b9
commit 821a6c3d67
1 changed files with 47 additions and 24 deletions
Download Patch File Download Diff File Expand all files Collapse all files
platform/lang-impl/src/com/intellij/execution/console/LanguageConsoleBuilder.java
+47 -24
View File
@@ -137,27 +137,24 @@ public class LanguageConsoleBuilder {
editor.getSettings().setAdditionalLinesCount(1);
}
else if (gutterContentProvider != null) {
final ConsoleIconGutterComponent lineStartGutter = new ConsoleIconGutterComponent(editor, gutterContentProvider);
final ConsoleGutterComponent lineEndGutter = new ConsoleGutterComponent(editor, gutterContentProvider);
JLayeredPane layeredPane = new JBLayeredPane() {
@Override
public Dimension getPreferredSize() {
Dimension editorSize = getEditorComponent().getPreferredSize();
return new Dimension(lineStartGutter.getPreferredSize().width + editorSize.width, editorSize.height);
}
@Override
public Dimension getMinimumSize() {
Dimension editorSize = getEditorComponent().getMinimumSize();
return new Dimension(lineStartGutter.getPreferredSize().width + editorSize.width, editorSize.height);
}
@Override
public void doLayout() {
EditorComponentImpl editor = null;
Component lineStartGutter = null;
Component lineEndGutter = null;
for (int i = getComponentCount() - 1; i >= 0; i--) {
Component component = getComponent(i);
if (component instanceof EditorComponentImpl) {
editor = (EditorComponentImpl)component;
}
else if (getLayer(component) == JLayeredPane.DEFAULT_LAYER) {
lineStartGutter = component;
}
else {
lineEndGutter = component;
}
}
assert editor != null && lineStartGutter != null && lineEndGutter != null;
EditorComponentImpl editor = getEditorComponent();
int w = getWidth();
int h = getHeight();
Dimension lineStartGutterDimension = lineStartGutter.getPreferredSize();
@@ -168,15 +165,24 @@ public class LanguageConsoleBuilder {
Dimension lineEndGutterDimension = lineEndGutter.getPreferredSize();
lineEndGutter.setBounds(w - lineEndGutterDimension.width - editor.getEditor().getScrollPane().getVerticalScrollBar().getWidth(), 0, lineEndGutterDimension.width, h);
}
@NotNull
private EditorComponentImpl getEditorComponent() {
for (int i = getComponentCount() - 1; i >= 0; i--) {
Component component = getComponent(i);
if (component instanceof EditorComponentImpl) {
return (EditorComponentImpl)component;
}
}
throw new IllegalStateException();
}
};
ConsoleIconGutterComponent lineStartGutter = new ConsoleIconGutterComponent(editor, gutterContentProvider);
layeredPane.add(lineStartGutter, JLayeredPane.DEFAULT_LAYER);
JScrollPane scrollPane = editor.getScrollPane();
layeredPane.add(scrollPane.getViewport().getView(), JLayeredPane.DEFAULT_LAYER);
ConsoleGutterComponent lineEndGutter = new ConsoleGutterComponent(editor, gutterContentProvider);
layeredPane.add(lineEndGutter, JLayeredPane.PALETTE_LAYER);
scrollPane.setViewportView(layeredPane);
@@ -202,6 +208,7 @@ public class LanguageConsoleBuilder {
private final ConsoleGutterComponent lineEndGutter;
private boolean lineSeparatorPainterAdded;
private Runnable gutterSizeUpdater;
public GutterUpdateScheduler(@NotNull ConsoleIconGutterComponent lineStartGutter, @NotNull ConsoleGutterComponent lineEndGutter) {
this.lineStartGutter = lineStartGutter;
@@ -235,8 +242,7 @@ public class LanguageConsoleBuilder {
int startDocLine = document.getLineNumber(event.getOffset());
int endDocLine = document.getLineNumber(event.getOffset() + event.getNewLength());
if (event.getOldLength() > event.getNewLength() || startDocLine != endDocLine || StringUtil.indexOf(event.getOldFragment(), '\n') != -1) {
lineStartGutter.updateSize();
lineEndGutter.updateSize();
updateGutterSize();
}
}
else if (event.getOldLength() > 0) {
@@ -258,8 +264,25 @@ public class LanguageConsoleBuilder {
else {
addLineSeparatorPainterIfNeed();
}
lineStartGutter.updateSize();
lineEndGutter.updateSize();
updateGutterSize();
}
private void updateGutterSize() {
if (gutterSizeUpdater != null) {
return;
}
gutterSizeUpdater = new Runnable() {
@Override
public void run() {
if (!getHistoryViewer().isDisposed()) {
lineStartGutter.updateSize();
lineEndGutter.updateSize();
}
gutterSizeUpdater = null;
}
};
SwingUtilities.invokeLater(gutterSizeUpdater);
}
}