src/Tools/jEdit/src/jEdit.props
author wenzelm
Sat, 24 Nov 2018 18:56:44 +0100
changeset 69343 395c4fb15ea2
parent 68080 17f79ae49401
child 69643 83f15deb2d36
permissions -rw-r--r--
use "Isabelle DejaVu" fonts uniformly: Text Area, GUI elements, HTML output etc.;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
34334
68e172602b86 essential default properties for jEdit;
wenzelm
parents:
diff changeset
     1
#jEdit properties
34702
efa196219dd3 sorted;
wenzelm
parents: 34666
diff changeset
     2
buffer.deepIndent=false
efa196219dd3 sorted;
wenzelm
parents: 34666
diff changeset
     3
buffer.encoding=UTF-8-Isabelle
efa196219dd3 sorted;
wenzelm
parents: 34666
diff changeset
     4
buffer.indentSize=2
efa196219dd3 sorted;
wenzelm
parents: 34666
diff changeset
     5
buffer.lineSeparator=\n
efa196219dd3 sorted;
wenzelm
parents: 34666
diff changeset
     6
buffer.maxLineLen=100
efa196219dd3 sorted;
wenzelm
parents: 34666
diff changeset
     7
buffer.noTabs=true
40791
d71fe93e8e0c less frequent sidekick parsing, which is relatively slow;
wenzelm
parents: 40460
diff changeset
     8
buffer.sidekick.keystroke-parse=false
34702
efa196219dd3 sorted;
wenzelm
parents: 34666
diff changeset
     9
buffer.tabSize=2
58779
aeba9ae93dd8 more generous default;
wenzelm
parents: 58746
diff changeset
    10
buffer.undoCount=1000
53188
bb5433b13ff2 some secondary shortcuts derived from 5.1.0/keymaps/German_Keyboard_keys.props (using CIRCUMFLEX instead of S+1);
wenzelm
parents: 53161
diff changeset
    11
close-docking-area.shortcut2=C+e C+CIRCUMFLEX
54318
1bdd8f541a06 avoid confusion of isabelle.complete vs. menu item complete-word (NB: alternative shortcuts not shown in menus);
wenzelm
parents: 54306
diff changeset
    12
complete-word.shortcut=
50796
2d68df7ed89d Console is not docked on startup;
wenzelm
parents: 50730
diff changeset
    13
console.dock-position=floating
34880
f88fc4fcab86 provide JEDIT_SETTINGS via settings;
wenzelm
parents: 34814
diff changeset
    14
console.encoding=UTF-8
69343
395c4fb15ea2 use "Isabelle DejaVu" fonts uniformly: Text Area, GUI elements, HTML output etc.;
wenzelm
parents: 68080
diff changeset
    15
console.font=Isabelle DejaVu Sans Mono
34880
f88fc4fcab86 provide JEDIT_SETTINGS via settings;
wenzelm
parents: 34814
diff changeset
    16
console.fontsize=14
34702
efa196219dd3 sorted;
wenzelm
parents: 34666
diff changeset
    17
delete-line.shortcut=A+d
efa196219dd3 sorted;
wenzelm
parents: 34666
diff changeset
    18
delete.shortcut2=C+d
34626
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
    19
encoding.opt-out.Big5-HKSCS=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
    20
encoding.opt-out.Big5=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
    21
encoding.opt-out.COMPOUND_TEXT=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
    22
encoding.opt-out.EUC-JP=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
    23
encoding.opt-out.EUC-KR=true
60877
8d00ff5a052e sort lines;
wenzelm
parents: 60749
diff changeset
    24
encoding.opt-out.GB2312=true
34626
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
    25
encoding.opt-out.GB18030=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
    26
encoding.opt-out.GBK=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
    27
encoding.opt-out.IBM-Thai=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
    28
encoding.opt-out.IBM00858=true
60877
8d00ff5a052e sort lines;
wenzelm
parents: 60749
diff changeset
    29
encoding.opt-out.IBM037=true
34626
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
    30
encoding.opt-out.IBM01140=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
    31
encoding.opt-out.IBM01141=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
    32
encoding.opt-out.IBM01142=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
    33
encoding.opt-out.IBM01143=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
    34
encoding.opt-out.IBM01144=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
    35
encoding.opt-out.IBM01145=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
    36
encoding.opt-out.IBM01146=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
    37
encoding.opt-out.IBM01147=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
    38
encoding.opt-out.IBM01148=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
    39
encoding.opt-out.IBM01149=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
    40
encoding.opt-out.IBM273=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
    41
encoding.opt-out.IBM277=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
    42
encoding.opt-out.IBM278=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
    43
encoding.opt-out.IBM280=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
    44
encoding.opt-out.IBM284=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
    45
encoding.opt-out.IBM285=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
    46
encoding.opt-out.IBM297=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
    47
encoding.opt-out.IBM420=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
    48
encoding.opt-out.IBM424=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
    49
encoding.opt-out.IBM437=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
    50
encoding.opt-out.IBM500=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
    51
encoding.opt-out.IBM775=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
    52
encoding.opt-out.IBM850=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
    53
encoding.opt-out.IBM852=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
    54
encoding.opt-out.IBM855=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
    55
encoding.opt-out.IBM857=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
    56
encoding.opt-out.IBM860=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
    57
encoding.opt-out.IBM861=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
    58
encoding.opt-out.IBM862=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
    59
encoding.opt-out.IBM863=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
    60
encoding.opt-out.IBM864=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
    61
encoding.opt-out.IBM865=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
    62
encoding.opt-out.IBM866=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
    63
encoding.opt-out.IBM868=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
    64
encoding.opt-out.IBM869=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
    65
encoding.opt-out.IBM870=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
    66
encoding.opt-out.IBM871=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
    67
encoding.opt-out.IBM918=true
60877
8d00ff5a052e sort lines;
wenzelm
parents: 60749
diff changeset
    68
encoding.opt-out.IBM1026=true
8d00ff5a052e sort lines;
wenzelm
parents: 60749
diff changeset
    69
encoding.opt-out.IBM1047=true
34626
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
    70
encoding.opt-out.ISO-2022-CN=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
    71
encoding.opt-out.ISO-2022-JP-2=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
    72
encoding.opt-out.ISO-2022-JP=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
    73
encoding.opt-out.ISO-2022-KR=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
    74
encoding.opt-out.ISO-8859-2=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
    75
encoding.opt-out.ISO-8859-3=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
    76
encoding.opt-out.ISO-8859-4=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
    77
encoding.opt-out.ISO-8859-5=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
    78
encoding.opt-out.ISO-8859-6=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
    79
encoding.opt-out.ISO-8859-7=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
    80
encoding.opt-out.ISO-8859-8=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
    81
encoding.opt-out.ISO-8859-9=true
60877
8d00ff5a052e sort lines;
wenzelm
parents: 60749
diff changeset
    82
encoding.opt-out.ISO-8859-13=true
34626
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
    83
encoding.opt-out.JIS_X0201=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
    84
encoding.opt-out.JIS_X0212-1990=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
    85
encoding.opt-out.KOI8-R=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
    86
encoding.opt-out.KOI8-U=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
    87
encoding.opt-out.Shift_JIS=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
    88
encoding.opt-out.TIS-620=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
    89
encoding.opt-out.UTF-16=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
    90
encoding.opt-out.UTF-16BE=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
    91
encoding.opt-out.UTF-16LE=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
    92
encoding.opt-out.UTF-32=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
    93
encoding.opt-out.UTF-32BE=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
    94
encoding.opt-out.UTF-32LE=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
    95
encoding.opt-out.X-UTF-32BE-BOM=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
    96
encoding.opt-out.X-UTF-32LE-BOM=true
60877
8d00ff5a052e sort lines;
wenzelm
parents: 60749
diff changeset
    97
encoding.opt-out.windows-31j=true
34626
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
    98
encoding.opt-out.windows-1250=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
    99
encoding.opt-out.windows-1251=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
   100
encoding.opt-out.windows-1253=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
   101
encoding.opt-out.windows-1254=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
   102
encoding.opt-out.windows-1255=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
   103
encoding.opt-out.windows-1256=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
   104
encoding.opt-out.windows-1257=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
   105
encoding.opt-out.windows-1258=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
   106
encoding.opt-out.x-Big5-Solaris=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
   107
encoding.opt-out.x-EUC-TW=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
   108
encoding.opt-out.x-IBM737=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
   109
encoding.opt-out.x-IBM834=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
   110
encoding.opt-out.x-IBM856=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
   111
encoding.opt-out.x-IBM874=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
   112
encoding.opt-out.x-IBM875=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
   113
encoding.opt-out.x-IBM921=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
   114
encoding.opt-out.x-IBM922=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
   115
encoding.opt-out.x-IBM930=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
   116
encoding.opt-out.x-IBM933=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
   117
encoding.opt-out.x-IBM935=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
   118
encoding.opt-out.x-IBM937=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
   119
encoding.opt-out.x-IBM939=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
   120
encoding.opt-out.x-IBM942=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
   121
encoding.opt-out.x-IBM942C=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
   122
encoding.opt-out.x-IBM943=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
   123
encoding.opt-out.x-IBM943C=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
   124
encoding.opt-out.x-IBM948=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
   125
encoding.opt-out.x-IBM949=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
   126
encoding.opt-out.x-IBM949C=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
   127
encoding.opt-out.x-IBM950=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
   128
encoding.opt-out.x-IBM964=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
   129
encoding.opt-out.x-IBM970=true
60877
8d00ff5a052e sort lines;
wenzelm
parents: 60749
diff changeset
   130
encoding.opt-out.x-IBM1006=true
8d00ff5a052e sort lines;
wenzelm
parents: 60749
diff changeset
   131
encoding.opt-out.x-IBM1025=true
8d00ff5a052e sort lines;
wenzelm
parents: 60749
diff changeset
   132
encoding.opt-out.x-IBM1046=true
8d00ff5a052e sort lines;
wenzelm
parents: 60749
diff changeset
   133
encoding.opt-out.x-IBM1097=true
8d00ff5a052e sort lines;
wenzelm
parents: 60749
diff changeset
   134
encoding.opt-out.x-IBM1098=true
8d00ff5a052e sort lines;
wenzelm
parents: 60749
diff changeset
   135
encoding.opt-out.x-IBM1112=true
8d00ff5a052e sort lines;
wenzelm
parents: 60749
diff changeset
   136
encoding.opt-out.x-IBM1122=true
8d00ff5a052e sort lines;
wenzelm
parents: 60749
diff changeset
   137
encoding.opt-out.x-IBM1123=true
8d00ff5a052e sort lines;
wenzelm
parents: 60749
diff changeset
   138
encoding.opt-out.x-IBM1124=true
8d00ff5a052e sort lines;
wenzelm
parents: 60749
diff changeset
   139
encoding.opt-out.x-IBM1381=true
8d00ff5a052e sort lines;
wenzelm
parents: 60749
diff changeset
   140
encoding.opt-out.x-IBM1383=true
8d00ff5a052e sort lines;
wenzelm
parents: 60749
diff changeset
   141
encoding.opt-out.x-IBM33722=true
34626
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
   142
encoding.opt-out.x-ISCII91=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
   143
encoding.opt-out.x-ISO-2022-CN-CNS=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
   144
encoding.opt-out.x-ISO-2022-CN-GB=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
   145
encoding.opt-out.x-JIS0208=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
   146
encoding.opt-out.x-JISAutoDetect=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
   147
encoding.opt-out.x-Johab=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
   148
encoding.opt-out.x-MS932_0213=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
   149
encoding.opt-out.x-MS950-HKSCS=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
   150
encoding.opt-out.x-MacArabic=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
   151
encoding.opt-out.x-MacCentralEurope=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
   152
encoding.opt-out.x-MacCroatian=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
   153
encoding.opt-out.x-MacCyrillic=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
   154
encoding.opt-out.x-MacDingbat=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
   155
encoding.opt-out.x-MacGreek=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
   156
encoding.opt-out.x-MacHebrew=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
   157
encoding.opt-out.x-MacIceland=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
   158
encoding.opt-out.x-MacRoman=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
   159
encoding.opt-out.x-MacRomania=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
   160
encoding.opt-out.x-MacSymbol=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
   161
encoding.opt-out.x-MacThai=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
   162
encoding.opt-out.x-MacTurkish=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
   163
encoding.opt-out.x-MacUkraine=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
   164
encoding.opt-out.x-PCK=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
   165
encoding.opt-out.x-SJIS_0213=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
   166
encoding.opt-out.x-UTF-16LE-BOM=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
   167
encoding.opt-out.x-euc-jp-linux=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
   168
encoding.opt-out.x-eucJP-Open=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
   169
encoding.opt-out.x-iso-8859-11=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
   170
encoding.opt-out.x-mswin-936=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
   171
encoding.opt-out.x-windows-874=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
   172
encoding.opt-out.x-windows-949=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
   173
encoding.opt-out.x-windows-950=true
60877
8d00ff5a052e sort lines;
wenzelm
parents: 60749
diff changeset
   174
encoding.opt-out.x-windows-50220=true
8d00ff5a052e sort lines;
wenzelm
parents: 60749
diff changeset
   175
encoding.opt-out.x-windows-50221=true
34626
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
   176
encoding.opt-out.x-windows-iso2022jp=true
34702
efa196219dd3 sorted;
wenzelm
parents: 34666
diff changeset
   177
encodingDetectors=BOM XML-PI buffer-local-property
37190
ea52509f4c42 more basic default behaviour of ENTER, HOME, END;
wenzelm
parents: 37162
diff changeset
   178
end.shortcut=
53188
bb5433b13ff2 some secondary shortcuts derived from 5.1.0/keymaps/German_Keyboard_keys.props (using CIRCUMFLEX instead of S+1);
wenzelm
parents: 53161
diff changeset
   179
expand-abbrev.shortcut2=CA+SPACE
63757
a9159d30070f avoid conflict after initial keymap migration;
wenzelm
parents: 63749
diff changeset
   180
expand-folds.shortcut=
34619
e89b6ec97910 added IsabelleEncoding -- a clone of utf-8 for now;
wenzelm
parents: 34613
diff changeset
   181
fallbackEncodings=UTF-8 ISO-8859-15 US-ASCII
34512
14d70378f1c7 modified netbeans build such that dist can be used as settings-directory for jedit;
immler@in.tum.de
parents: 34425
diff changeset
   182
firstTime=false
53188
bb5433b13ff2 some secondary shortcuts derived from 5.1.0/keymaps/German_Keyboard_keys.props (using CIRCUMFLEX instead of S+1);
wenzelm
parents: 53161
diff changeset
   183
focus-buffer-switcher.shortcut2=A+CIRCUMFLEX
58746
68c2cbe2fd3a back to alternative fold painter, despite f03a9c57760a -- gutter painter seems to have changed in the meantime;
wenzelm
parents: 57627
diff changeset
   184
foldPainter=Circle
62675
2f816b80e3f4 avoid redundant addLeftOfScrollBar;
wenzelm
parents: 61529
diff changeset
   185
gatchan.highlight.overview=false
69343
395c4fb15ea2 use "Isabelle DejaVu" fonts uniformly: Text Area, GUI elements, HTML output etc.;
wenzelm
parents: 68080
diff changeset
   186
helpviewer.font=Isabelle DejaVu Serif
37190
ea52509f4c42 more basic default behaviour of ENTER, HOME, END;
wenzelm
parents: 37162
diff changeset
   187
home.shortcut=
ea52509f4c42 more basic default behaviour of ENTER, HOME, END;
wenzelm
parents: 37162
diff changeset
   188
insert-newline-indent.shortcut=
63735
fb0ae6b60491 clarified (see 019856db2bb6, ea52509f4c42);
wenzelm
parents: 63726
diff changeset
   189
insert-newline.shortcut=
67132
336831647779 added action to make antiquoted cartouche;
wenzelm
parents: 66036
diff changeset
   190
isabelle.antiquoted_cartouche.label=Make antiquoted cartouche
60749
f727b99faaf7 skeleton for interactive debugger;
wenzelm
parents: 60269
diff changeset
   191
isabelle-debugger.dock-position=floating
52947
a7947b72bac2 sorted lines;
wenzelm
parents: 52815
diff changeset
   192
isabelle-documentation.dock-position=right
34880
f88fc4fcab86 provide JEDIT_SETTINGS via settings;
wenzelm
parents: 34814
diff changeset
   193
isabelle-output.dock-position=bottom
39815
37bdc2220cf8 tuned default "Prover Session" perspective;
wenzelm
parents: 39739
diff changeset
   194
isabelle-output.height=174
37bdc2220cf8 tuned default "Prover Session" perspective;
wenzelm
parents: 39739
diff changeset
   195
isabelle-output.width=412
56879
ee2b61f37ad9 renamed "Find" to "Query", with more general operations;
wenzelm
parents: 56632
diff changeset
   196
isabelle-query.dock-position=bottom
56986
43be5818a45c clarified docking layout, amending 9c2ca698690e;
wenzelm
parents: 56962
diff changeset
   197
isabelle-simplifier-trace.dock-position=floating
43be5818a45c clarified docking layout, amending 9c2ca698690e;
wenzelm
parents: 56962
diff changeset
   198
isabelle-sledgehammer.dock-position=bottom
61208
19118f9b939d separate panel for proof state output;
wenzelm
parents: 60878
diff changeset
   199
isabelle-state.dock-position=right
50306
b655d2d0406d updated to jedit-5.0.0;
wenzelm
parents: 50299
diff changeset
   200
isabelle-symbols.dock-position=bottom
50803
8a1ea6b00ace dock "Theories" right, although it might obscure some control buttons;
wenzelm
parents: 50796
diff changeset
   201
isabelle-theories.dock-position=right
60877
8d00ff5a052e sort lines;
wenzelm
parents: 60749
diff changeset
   202
isabelle.complete-word.label=Complete word
54318
1bdd8f541a06 avoid confusion of isabelle.complete vs. menu item complete-word (NB: alternative shortcuts not shown in menus);
wenzelm
parents: 54306
diff changeset
   203
isabelle.complete.label=Complete Isabelle text
1bdd8f541a06 avoid confusion of isabelle.complete vs. menu item complete-word (NB: alternative shortcuts not shown in menus);
wenzelm
parents: 54306
diff changeset
   204
isabelle.complete.shortcut2=C+b
50308
08b55c5ce064 moved isabelle shortcuts to main jEdit.props, in order to have them migrated to the "imported" keymap;
wenzelm
parents: 50306
diff changeset
   205
isabelle.control-bold.label=Control bold
08b55c5ce064 moved isabelle shortcuts to main jEdit.props, in order to have them migrated to the "imported" keymap;
wenzelm
parents: 50306
diff changeset
   206
isabelle.control-bold.shortcut=C+e RIGHT
61483
07c8d5d8acab added action "isabelle-emph";
wenzelm
parents: 61218
diff changeset
   207
isabelle.control-emph.label=Control emphasized
07c8d5d8acab added action "isabelle-emph";
wenzelm
parents: 61218
diff changeset
   208
isabelle.control-emph.shortcut=C+e LEFT
53188
bb5433b13ff2 some secondary shortcuts derived from 5.1.0/keymaps/German_Keyboard_keys.props (using CIRCUMFLEX instead of S+1);
wenzelm
parents: 53161
diff changeset
   209
isabelle.control-reset.label=Control reset
61483
07c8d5d8acab added action "isabelle-emph";
wenzelm
parents: 61218
diff changeset
   210
isabelle.control-reset.shortcut=C+e BACK_SPACE
53021
d0fa3f446b9d discontinued special treatment of \<^isub> and \<^isup> in rendering or editor front-end;
wenzelm
parents: 52948
diff changeset
   211
isabelle.control-sub.label=Control subscript
d0fa3f446b9d discontinued special treatment of \<^isub> and \<^isup> in rendering or editor front-end;
wenzelm
parents: 52948
diff changeset
   212
isabelle.control-sub.shortcut=C+e DOWN
50506
7d8406ebe18f odd bias of sub/superscript keyboard shortcuts -- according to frequency of use;
wenzelm
parents: 50492
diff changeset
   213
isabelle.control-sup.label=Control superscript
7d8406ebe18f odd bias of sub/superscript keyboard shortcuts -- according to frequency of use;
wenzelm
parents: 50492
diff changeset
   214
isabelle.control-sup.shortcut=C+e UP
50308
08b55c5ce064 moved isabelle shortcuts to main jEdit.props, in order to have them migrated to the "imported" keymap;
wenzelm
parents: 50306
diff changeset
   215
isabelle.decrease-font-size.label=Decrease font size
51069
2f50ddd3b586 more portable alternative shortcuts on numeric keypad;
wenzelm
parents: 50803
diff changeset
   216
isabelle.decrease-font-size.shortcut2=C+SUBTRACT
50308
08b55c5ce064 moved isabelle shortcuts to main jEdit.props, in order to have them migrated to the "imported" keymap;
wenzelm
parents: 50306
diff changeset
   217
isabelle.decrease-font-size.shortcut=C+MINUS
52428
fce1c133e1f8 clones of increase-font-size / decrease-font-size to allow two further shortcuts for various keyboard layouts;
wenzelm
parents: 51069
diff changeset
   218
isabelle.decrease-font-size2.label=Decrease font size (clone)
68067
b91c4acc1aaf clarified menu actions;
wenzelm
parents: 67647
diff changeset
   219
isabelle.draft.label=Show draft in browser
60877
8d00ff5a052e sort lines;
wenzelm
parents: 60749
diff changeset
   220
isabelle.exclude-word-permanently.label=Exclude word permanently
8d00ff5a052e sort lines;
wenzelm
parents: 60749
diff changeset
   221
isabelle.exclude-word.label=Exclude word
8d00ff5a052e sort lines;
wenzelm
parents: 60749
diff changeset
   222
isabelle.include-word-permanently.label=Include word permanently
8d00ff5a052e sort lines;
wenzelm
parents: 60749
diff changeset
   223
isabelle.include-word.label=Include word
50308
08b55c5ce064 moved isabelle shortcuts to main jEdit.props, in order to have them migrated to the "imported" keymap;
wenzelm
parents: 50306
diff changeset
   224
isabelle.increase-font-size.label=Increase font size
51069
2f50ddd3b586 more portable alternative shortcuts on numeric keypad;
wenzelm
parents: 50803
diff changeset
   225
isabelle.increase-font-size.shortcut2=C+ADD
50308
08b55c5ce064 moved isabelle shortcuts to main jEdit.props, in order to have them migrated to the "imported" keymap;
wenzelm
parents: 50306
diff changeset
   226
isabelle.increase-font-size.shortcut=C+PLUS
52428
fce1c133e1f8 clones of increase-font-size / decrease-font-size to allow two further shortcuts for various keyboard layouts;
wenzelm
parents: 51069
diff changeset
   227
isabelle.increase-font-size2.label=Increase font size (clone)
52947
a7947b72bac2 sorted lines;
wenzelm
parents: 52815
diff changeset
   228
isabelle.increase-font-size2.shortcut=C+EQUALS
63455
019856db2bb6 added action "isabelle.newline" (shortcut ENTER);
wenzelm
parents: 63236
diff changeset
   229
isabelle.newline.label=Newline with indentation of Isabelle keywords
019856db2bb6 added action "isabelle.newline" (shortcut ENTER);
wenzelm
parents: 63236
diff changeset
   230
isabelle.newline.shortcut=ENTER
57627
65fc7ae1bf66 added action "isabelle.options" (despite problems with initial window size);
wenzelm
parents: 56986
diff changeset
   231
isabelle.options.label=Isabelle options
68067
b91c4acc1aaf clarified menu actions;
wenzelm
parents: 67647
diff changeset
   232
isabelle.preview.label=Show preview in browser
52947
a7947b72bac2 sorted lines;
wenzelm
parents: 52815
diff changeset
   233
isabelle.reset-continuous-checking.label=Reset continuous checking
53161
051cbf663b5f added action isabelle.reset-font-size;
wenzelm
parents: 53058
diff changeset
   234
isabelle.reset-font-size.label=Reset font size
52947
a7947b72bac2 sorted lines;
wenzelm
parents: 52815
diff changeset
   235
isabelle.reset-node-required.label=Reset node required
60877
8d00ff5a052e sort lines;
wenzelm
parents: 60749
diff changeset
   236
isabelle.reset-words.label=Reset non-permanent words
63236
48bc9045866e added action "isabelle.select-entity";
wenzelm
parents: 62675
diff changeset
   237
isabelle.select-entity.label=Select all occurences of formal entity at caret
48bc9045866e added action "isabelle.select-entity";
wenzelm
parents: 62675
diff changeset
   238
isabelle.select-entity.shortcut=CS+ENTER
52947
a7947b72bac2 sorted lines;
wenzelm
parents: 52815
diff changeset
   239
isabelle.set-continuous-checking.label=Set continuous checking
a7947b72bac2 sorted lines;
wenzelm
parents: 52815
diff changeset
   240
isabelle.set-node-required.label=Set node required
60878
1f0d2bbcf38b added action to toggle breakpoints (on editor side);
wenzelm
parents: 60877
diff changeset
   241
isabelle.toggle-breakpoint.label=Toggle Breakpoint
52947
a7947b72bac2 sorted lines;
wenzelm
parents: 52815
diff changeset
   242
isabelle.toggle-continuous-checking.label=Toggle continuous checking
a7947b72bac2 sorted lines;
wenzelm
parents: 52815
diff changeset
   243
isabelle.toggle-continuous-checking.shortcut=C+e ENTER
a7947b72bac2 sorted lines;
wenzelm
parents: 52815
diff changeset
   244
isabelle.toggle-node-required.label=Toggle node required
a7947b72bac2 sorted lines;
wenzelm
parents: 52815
diff changeset
   245
isabelle.toggle-node-required.shortcut=C+e SPACE
61218
04c769fe1cb5 clarified isabelle.update-state;
wenzelm
parents: 61208
diff changeset
   246
isabelle.update-state.label=Update state output
04c769fe1cb5 clarified isabelle.update-state;
wenzelm
parents: 61208
diff changeset
   247
isabelle.update-state.shortcut=S+ENTER
50306
b655d2d0406d updated to jedit-5.0.0;
wenzelm
parents: 50299
diff changeset
   248
lang.usedefaultlocale=false
b655d2d0406d updated to jedit-5.0.0;
wenzelm
parents: 50299
diff changeset
   249
largefilemode=full
37190
ea52509f4c42 more basic default behaviour of ENTER, HOME, END;
wenzelm
parents: 37162
diff changeset
   250
line-end.shortcut=END
ea52509f4c42 more basic default behaviour of ENTER, HOME, END;
wenzelm
parents: 37162
diff changeset
   251
line-home.shortcut=HOME
54660
d9c88171b393 prefer isabelle application icon;
wenzelm
parents: 54654
diff changeset
   252
logo.icon.medium=32x32/apps/isabelle.gif
61529
82fc5a6231a2 back to traditional Metal as default, and thus evade current problems with Nimbus scrollbar slider;
wenzelm
parents: 61526
diff changeset
   253
lookAndFeel=javax.swing.plaf.metal.MetalLookAndFeel
53188
bb5433b13ff2 some secondary shortcuts derived from 5.1.0/keymaps/German_Keyboard_keys.props (using CIRCUMFLEX instead of S+1);
wenzelm
parents: 53161
diff changeset
   254
match-bracket.shortcut2=C+9
69343
395c4fb15ea2 use "Isabelle DejaVu" fonts uniformly: Text Area, GUI elements, HTML output etc.;
wenzelm
parents: 68080
diff changeset
   255
metal.primary.font=Isabelle DejaVu Sans
395c4fb15ea2 use "Isabelle DejaVu" fonts uniformly: Text Area, GUI elements, HTML output etc.;
wenzelm
parents: 68080
diff changeset
   256
metal.secondary.font=Isabelle DejaVu Sans
56413
2d4d9a5f68ff support for jEdit Navigator plugin;
wenzelm
parents: 55558
diff changeset
   257
navigator.showOnToolbar=true
53188
bb5433b13ff2 some secondary shortcuts derived from 5.1.0/keymaps/German_Keyboard_keys.props (using CIRCUMFLEX instead of S+1);
wenzelm
parents: 53161
diff changeset
   258
next-bracket.shortcut2=C+e C+9
63760
b1088b1e3b7e uniform capitalization of labels;
wenzelm
parents: 63757
diff changeset
   259
options.shortcuts.deletekeymap.label=Delete
b1088b1e3b7e uniform capitalization of labels;
wenzelm
parents: 63757
diff changeset
   260
options.shortcuts.duplicatekeymap.dialog.title=Keymap name
b1088b1e3b7e uniform capitalization of labels;
wenzelm
parents: 63757
diff changeset
   261
options.shortcuts.duplicatekeymap.label=Duplicate
b1088b1e3b7e uniform capitalization of labels;
wenzelm
parents: 63757
diff changeset
   262
options.shortcuts.resetkeymap.dialog.title=Reset keymap
b1088b1e3b7e uniform capitalization of labels;
wenzelm
parents: 63757
diff changeset
   263
options.shortcuts.resetkeymap.label=Reset
69343
395c4fb15ea2 use "Isabelle DejaVu" fonts uniformly: Text Area, GUI elements, HTML output etc.;
wenzelm
parents: 68080
diff changeset
   264
options.textarea.lineSpacing=0
53883
f1c5f857df3d include MacOSX plugin by default -- disabled by default to avoid multiplatform confusion;
wenzelm
parents: 53772
diff changeset
   265
plugin-blacklist.MacOSX.jar=true
50728
e7b2cfcef94c updated to jedit_build-20130104;
wenzelm
parents: 50506
diff changeset
   266
plugin.MacOSXPlugin.altDispatcher=false
50492
8d8e882c7fbe prevent dedicated MacOSX plugin from switching off vital workarounds;
wenzelm
parents: 50354
diff changeset
   267
plugin.MacOSXPlugin.disableOption=true
53188
bb5433b13ff2 some secondary shortcuts derived from 5.1.0/keymaps/German_Keyboard_keys.props (using CIRCUMFLEX instead of S+1);
wenzelm
parents: 53161
diff changeset
   268
prev-bracket.shortcut2=C+e C+8
69343
395c4fb15ea2 use "Isabelle DejaVu" fonts uniformly: Text Area, GUI elements, HTML output etc.;
wenzelm
parents: 68080
diff changeset
   269
print.font=Isabelle DejaVu Sans Mono
63726
dd327befd2ef clarified default;
wenzelm
parents: 63455
diff changeset
   270
print.glyphVector=true
53188
bb5433b13ff2 some secondary shortcuts derived from 5.1.0/keymaps/German_Keyboard_keys.props (using CIRCUMFLEX instead of S+1);
wenzelm
parents: 53161
diff changeset
   271
recent-buffer.shortcut2=C+CIRCUMFLEX
41631
8ff597b3dd80 do not restore old files on startup, which is potentially slow due to automatic rechecking;
wenzelm
parents: 40791
diff changeset
   272
restore.remote=false
8ff597b3dd80 do not restore old files on startup, which is potentially slow due to automatic rechecking;
wenzelm
parents: 40791
diff changeset
   273
restore=false
56892
1c7552b05466 tuned defaults;
wenzelm
parents: 56879
diff changeset
   274
search.subdirs.toggle=true
53188
bb5433b13ff2 some secondary shortcuts derived from 5.1.0/keymaps/German_Keyboard_keys.props (using CIRCUMFLEX instead of S+1);
wenzelm
parents: 53161
diff changeset
   275
select-block.shortcut2=C+8
34702
efa196219dd3 sorted;
wenzelm
parents: 34666
diff changeset
   276
sidekick-tree.dock-position=right
47590
8bdfacbc2fa2 some sidekick options for more advanced completion;
wenzelm
parents: 43287
diff changeset
   277
sidekick.auto-complete-popup-get-focus=true
34702
efa196219dd3 sorted;
wenzelm
parents: 34666
diff changeset
   278
sidekick.buffer-save-parse=true
50730
883963f45ac9 more reactive completion popup by default;
wenzelm
parents: 50728
diff changeset
   279
sidekick.complete-delay=0
47590
8bdfacbc2fa2 some sidekick options for more advanced completion;
wenzelm
parents: 43287
diff changeset
   280
sidekick.complete-instant.toggle=false
50730
883963f45ac9 more reactive completion popup by default;
wenzelm
parents: 50728
diff changeset
   281
sidekick.complete-popup.accept-characters=\\t
47590
8bdfacbc2fa2 some sidekick options for more advanced completion;
wenzelm
parents: 43287
diff changeset
   282
sidekick.complete-popup.insert-characters=
60269
652a8e72cb75 less confusing default;
wenzelm
parents: 60267
diff changeset
   283
sidekick.persistentFilter=true
60267
d496ab7e0136 prevent incoherent default in SideKick 1.7;
wenzelm
parents: 58785
diff changeset
   284
sidekick.showFilter=true
34880
f88fc4fcab86 provide JEDIT_SETTINGS via settings;
wenzelm
parents: 34814
diff changeset
   285
sidekick.splitter.location=721
50318
6be9e490d82a avoid odd warnings due to failure of systray icon;
wenzelm
parents: 50308
diff changeset
   286
systrayicon=false
34512
14d70378f1c7 modified netbeans build such that dist can be used as settings-directory for jedit;
immler@in.tum.de
parents: 34425
diff changeset
   287
tip.show=false
53188
bb5433b13ff2 some secondary shortcuts derived from 5.1.0/keymaps/German_Keyboard_keys.props (using CIRCUMFLEX instead of S+1);
wenzelm
parents: 53161
diff changeset
   288
toggle-multi-select.shortcut2=C+NUMBER_SIGN
bb5433b13ff2 some secondary shortcuts derived from 5.1.0/keymaps/German_Keyboard_keys.props (using CIRCUMFLEX instead of S+1);
wenzelm
parents: 53161
diff changeset
   289
toggle-rect-select.shortcut2=A+NUMBER_SIGN
36792
4cf537964010 disable two stage save by default, to avoid change of file permissions (notably the dreaded executable bit on Cygwin);
wenzelm
parents: 34881
diff changeset
   290
twoStageSave=false
50306
b655d2d0406d updated to jedit-5.0.0;
wenzelm
parents: 50299
diff changeset
   291
vfs.browser.dock-position=floating
60877
8d00ff5a052e sort lines;
wenzelm
parents: 60749
diff changeset
   292
vfs.favorite.0.type=1
56632
b3a2dedcc9ec favorites for jEdit file browser, although an expanded directory path is expected here, not environment variables;
wenzelm
parents: 56586
diff changeset
   293
vfs.favorite.0=$ISABELLE_HOME
60877
8d00ff5a052e sort lines;
wenzelm
parents: 60749
diff changeset
   294
vfs.favorite.1.type=1
56632
b3a2dedcc9ec favorites for jEdit file browser, although an expanded directory path is expected here, not environment variables;
wenzelm
parents: 56586
diff changeset
   295
vfs.favorite.1=$ISABELLE_HOME_USER
63749
4fe8cfaeb1fc clarified important directories;
wenzelm
parents: 63735
diff changeset
   296
vfs.favorite.2.type=1
4fe8cfaeb1fc clarified important directories;
wenzelm
parents: 63735
diff changeset
   297
vfs.favorite.2=$JEDIT_HOME
4fe8cfaeb1fc clarified important directories;
wenzelm
parents: 63735
diff changeset
   298
vfs.favorite.3.type=1
4fe8cfaeb1fc clarified important directories;
wenzelm
parents: 63735
diff changeset
   299
vfs.favorite.3=$JEDIT_SETTINGS
34334
68e172602b86 essential default properties for jEdit;
wenzelm
parents:
diff changeset
   300
view.antiAlias=standard
68e172602b86 essential default properties for jEdit;
wenzelm
parents:
diff changeset
   301
view.blockCaret=true
68e172602b86 essential default properties for jEdit;
wenzelm
parents:
diff changeset
   302
view.caretBlink=false
56907
0f3c375fd27c enable "PIDE" docking framework by default, and rely on its "Detach" menu item;
wenzelm
parents: 56892
diff changeset
   303
view.docking.framework=PIDE
34334
68e172602b86 essential default properties for jEdit;
wenzelm
parents:
diff changeset
   304
view.eolMarkers=false
68e172602b86 essential default properties for jEdit;
wenzelm
parents:
diff changeset
   305
view.extendedState=0
69343
395c4fb15ea2 use "Isabelle DejaVu" fonts uniformly: Text Area, GUI elements, HTML output etc.;
wenzelm
parents: 68080
diff changeset
   306
view.font=Isabelle DejaVu Sans Mono
34334
68e172602b86 essential default properties for jEdit;
wenzelm
parents:
diff changeset
   307
view.fontsize=18
34725
43b02b4c8e0b avoid fractional font metrics, which produces bad antialiasing with reletively new versions of jedit and java;
wenzelm
parents: 34702
diff changeset
   308
view.fracFontMetrics=false
69343
395c4fb15ea2 use "Isabelle DejaVu" fonts uniformly: Text Area, GUI elements, HTML output etc.;
wenzelm
parents: 68080
diff changeset
   309
view.gutter.font=Isabelle DejaVu Sans Mono
34334
68e172602b86 essential default properties for jEdit;
wenzelm
parents:
diff changeset
   310
view.gutter.fontsize=12
50306
b655d2d0406d updated to jedit-5.0.0;
wenzelm
parents: 50299
diff changeset
   311
view.gutter.lineNumbers=false
39176
b8fdd3ae8815 Document_View: more precise painting of gutter icons, only if line selection area is sufficiently large;
wenzelm
parents: 38261
diff changeset
   312
view.gutter.selectionAreaWidth=18
34880
f88fc4fcab86 provide JEDIT_SETTINGS via settings;
wenzelm
parents: 34814
diff changeset
   313
view.height=787
34334
68e172602b86 essential default properties for jEdit;
wenzelm
parents:
diff changeset
   314
view.middleMousePaste=true
56413
2d4d9a5f68ff support for jEdit Navigator plugin;
wenzelm
parents: 55558
diff changeset
   315
view.showToolbar=true
41631
8ff597b3dd80 do not restore old files on startup, which is potentially slow due to automatic rechecking;
wenzelm
parents: 40791
diff changeset
   316
view.thickCaret=true
34880
f88fc4fcab86 provide JEDIT_SETTINGS via settings;
wenzelm
parents: 34814
diff changeset
   317
view.width=1072
67647
27f3dceb5a70 avoid conflict with Isabelle/jEdit completion of '>', e.g. "-->", "==>";
wenzelm
parents: 67132
diff changeset
   318
xml-insert-closing-tag.shortcut=