88 - Font.PLAIN, font1.getSize()); |
88 - Font.PLAIN, font1.getSize()); |
89 + Font font2 = new Font("Isabelle DejaVu Sans Mono", Font.PLAIN, font1.getSize()); |
89 + Font font2 = new Font("Isabelle DejaVu Sans Mono", Font.PLAIN, font1.getSize()); |
90 FontRenderContext frc = new FontRenderContext(null, true, false); |
90 FontRenderContext frc = new FontRenderContext(null, true, false); |
91 float scale = |
91 float scale = |
92 font1.getLineMetrics("", frc).getHeight() / font2.getLineMetrics("", frc).getHeight(); |
92 font1.getLineMetrics("", frc).getHeight() / font2.getLineMetrics("", frc).getHeight(); |
93 @@ -1107,6 +1124,22 @@ |
93 @@ -1107,6 +1124,48 @@ |
94 |
94 |
95 //{{{ Colors and styles |
95 //{{{ Colors and styles |
96 |
96 |
97 + public static Color menuAcceleratorForeground(boolean selection) { |
97 + public static Color menuAcceleratorForeground(boolean selection) { |
98 + Color color = |
98 + Color color = |
99 + UIManager.getColor(selection ? |
99 + UIManager.getColor(selection ? |
100 + "MenuItem.acceleratorSelectionForeground" : |
100 + "MenuItem.acceleratorSelectionForeground" : |
101 + "MenuItem.acceleratorForeground"); |
101 + "MenuItem.acceleratorForeground"); |
102 + |
102 + |
103 + if (color == null) color = Color.black; |
103 + if (color == null) color = defaultFgColor(); |
104 + |
104 + |
105 + return color; |
105 + return color; |
106 + } |
106 + } |
107 + |
107 + |
108 + public static boolean isDarkLaf() |
108 + public static boolean isDarkLaf() |
109 + { |
109 + { |
110 + return com.formdev.flatlaf.FlatLaf.isLafDark(); |
110 + return com.formdev.flatlaf.FlatLaf.isLafDark(); |
|
111 + } |
|
112 + |
|
113 + public static Color defaultBgColor() |
|
114 + { |
|
115 + return isDarkLaf() ? Color.BLACK : Color.WHITE; |
|
116 + } |
|
117 + |
|
118 + public static Color defaultFgColor() |
|
119 + { |
|
120 + return isDarkLaf() ? Color.WHITE : Color.BLACK; |
|
121 + } |
|
122 + |
|
123 + public static String getTheme() |
|
124 + { |
|
125 + return isDarkLaf() ? "dark" : ""; |
|
126 + } |
|
127 + |
|
128 + public static String getThemeSuffix() |
|
129 + { |
|
130 + return getThemeSuffix("."); |
|
131 + } |
|
132 + |
|
133 + public static String getThemeSuffix(String s) |
|
134 + { |
|
135 + String t = getTheme(); |
|
136 + return t.isEmpty() ? t : s + t; |
111 + } |
137 + } |
112 + |
138 + |
113 //{{{ getStyleString() method |
139 //{{{ getStyleString() method |
114 /** |
140 /** |
115 * Converts a style into it's string representation. |
141 * Converts a style into it's string representation. |
116 @@ -1619,6 +1652,21 @@ |
142 @@ -1407,8 +1466,8 @@ |
|
143 { |
|
144 for (Component child: win.getComponents()) |
|
145 { |
|
146 - child.setBackground(jEdit.getColorProperty("view.bgColor", Color.WHITE)); |
|
147 - child.setForeground(jEdit.getColorProperty("view.fgColor", Color.BLACK)); |
|
148 + child.setBackground(jEdit.getColorProperty("view.bgColor", defaultBgColor())); |
|
149 + child.setForeground(jEdit.getColorProperty("view.fgColor")); |
|
150 if (child instanceof JTextPane) |
|
151 ((JTextPane)child).setUI(new javax.swing.plaf.basic.BasicEditorPaneUI()); |
|
152 if (child instanceof Container) |
|
153 @@ -1619,6 +1678,21 @@ |
117 } |
154 } |
118 //}}} |
155 //}}} |
119 |
156 |
120 + //{{{ isPopupTrigger() method |
157 + //{{{ isPopupTrigger() method |
121 + /** |
158 + /** |
713 - GUIUtilities.loadIcon("Clear.png")); |
760 - GUIUtilities.loadIcon("Clear.png")); |
714 + GUIUtilities.loadIcon(jEdit.getProperty("common.clearAll.icon"))); |
761 + GUIUtilities.loadIcon(jEdit.getProperty("common.clearAll.icon"))); |
715 clearRegister.setToolTipText(GenericGUIUtilities.prettifyMenuLabel( |
762 clearRegister.setToolTipText(GenericGUIUtilities.prettifyMenuLabel( |
716 jEdit.getProperty("clear-string-register.label"))); |
763 jEdit.getProperty("clear-string-register.label"))); |
717 clearRegister.addActionListener(e -> clearSelectedIndex()); |
764 clearRegister.addActionListener(e -> clearSelectedIndex()); |
|
765 diff -ru jedit5.7.0/jEdit/org/gjt/sp/jedit/jEdit.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/jEdit.java |
|
766 --- jedit5.7.0/jEdit/org/gjt/sp/jedit/jEdit.java 2024-08-03 19:53:14.000000000 +0200 |
|
767 +++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/jEdit.java 2025-05-15 21:20:18.075698848 +0200 |
|
768 @@ -674,6 +674,12 @@ |
|
769 return value; |
|
770 } //}}} |
|
771 |
|
772 + public static String getThemeProperty(String name) |
|
773 + { |
|
774 + String s = GUIUtilities.getThemeSuffix(); |
|
775 + return s.isEmpty() ? getProperty(name) : getProperty(name + s, getProperty(name)); |
|
776 + } |
|
777 + |
|
778 //{{{ getProperty() method |
|
779 /** |
|
780 * Returns the property with the specified name.<p> |
|
781 @@ -859,7 +865,7 @@ |
|
782 */ |
|
783 public static Color getColorProperty(String name) |
|
784 { |
|
785 - return getColorProperty(name,Color.black); |
|
786 + return getColorProperty(name, GUIUtilities.defaultFgColor()); |
|
787 } |
|
788 |
|
789 /** |
|
790 @@ -870,7 +876,7 @@ |
|
791 */ |
|
792 public static Color getColorProperty(String name, Color def) |
|
793 { |
|
794 - String value = getProperty(name); |
|
795 + String value = getThemeProperty(name); |
|
796 if(value == null) |
|
797 return def; |
|
798 else |
|
799 @@ -886,7 +892,7 @@ |
|
800 */ |
|
801 public static void setColorProperty(String name, Color value) |
|
802 { |
|
803 - setProperty(name, SyntaxUtilities.getColorHexString(value)); |
|
804 + setThemeProperty(name, SyntaxUtilities.getColorHexString(value)); |
|
805 } //}}} |
|
806 |
|
807 //{{{ getColorMatrixProperty() method |
|
808 @@ -936,6 +942,11 @@ |
|
809 public static void setProperty(String name, String value) |
|
810 { |
|
811 propMgr.setProperty(name,value); |
|
812 + } |
|
813 + |
|
814 + public static void setThemeProperty(String name, String value) |
|
815 + { |
|
816 + setProperty(name + GUIUtilities.getThemeSuffix(), value); |
|
817 } //}}} |
|
818 |
|
819 //{{{ setTemporaryProperty() method |
|
820 @@ -4233,7 +4244,7 @@ |
|
821 } //}}} |
|
822 |
|
823 //{{{ gotoMarker() method |
|
824 - private static void gotoMarker(final View view, final Buffer buffer, |
|
825 + public static void gotoMarker(final View view, final Buffer buffer, |
|
826 final String marker) |
|
827 { |
|
828 AwtRunnableQueue.INSTANCE.runAfterIoTasks(new Runnable() |
|
829 diff -ru jedit5.7.0/jEdit/org/gjt/sp/jedit/gui/BufferSwitcher.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/gui/BufferSwitcher.java |
|
830 --- jedit5.7.0/jEdit/org/gjt/sp/jedit/gui/BufferSwitcher.java 2024-08-03 19:53:16.000000000 +0200 |
|
831 +++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/gui/BufferSwitcher.java 2025-05-13 16:29:14.196283445 +0200 |
|
832 @@ -58,7 +58,7 @@ |
|
833 public static final DataFlavor BufferDataFlavor = new DataFlavor(BufferTransferableData.class, DataFlavor.javaJVMLocalObjectMimeType); |
|
834 |
|
835 // actual colors will be set in constructor, here are just fallback values |
|
836 - static Color defaultColor = Color.BLACK; |
|
837 + static Color defaultColor = GUIUtilities.defaultFgColor(); |
|
838 static Color defaultBGColor = Color.LIGHT_GRAY; |
|
839 |
|
840 public BufferSwitcher(final EditPane editPane) |
|
841 diff -ru jedit5.7.0/jEdit/org/gjt/sp/jedit/gui/LogViewer.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/gui/LogViewer.java |
|
842 --- jedit5.7.0/jEdit/org/gjt/sp/jedit/gui/LogViewer.java 2024-08-03 19:53:16.000000000 +0200 |
|
843 +++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/gui/LogViewer.java 2025-05-14 11:05:39.544481221 +0200 |
|
844 @@ -413,7 +413,7 @@ |
|
845 { |
|
846 this.list = list; |
|
847 debugColor = jEdit.getColorProperty("log-viewer.message.debug.color", Color.BLUE); |
|
848 - messageColor = jEdit.getColorProperty("log-viewer.message.message.color", Color.BLACK); |
|
849 + messageColor = jEdit.getColorProperty("log-viewer.message.message.color"); |
|
850 noticeColor = jEdit.getColorProperty("log-viewer.message.notice.color", Color.GREEN); |
|
851 warningColor = jEdit.getColorProperty("log-viewer.message.warning.color", Color.ORANGE); |
|
852 errorColor = jEdit.getColorProperty("log-viewer.message.error.color", Color.RED); |
|
853 diff -ru /home/makarius/.isabelle/contrib/jedit-20250424/jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/io/VFS.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/io/VFS.java |
|
854 --- /home/makarius/.isabelle/contrib/jedit-20250424/jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/io/VFS.java 2024-08-03 19:53:14.000000000 +0200 |
|
855 +++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/io/VFS.java 2025-05-14 10:51:16.530755624 +0200 |
|
856 @@ -1302,8 +1302,7 @@ |
|
857 colors.add(new ColorEntry( |
|
858 Pattern.compile(StandardUtilities.globToRE(glob)), |
|
859 jEdit.getColorProperty( |
|
860 - "vfs.browser.colors." + i + ".color", |
|
861 - Color.black))); |
|
862 + "vfs.browser.colors." + i + ".color"))); |
|
863 } |
|
864 catch(PatternSyntaxException e) |
|
865 { |
|
866 diff -ru jedit5.7.0/jEdit/org/gjt/sp/util/SyntaxUtilities.java jedit5.7.0-patched/jEdit/org/gjt/sp/util/SyntaxUtilities.java |
|
867 --- jedit5.7.0/jEdit/org/gjt/sp/util/SyntaxUtilities.java 2024-08-03 19:53:21.000000000 +0200 |
|
868 +++ jedit5.7.0-patched/jEdit/org/gjt/sp/util/SyntaxUtilities.java 2025-05-14 15:20:40.515623017 +0200 |
|
869 @@ -35,6 +35,7 @@ |
|
870 import org.gjt.sp.jedit.syntax.SyntaxStyle; |
|
871 import org.gjt.sp.jedit.syntax.Token; |
|
872 import org.gjt.sp.jedit.IPropertyManager; |
|
873 +import org.gjt.sp.jedit.GUIUtilities; |
|
874 |
|
875 import static java.util.stream.Collectors.joining; |
|
876 //}}} |
|
877 @@ -49,6 +50,15 @@ |
|
878 public class SyntaxUtilities |
|
879 { |
|
880 public static IPropertyManager propertyManager; |
|
881 + |
|
882 + public static String getThemeProperty(String name) |
|
883 + { |
|
884 + String s = GUIUtilities.getThemeSuffix(); |
|
885 + String a = propertyManager.getProperty(name); |
|
886 + String b = propertyManager.getProperty(name + s); |
|
887 + return b == null ? a : b; |
|
888 + } |
|
889 + |
|
890 private static final Pattern COLOR_MATRIX_PATTERN = Pattern.compile("(?x)\n" + |
|
891 "^\n" + |
|
892 "\\s*+ # optionally preceded by whitespace\n" + |
|
893 @@ -125,7 +135,7 @@ |
|
894 */ |
|
895 public static Color parseColor(String name) |
|
896 { |
|
897 - return parseColor(name, Color.black); |
|
898 + return parseColor(name, GUIUtilities.defaultFgColor()); |
|
899 } //}}} |
|
900 |
|
901 //{{{ parseColor() method |
|
902 @@ -267,7 +277,7 @@ |
|
903 if(s.startsWith("color:")) |
|
904 { |
|
905 if(color) |
|
906 - fgColor = parseColor(s.substring(6), Color.black); |
|
907 + fgColor = parseColor(s.substring(6), GUIUtilities.defaultFgColor()); |
|
908 } |
|
909 else if(s.startsWith("bgColor:")) |
|
910 { |
|
911 @@ -311,7 +321,7 @@ |
|
912 boolean color) |
|
913 throws IllegalArgumentException |
|
914 { |
|
915 - return parseStyle(str, family, size, color, Color.black); |
|
916 + return parseStyle(str, family, size, color, GUIUtilities.defaultFgColor()); |
|
917 } //}}} |
|
918 |
|
919 //{{{ loadStyles() methods |
|
920 @@ -347,9 +357,7 @@ |
|
921 String styleName = "view.style." |
|
922 + Token.tokenToString((byte)i) |
|
923 .toLowerCase(Locale.ENGLISH); |
|
924 - styles[i] = parseStyle( |
|
925 - propertyManager.getProperty(styleName), |
|
926 - family,size,color); |
|
927 + styles[i] = parseStyle(getThemeProperty(styleName),family,size,color); |
|
928 } |
|
929 catch(Exception e) |
|
930 { |
|
931 @@ -357,8 +365,28 @@ |
|
932 } |
|
933 } |
|
934 |
|
935 - return styles; |
|
936 + styles[0] = |
|
937 + new SyntaxStyle(org.gjt.sp.jedit.jEdit.getColorProperty("view.fgColor", GUIUtilities.defaultFgColor()), |
|
938 + null, new Font(family, 0, size)); |
|
939 + return _styleExtender.extendStyles(styles); |
|
940 } //}}} |
|
941 |
|
942 + /** |
|
943 + * Extended styles derived from the user-specified style array. |
|
944 + */ |
|
945 + |
|
946 + public static class StyleExtender |
|
947 + { |
|
948 + public SyntaxStyle[] extendStyles(SyntaxStyle[] styles) |
|
949 + { |
|
950 + return styles; |
|
951 + } |
|
952 + } |
|
953 + volatile private static StyleExtender _styleExtender = new StyleExtender(); |
|
954 + public static void setStyleExtender(StyleExtender ext) |
|
955 + { |
|
956 + _styleExtender = ext; |
|
957 + } |
|
958 + |
|
959 private SyntaxUtilities(){} |
|
960 } |
|
961 diff -ru jedit5.7.0/jEdit/org/gjt/sp/jedit/EditPane.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/EditPane.java |
|
962 --- jedit5.7.0/jEdit/org/gjt/sp/jedit/EditPane.java 2024-08-03 19:53:15.000000000 +0200 |
|
963 +++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/EditPane.java 2025-05-14 15:46:36.934878462 +0200 |
|
964 @@ -43,6 +43,7 @@ |
|
965 import org.gjt.sp.jedit.msg.BufferChanging; |
|
966 import org.gjt.sp.jedit.msg.BufferUpdate; |
|
967 import org.gjt.sp.jedit.msg.EditPaneUpdate; |
|
968 +import org.gjt.sp.jedit.msg.PositionChanging; |
|
969 import org.gjt.sp.jedit.msg.PropertiesChanged; |
|
970 import org.gjt.sp.jedit.options.GeneralOptionPane; |
|
971 import org.gjt.sp.jedit.options.GutterOptionPane; |
|
972 @@ -380,9 +381,11 @@ |
|
973 buffer.unsetProperty(Buffer.CARET_POSITIONED); |
|
974 |
|
975 |
|
976 - if(caret != -1) |
|
977 + if(caret != -1) { |
|
978 textArea.setCaretPosition(Math.min(caret, |
|
979 buffer.getLength())); |
|
980 + EditBus.send(new PositionChanging(this)); |
|
981 + } |
|
982 |
|
983 // set any selections |
|
984 Selection[] selection = caretInfo.selection; |
|
985 @@ -1029,7 +1032,7 @@ |
|
986 for(int i = 0; i <= 3; i++) |
|
987 { |
|
988 foldLineStyle[i] = SyntaxUtilities.parseStyle( |
|
989 - jEdit.getProperty("view.style.foldLine." + i), |
|
990 + jEdit.getThemeProperty("view.style.foldLine." + i), |
|
991 defaultFont,defaultFontSize, true); |
|
992 } |
|
993 painter.setFoldLineStyle(foldLineStyle); |
|
994 diff -ru /home/makarius/.isabelle/contrib/jedit-20250424/jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/gui/NumericTextField.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/gui/NumericTextField.java |
|
995 --- /home/makarius/.isabelle/contrib/jedit-20250424/jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/gui/NumericTextField.java 2024-08-03 19:53:18.000000000 +0200 |
|
996 +++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/gui/NumericTextField.java 2025-05-14 15:46:44.805742407 +0200 |
|
997 @@ -95,7 +95,7 @@ |
|
998 Font font = getFont(); |
|
999 String family = font.getFamily(); |
|
1000 int size = font.getSize(); |
|
1001 - invalidStyle = SyntaxUtilities.parseStyle(jEdit.getProperty("view.style.invalid"), family, size, true); |
|
1002 + invalidStyle = SyntaxUtilities.parseStyle(jEdit.getThemeProperty("view.style.invalid"), family, size, true); |
|
1003 defaultForeground = getForeground(); |
|
1004 defaultBackground = getBackground(); |
|
1005 } |
|
1006 diff -ru /home/makarius/.isabelle/contrib/jedit-20250424/jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/gui/statusbar/ErrorsWidgetFactory.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/gui/statusbar/ErrorsWidgetFactory.java |
|
1007 --- /home/makarius/.isabelle/contrib/jedit-20250424/jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/gui/statusbar/ErrorsWidgetFactory.java 2024-08-03 19:53:16.000000000 +0200 |
|
1008 +++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/gui/statusbar/ErrorsWidgetFactory.java 2025-05-14 15:46:52.413610804 +0200 |
|
1009 @@ -102,7 +102,7 @@ |
|
1010 String defaultFont = jEdit.getProperty("view.font"); |
|
1011 int defaultFontSize = jEdit.getIntegerProperty("view.fontsize", 12); |
|
1012 SyntaxStyle invalid = SyntaxUtilities.parseStyle( |
|
1013 - jEdit.getProperty("view.style.invalid"), |
|
1014 + jEdit.getThemeProperty("view.style.invalid"), |
|
1015 defaultFont,defaultFontSize, true); |
|
1016 foregroundColor = invalid.getForegroundColor(); |
|
1017 setForeground(foregroundColor); |
|
1018 diff -ru jedit5.7.0/jEdit/org/gjt/sp/jedit/options/SyntaxHiliteOptionPane.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/options/SyntaxHiliteOptionPane.java |
|
1019 --- jedit5.7.0/jEdit/org/gjt/sp/jedit/options/SyntaxHiliteOptionPane.java 2024-08-03 19:53:15.000000000 +0200 |
|
1020 +++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/options/SyntaxHiliteOptionPane.java 2025-05-15 21:23:50.047418219 +0200 |
|
1021 @@ -222,8 +222,7 @@ |
|
1022 { |
|
1023 for (StyleChoice ch : styleChoices) |
|
1024 { |
|
1025 - jEdit.setProperty(ch.property, |
|
1026 - GUIUtilities.getStyleString(ch.style)); |
|
1027 + jEdit.setThemeProperty(ch.property,GUIUtilities.getStyleString(ch.style)); |
|
1028 } |
|
1029 } //}}} |
|
1030 |
|
1031 @@ -233,7 +232,7 @@ |
|
1032 Font font = new JLabel().getFont(); |
|
1033 styleChoices.add(new StyleChoice(label, |
|
1034 property, |
|
1035 - SyntaxUtilities.parseStyle(jEdit.getProperty(property), |
|
1036 + SyntaxUtilities.parseStyle(jEdit.getThemeProperty(property), |
|
1037 font.getFamily(), font.getSize(), true))); |
|
1038 } //}}} |
|
1039 |
|
1040 @@ -289,8 +288,8 @@ |
|
1041 else |
|
1042 { |
|
1043 // this part sucks |
|
1044 - setBackground(jEdit.getColorProperty( |
|
1045 - "view.bgColor")); |
|
1046 + setBackground( |
|
1047 + jEdit.getColorProperty("view.bgColor", GUIUtilities.defaultBgColor())); |
|
1048 } |
|
1049 setFont(style.getFont()); |
|
1050 } |
|
1051 diff -ru jedit5.7.0/jEdit/org/gjt/sp/jedit/gui/StyleEditor.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/gui/StyleEditor.java |
|
1052 --- jedit5.7.0/jEdit/org/gjt/sp/jedit/gui/StyleEditor.java 2024-08-03 19:53:18.000000000 +0200 |
|
1053 +++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/gui/StyleEditor.java 2025-05-14 15:48:00.821423396 +0200 |
|
1054 @@ -90,12 +90,12 @@ |
|
1055 String property = "view.style." + typeName.toLowerCase(); |
|
1056 Font font = new JLabel().getFont(); |
|
1057 SyntaxStyle currentStyle = SyntaxUtilities.parseStyle( |
|
1058 - jEdit.getProperty(property), font.getFamily(), font.getSize(), true); |
|
1059 + jEdit.getThemeProperty(property), font.getFamily(), font.getSize(), true); |
|
1060 SyntaxStyle style = new StyleEditor(textArea.getView(), |
|
1061 currentStyle, typeName).getStyle(); |
|
1062 if(style != null) |
|
1063 { |
|
1064 - jEdit.setProperty(property, GUIUtilities.getStyleString(style)); |
|
1065 + jEdit.setProperty(property + GUIUtilities.getThemeSuffix(), GUIUtilities.getStyleString(style)); |
|
1066 jEdit.propertiesChanged(); |
|
1067 } |
|
1068 } //}}} |
|
1069 diff -ru jedit5.7.0/jEdit/org/gjt/sp/jedit/search/SearchBar.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/search/SearchBar.java |
|
1070 --- jedit5.7.0/jEdit/org/gjt/sp/jedit/search/SearchBar.java 2024-08-03 19:53:18.000000000 +0200 |
|
1071 +++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/search/SearchBar.java 2025-05-14 15:49:19.228054251 +0200 |
|
1072 @@ -51,6 +51,10 @@ |
|
1073 setFloatable(false); |
|
1074 add(Box.createHorizontalStrut(2)); |
|
1075 |
|
1076 + if (!jEdit.getProperty("navigate-toolbar", "").isEmpty()) { |
|
1077 + add(GUIUtilities.loadToolBar("navigate-toolbar")); |
|
1078 + } |
|
1079 + |
|
1080 JLabel label = new JLabel(jEdit.getProperty("view.search.find")); |
|
1081 add(label); |
|
1082 |
|
1083 @@ -59,7 +63,7 @@ |
|
1084 add(find = new HistoryTextField("find")); |
|
1085 find.setSelectAllOnFocus(true); |
|
1086 |
|
1087 - SyntaxStyle style = SyntaxUtilities.parseStyle(jEdit.getProperty("view.style.invalid"), "Dialog", 12, true); |
|
1088 + SyntaxStyle style = SyntaxUtilities.parseStyle(jEdit.getThemeProperty("view.style.invalid"), "Dialog", 12, true); |
|
1089 errorBackground = style.getBackgroundColor(); |
|
1090 errorForeground = style.getForegroundColor(); |
|
1091 defaultBackground = find.getBackground(); |