src/Tools/jEdit/src/jEdit.props
changeset 60878 1f0d2bbcf38b
parent 60877 8d00ff5a052e
child 61208 19118f9b939d
equal deleted inserted replaced
60877:8d00ff5a052e 60878:1f0d2bbcf38b
   224 isabelle.reset-font-size.label=Reset font size
   224 isabelle.reset-font-size.label=Reset font size
   225 isabelle.reset-node-required.label=Reset node required
   225 isabelle.reset-node-required.label=Reset node required
   226 isabelle.reset-words.label=Reset non-permanent words
   226 isabelle.reset-words.label=Reset non-permanent words
   227 isabelle.set-continuous-checking.label=Set continuous checking
   227 isabelle.set-continuous-checking.label=Set continuous checking
   228 isabelle.set-node-required.label=Set node required
   228 isabelle.set-node-required.label=Set node required
       
   229 isabelle.toggle-breakpoint.label=Toggle Breakpoint
   229 isabelle.toggle-continuous-checking.label=Toggle continuous checking
   230 isabelle.toggle-continuous-checking.label=Toggle continuous checking
   230 isabelle.toggle-continuous-checking.shortcut=C+e ENTER
   231 isabelle.toggle-continuous-checking.shortcut=C+e ENTER
   231 isabelle.toggle-node-required.label=Toggle node required
   232 isabelle.toggle-node-required.label=Toggle node required
   232 isabelle.toggle-node-required.shortcut=C+e SPACE
   233 isabelle.toggle-node-required.shortcut=C+e SPACE
   233 lang.usedefaultlocale=false
   234 lang.usedefaultlocale=false