src/Tools/jEdit/src/jEdit.props
changeset 50147 8d2251b9a200
parent 48717 622251b2b0f1
child 50299 f70b3712040f
equal deleted inserted replaced
50146:03f38212442a 50147:8d2251b9a200
   180 isabelle-output.dock-position=bottom
   180 isabelle-output.dock-position=bottom
   181 isabelle-output.height=174
   181 isabelle-output.height=174
   182 isabelle-output.width=412
   182 isabelle-output.width=412
   183 isabelle-readme.dock-position=bottom
   183 isabelle-readme.dock-position=bottom
   184 isabelle-session.dock-position=bottom
   184 isabelle-session.dock-position=bottom
       
   185 isabelle-symbols.dock-position=bottom
   185 line-end.shortcut=END
   186 line-end.shortcut=END
   186 line-home.shortcut=HOME
   187 line-home.shortcut=HOME
   187 lookAndFeel=com.sun.java.swing.plaf.nimbus.NimbusLookAndFeel
   188 lookAndFeel=com.sun.java.swing.plaf.nimbus.NimbusLookAndFeel
   188 print.font=IsabelleText
   189 print.font=IsabelleText
   189 restore.remote=false
   190 restore.remote=false