equal
deleted
inserted
replaced
1 #jEdit properties |
1 #jEdit properties |
2 buffer.deepIndent=false |
2 buffer.deepIndent=false |
3 buffer.encoding=UTF-8 |
3 buffer.encoding=UTF-8-isabelle |
4 buffer.indentSize=2 |
4 buffer.indentSize=2 |
5 buffer.lineSeparator=\n |
5 buffer.lineSeparator=\n |
6 buffer.maxLineLen=100 |
6 buffer.maxLineLen=100 |
7 buffer.noTabs=true |
7 buffer.noTabs=true |
8 buffer.tabSize=2 |
8 buffer.tabSize=2 |
9 fallbackEncodings=US-ASCII ISO-8859-15 |
9 fallbackEncodings=UTF-8 ISO-8859-15 US-ASCII |
10 firstTime=false |
10 firstTime=false |
11 tip.show=false |
11 tip.show=false |
12 encodingDetectors=BOM XML-PI buffer-local-property |
12 encodingDetectors=BOM XML-PI buffer-local-property |
13 delete-line.shortcut=A+d |
13 delete-line.shortcut=A+d |
14 delete.shortcut2=C+d |
14 delete.shortcut2=C+d |