TheCloud/Digital
1
0
Fork 0
mirror of https://github.com/hneemann/Digital.git synced 2025-09-26 06:22:48 -04:00
Code Issues Packages Projects Releases Wiki Activity

fixed some missed font size issues

Browse Source
This commit is contained in:
helmut.neemann 2017-05-10 12:12:37 +02:00
parent 535763aa12
commit 2880b37d4d
2 changed files with 7 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
src/main/java/de/neemann/digital/gui/components/ElementHelpDialog.java
View File

@ -8,6 +8,7 @@ import de.neemann.digital.draw.library.ElementLibrary;
import de.neemann.digital.draw.shapes.ShapeFactory;
import de.neemann.digital.lang.Lang;
import de.neemann.gui.ErrorMessage;
import de.neemann.gui.Screen;
import de.neemann.gui.ToolTipAction;
import javax.imageio.ImageIO;
@ -99,6 +100,7 @@ public class ElementHelpDialog extends JDialog {
JEditorPane editorPane = new JEditorPane("text/html", description);
editorPane.setEditable(false);
editorPane.setCaretPosition(0);
editorPane.putClientProperty(JEditorPane.HONOR_DISPLAY_PROPERTIES, true);
editorPane.addHyperlinkListener(hyperlinkEvent -> {
if (HyperlinkEvent.EventType.ACTIVATED == hyperlinkEvent.getEventType()) {
@ -124,7 +126,7 @@ public class ElementHelpDialog extends JDialog {
Dimension r = getSize();
if (r.width > MAX_WIDTH) r.width = MAX_WIDTH;
if (r.height > MAX_HEIGHT) r.height = MAX_HEIGHT;
setSize(r);
setSize(Screen.getInstance().scale(r));
setLocationRelativeTo(parent);
}

5
src/main/java/de/neemann/digital/gui/components/table/ShowStringDialog.java
View File

@ -1,5 +1,7 @@
package de.neemann.digital.gui.components.table;
import de.neemann.gui.Screen;
import javax.swing.*;
import javax.swing.text.JTextComponent;
import java.awt.*;
@ -54,7 +56,8 @@ public class ShowStringDialog extends JDialog {
if (html) {
textComp = new JEditorPane("text/html", str);
textComp.setCaretPosition(0);
textComp.setPreferredSize(new Dimension(600, 800));
textComp.putClientProperty(JEditorPane.HONOR_DISPLAY_PROPERTIES, true);
textComp.setPreferredSize(Screen.getInstance().scale(new Dimension(600, 800)));
} else {
textComp = new JTextArea(str);
textComp.setFont(new JLabel().getFont());