src/Tools/jEdit/src/jEdit.props
changeset 66036 b6396880b644
parent 63760 b1088b1e3b7e
child 67132 336831647779
equal deleted inserted replaced
66034:ded1c636aece 66036:b6396880b644
   224 isabelle.increase-font-size2.label=Increase font size (clone)
   224 isabelle.increase-font-size2.label=Increase font size (clone)
   225 isabelle.increase-font-size2.shortcut=C+EQUALS
   225 isabelle.increase-font-size2.shortcut=C+EQUALS
   226 isabelle.newline.label=Newline with indentation of Isabelle keywords
   226 isabelle.newline.label=Newline with indentation of Isabelle keywords
   227 isabelle.newline.shortcut=ENTER
   227 isabelle.newline.shortcut=ENTER
   228 isabelle.options.label=Isabelle options
   228 isabelle.options.label=Isabelle options
       
   229 isabelle.preview.label=HTML preview of PIDE document
   229 isabelle.reset-continuous-checking.label=Reset continuous checking
   230 isabelle.reset-continuous-checking.label=Reset continuous checking
   230 isabelle.reset-font-size.label=Reset font size
   231 isabelle.reset-font-size.label=Reset font size
   231 isabelle.reset-node-required.label=Reset node required
   232 isabelle.reset-node-required.label=Reset node required
   232 isabelle.reset-words.label=Reset non-permanent words
   233 isabelle.reset-words.label=Reset non-permanent words
   233 isabelle.select-entity.label=Select all occurences of formal entity at caret
   234 isabelle.select-entity.label=Select all occurences of formal entity at caret