src/Tools/jEdit/src/jEdit.props
changeset 63455 019856db2bb6
parent 63236 48bc9045866e
child 63726 dd327befd2ef
equal deleted inserted replaced
63454:08a1f61a49a6 63455:019856db2bb6
   220 isabelle.increase-font-size.label=Increase font size
   220 isabelle.increase-font-size.label=Increase font size
   221 isabelle.increase-font-size.shortcut2=C+ADD
   221 isabelle.increase-font-size.shortcut2=C+ADD
   222 isabelle.increase-font-size.shortcut=C+PLUS
   222 isabelle.increase-font-size.shortcut=C+PLUS
   223 isabelle.increase-font-size2.label=Increase font size (clone)
   223 isabelle.increase-font-size2.label=Increase font size (clone)
   224 isabelle.increase-font-size2.shortcut=C+EQUALS
   224 isabelle.increase-font-size2.shortcut=C+EQUALS
       
   225 isabelle.newline.label=Newline with indentation of Isabelle keywords
       
   226 isabelle.newline.shortcut=ENTER
   225 isabelle.options.label=Isabelle options
   227 isabelle.options.label=Isabelle options
   226 isabelle.reset-continuous-checking.label=Reset continuous checking
   228 isabelle.reset-continuous-checking.label=Reset continuous checking
   227 isabelle.reset-font-size.label=Reset font size
   229 isabelle.reset-font-size.label=Reset font size
   228 isabelle.reset-node-required.label=Reset node required
   230 isabelle.reset-node-required.label=Reset node required
   229 isabelle.reset-words.label=Reset non-permanent words
   231 isabelle.reset-words.label=Reset non-permanent words