equal
deleted
inserted
replaced
267 lang.usedefaultlocale=false |
267 lang.usedefaultlocale=false |
268 largefilemode=full |
268 largefilemode=full |
269 line-end.shortcut=END |
269 line-end.shortcut=END |
270 line-home.shortcut=HOME |
270 line-home.shortcut=HOME |
271 logo.icon.medium=32x32/apps/isabelle.gif |
271 logo.icon.medium=32x32/apps/isabelle.gif |
272 lookAndFeel=javax.swing.plaf.metal.MetalLookAndFeel |
272 lookAndFeel=com.formdev.flatlaf.FlatLightLaf |
273 match-bracket.shortcut2=C+9 |
273 match-bracket.shortcut2=C+9 |
274 metal.primary.font=Isabelle DejaVu Sans |
274 metal.primary.font=Isabelle DejaVu Sans |
275 metal.primary.fontsize=12 |
275 metal.primary.fontsize=12 |
276 metal.secondary.font=Isabelle DejaVu Sans |
276 metal.secondary.font=Isabelle DejaVu Sans |
277 metal.secondary.fontsize=12 |
277 metal.secondary.fontsize=12 |