Mercurial Mercurial > repos > isabelle / annotate
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Tools/jEdit/src/jEdit.props
author wenzelm
Wed, 25 Sep 2013 15:40:34 +0200
changeset 53883 f1c5f857df3d
parent 53772 30de372ca56f
child 53933 7924d61b50cf
permissions -rw-r--r--
include MacOSX plugin by default -- disabled by default to avoid multiplatform confusion;
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
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 
    10
 
close-docking-area.shortcut2=C+e C+CIRCUMFLEX
50796
2d68df7ed89d Console is not docked on startup;
wenzelm
parents: 50730
diff changeset 
    11
 
console.dock-position=floating
34880
f88fc4fcab86 provide JEDIT_SETTINGS via settings;
wenzelm
parents: 34814
diff changeset 
    12
 
console.encoding=UTF-8
f88fc4fcab86 provide JEDIT_SETTINGS via settings;
wenzelm
parents: 34814
diff changeset 
    13
 
console.font=IsabelleText
f88fc4fcab86 provide JEDIT_SETTINGS via settings;
wenzelm
parents: 34814
diff changeset 
    14
 
console.fontsize=14
34702
efa196219dd3 sorted;
wenzelm
parents: 34666
diff changeset 
    15
 
delete-line.shortcut=A+d
efa196219dd3 sorted;
wenzelm
parents: 34666
diff changeset 
    16
 
delete.shortcut2=C+d
34626
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset 
    17
 
encoding.opt-out.Big5-HKSCS=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset 
    18
 
encoding.opt-out.Big5=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset 
    19
 
encoding.opt-out.COMPOUND_TEXT=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset 
    20
 
encoding.opt-out.EUC-JP=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset 
    21
 
encoding.opt-out.EUC-KR=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset 
    22
 
encoding.opt-out.GB18030=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset 
    23
 
encoding.opt-out.GB2312=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset 
    24
 
encoding.opt-out.GBK=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset 
    25
 
encoding.opt-out.IBM-Thai=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset 
    26
 
encoding.opt-out.IBM00858=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset 
    27
 
encoding.opt-out.IBM01140=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset 
    28
 
encoding.opt-out.IBM01141=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset 
    29
 
encoding.opt-out.IBM01142=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset 
    30
 
encoding.opt-out.IBM01143=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset 
    31
 
encoding.opt-out.IBM01144=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset 
    32
 
encoding.opt-out.IBM01145=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset 
    33
 
encoding.opt-out.IBM01146=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset 
    34
 
encoding.opt-out.IBM01147=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset 
    35
 
encoding.opt-out.IBM01148=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset 
    36
 
encoding.opt-out.IBM01149=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset 
    37
 
encoding.opt-out.IBM037=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset 
    38
 
encoding.opt-out.IBM1026=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset 
    39
 
encoding.opt-out.IBM1047=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
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset 
    68
 
encoding.opt-out.ISO-2022-CN=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset 
    69
 
encoding.opt-out.ISO-2022-JP-2=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset 
    70
 
encoding.opt-out.ISO-2022-JP=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset 
    71
 
encoding.opt-out.ISO-2022-KR=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset 
    72
 
encoding.opt-out.ISO-8859-13=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset 
    73
 
encoding.opt-out.ISO-8859-2=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset 
    74
 
encoding.opt-out.ISO-8859-3=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset 
    75
 
encoding.opt-out.ISO-8859-4=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset 
    76
 
encoding.opt-out.ISO-8859-5=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset 
    77
 
encoding.opt-out.ISO-8859-6=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset 
    78
 
encoding.opt-out.ISO-8859-7=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset 
    79
 
encoding.opt-out.ISO-8859-8=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset 
    80
 
encoding.opt-out.ISO-8859-9=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset 
    81
 
encoding.opt-out.JIS_X0201=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset 
    82
 
encoding.opt-out.JIS_X0212-1990=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset 
    83
 
encoding.opt-out.KOI8-R=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset 
    84
 
encoding.opt-out.KOI8-U=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset 
    85
 
encoding.opt-out.Shift_JIS=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset 
    86
 
encoding.opt-out.TIS-620=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset 
    87
 
encoding.opt-out.UTF-16=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset 
    88
 
encoding.opt-out.UTF-16BE=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset 
    89
 
encoding.opt-out.UTF-16LE=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset 
    90
 
encoding.opt-out.UTF-32=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset 
    91
 
encoding.opt-out.UTF-32BE=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset 
    92
 
encoding.opt-out.UTF-32LE=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset 
    93
 
encoding.opt-out.X-UTF-32BE-BOM=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset 
    94
 
encoding.opt-out.X-UTF-32LE-BOM=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset 
    95
 
encoding.opt-out.windows-1250=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset 
    96
 
encoding.opt-out.windows-1251=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset 
    97
 
encoding.opt-out.windows-1253=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset 
    98
 
encoding.opt-out.windows-1254=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset 
    99
 
encoding.opt-out.windows-1255=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset 
   100
 
encoding.opt-out.windows-1256=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset 
   101
 
encoding.opt-out.windows-1257=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset 
   102
 
encoding.opt-out.windows-1258=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset 
   103
 
encoding.opt-out.windows-31j=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset 
   104
 
encoding.opt-out.x-Big5-Solaris=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset 
   105
 
encoding.opt-out.x-EUC-TW=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset 
   106
 
encoding.opt-out.x-IBM1006=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset 
   107
 
encoding.opt-out.x-IBM1025=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset 
   108
 
encoding.opt-out.x-IBM1046=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset 
   109
 
encoding.opt-out.x-IBM1097=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset 
   110
 
encoding.opt-out.x-IBM1098=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset 
   111
 
encoding.opt-out.x-IBM1112=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset 
   112
 
encoding.opt-out.x-IBM1122=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset 
   113
 
encoding.opt-out.x-IBM1123=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset 
   114
 
encoding.opt-out.x-IBM1124=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset 
   115
 
encoding.opt-out.x-IBM1381=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset 
   116
 
encoding.opt-out.x-IBM1383=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset 
   117
 
encoding.opt-out.x-IBM33722=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset 
   118
 
encoding.opt-out.x-IBM737=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset 
   119
 
encoding.opt-out.x-IBM834=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset 
   120
 
encoding.opt-out.x-IBM856=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset 
   121
 
encoding.opt-out.x-IBM874=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset 
   122
 
encoding.opt-out.x-IBM875=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset 
   123
 
encoding.opt-out.x-IBM921=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset 
   124
 
encoding.opt-out.x-IBM922=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset 
   125
 
encoding.opt-out.x-IBM930=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset 
   126
 
encoding.opt-out.x-IBM933=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset 
   127
 
encoding.opt-out.x-IBM935=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset 
   128
 
encoding.opt-out.x-IBM937=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset 
   129
 
encoding.opt-out.x-IBM939=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset 
   130
 
encoding.opt-out.x-IBM942=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset 
   131
 
encoding.opt-out.x-IBM942C=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset 
   132
 
encoding.opt-out.x-IBM943=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset 
   133
 
encoding.opt-out.x-IBM943C=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset 
   134
 
encoding.opt-out.x-IBM948=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset 
   135
 
encoding.opt-out.x-IBM949=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset 
   136
 
encoding.opt-out.x-IBM949C=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset 
   137
 
encoding.opt-out.x-IBM950=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset 
   138
 
encoding.opt-out.x-IBM964=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset 
   139
 
encoding.opt-out.x-IBM970=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset 
   140
 
encoding.opt-out.x-ISCII91=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset 
   141
 
encoding.opt-out.x-ISO-2022-CN-CNS=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset 
   142
 
encoding.opt-out.x-ISO-2022-CN-GB=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset 
   143
 
encoding.opt-out.x-JIS0208=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset 
   144
 
encoding.opt-out.x-JISAutoDetect=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset 
   145
 
encoding.opt-out.x-Johab=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset 
   146
 
encoding.opt-out.x-MS932_0213=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset 
   147
 
encoding.opt-out.x-MS950-HKSCS=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset 
   148
 
encoding.opt-out.x-MacArabic=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset 
   149
 
encoding.opt-out.x-MacCentralEurope=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset 
   150
 
encoding.opt-out.x-MacCroatian=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset 
   151
 
encoding.opt-out.x-MacCyrillic=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset 
   152
 
encoding.opt-out.x-MacDingbat=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset 
   153
 
encoding.opt-out.x-MacGreek=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset 
   154
 
encoding.opt-out.x-MacHebrew=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset 
   155
 
encoding.opt-out.x-MacIceland=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset 
   156
 
encoding.opt-out.x-MacRoman=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset 
   157
 
encoding.opt-out.x-MacRomania=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset 
   158
 
encoding.opt-out.x-MacSymbol=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset 
   159
 
encoding.opt-out.x-MacThai=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset 
   160
 
encoding.opt-out.x-MacTurkish=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset 
   161
 
encoding.opt-out.x-MacUkraine=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset 
   162
 
encoding.opt-out.x-PCK=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset 
   163
 
encoding.opt-out.x-SJIS_0213=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset 
   164
 
encoding.opt-out.x-UTF-16LE-BOM=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset 
   165
 
encoding.opt-out.x-euc-jp-linux=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset 
   166
 
encoding.opt-out.x-eucJP-Open=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset 
   167
 
encoding.opt-out.x-iso-8859-11=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset 
   168
 
encoding.opt-out.x-mswin-936=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset 
   169
 
encoding.opt-out.x-windows-50220=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset 
   170
 
encoding.opt-out.x-windows-50221=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
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset 
   174
 
encoding.opt-out.x-windows-iso2022jp=true
34702
efa196219dd3 sorted;
wenzelm
parents: 34666
diff changeset 
   175
 
encodingDetectors=BOM XML-PI buffer-local-property
37190
ea52509f4c42 more basic default behaviour of ENTER, HOME, END;
wenzelm
parents: 37162
diff changeset 
   176
 
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 
   177
 
expand-abbrev.shortcut2=CA+SPACE
34619
e89b6ec97910 added IsabelleEncoding -- a clone of utf-8 for now;
wenzelm
parents: 34613
diff changeset 
   178
 
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 
   179
 
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 
   180
 
focus-buffer-switcher.shortcut2=A+CIRCUMFLEX
37190
ea52509f4c42 more basic default behaviour of ENTER, HOME, END;
wenzelm
parents: 37162
diff changeset 
   181
 
home.shortcut=
ea52509f4c42 more basic default behaviour of ENTER, HOME, END;
wenzelm
parents: 37162
diff changeset 
   182
 
insert-newline-indent.shortcut=
ea52509f4c42 more basic default behaviour of ENTER, HOME, END;
wenzelm
parents: 37162
diff changeset 
   183
 
insert-newline.shortcut=ENTER
52947
a7947b72bac2 sorted lines;
wenzelm
parents: 52815
diff changeset 
   184
 
isabelle-documentation.dock-position=right
52948
383c1496d0aa Find is docked on startup;
wenzelm
parents: 52947
diff changeset 
   185
 
isabelle-find.dock-position=bottom
34880
f88fc4fcab86 provide JEDIT_SETTINGS via settings;
wenzelm
parents: 34814
diff changeset 
   186
 
isabelle-output.dock-position=bottom
39815
37bdc2220cf8 tuned default "Prover Session" perspective;
wenzelm
parents: 39739
diff changeset 
   187
 
isabelle-output.height=174
37bdc2220cf8 tuned default "Prover Session" perspective;
wenzelm
parents: 39739
diff changeset 
   188
 
isabelle-output.width=412
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 
   189
 
isabelle-sledgehammer.dock-position=bottom
50306
b655d2d0406d updated to jedit-5.0.0;
wenzelm
parents: 50299
diff changeset 
   190
 
isabelle-symbols.dock-position=bottom
50803
8a1ea6b00ace dock "Theories" right, although it might obscure some control buttons;
wenzelm
parents: 50796
diff changeset 
   191
 
isabelle-theories.dock-position=right
53293
fd27b8f5a479 added action isabelle.complete, using standard jEdit keyboard shortcut;
wenzelm
parents: 53188
diff changeset 
   192
 
isabelle.complete.label=Complete text
fd27b8f5a479 added action isabelle.complete, using standard jEdit keyboard shortcut;
wenzelm
parents: 53188
diff changeset 
   193
 
isabelle.complete.shortcut=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 
   194
 
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 
   195
 
isabelle.control-bold.shortcut=C+e RIGHT
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 
   196
 
isabelle.control-reset.label=Control reset
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 
   197
 
isabelle.control-reset.shortcut=C+e LEFT
53021
d0fa3f446b9d discontinued special treatment of \<^isub> and \<^isup> in rendering or editor front-end;
wenzelm
parents: 52948
diff changeset 
   198
 
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 
   199
 
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 
   200
 
isabelle.control-sup.label=Control superscript
7d8406ebe18f odd bias of sub/superscript keyboard shortcuts -- according to frequency of use;
wenzelm
parents: 50492
diff changeset 
   201
 
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 
   202
 
isabelle.decrease-font-size.label=Decrease font size
51069
2f50ddd3b586 more portable alternative shortcuts on numeric keypad;
wenzelm
parents: 50803
diff changeset 
   203
 
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 
   204
 
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 
   205
 
isabelle.decrease-font-size2.label=Decrease font size (clone)
50308
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.increase-font-size.label=Increase font size
51069
2f50ddd3b586 more portable alternative shortcuts on numeric keypad;
wenzelm
parents: 50803
diff changeset 
   207
 
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 
   208
 
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 
   209
 
isabelle.increase-font-size2.label=Increase font size (clone)
52947
a7947b72bac2 sorted lines;
wenzelm
parents: 52815
diff changeset 
   210
 
isabelle.increase-font-size2.shortcut=C+EQUALS
a7947b72bac2 sorted lines;
wenzelm
parents: 52815
diff changeset 
   211
 
isabelle.reset-continuous-checking.label=Reset continuous checking
53161
051cbf663b5f added action isabelle.reset-font-size;
wenzelm
parents: 53058
diff changeset 
   212
 
isabelle.reset-font-size.label=Reset font size
051cbf663b5f added action isabelle.reset-font-size;
wenzelm
parents: 53058
diff changeset 
   213
 
isabelle.reset-font-size.shortcut=C+0
52947
a7947b72bac2 sorted lines;
wenzelm
parents: 52815
diff changeset 
   214
 
isabelle.reset-node-required.label=Reset node required
a7947b72bac2 sorted lines;
wenzelm
parents: 52815
diff changeset 
   215
 
isabelle.set-continuous-checking.label=Set continuous checking
a7947b72bac2 sorted lines;
wenzelm
parents: 52815
diff changeset 
   216
 
isabelle.set-node-required.label=Set node required
a7947b72bac2 sorted lines;
wenzelm
parents: 52815
diff changeset 
   217
 
isabelle.toggle-continuous-checking.label=Toggle continuous checking
a7947b72bac2 sorted lines;
wenzelm
parents: 52815
diff changeset 
   218
 
isabelle.toggle-continuous-checking.shortcut=C+e ENTER
a7947b72bac2 sorted lines;
wenzelm
parents: 52815
diff changeset 
   219
 
isabelle.toggle-node-required.label=Toggle node required
a7947b72bac2 sorted lines;
wenzelm
parents: 52815
diff changeset 
   220
 
isabelle.toggle-node-required.shortcut=C+e SPACE
50306
b655d2d0406d updated to jedit-5.0.0;
wenzelm
parents: 50299
diff changeset 
   221
 
lang.usedefaultlocale=false
b655d2d0406d updated to jedit-5.0.0;
wenzelm
parents: 50299
diff changeset 
   222
 
largefilemode=full
37190
ea52509f4c42 more basic default behaviour of ENTER, HOME, END;
wenzelm
parents: 37162
diff changeset 
   223
 
line-end.shortcut=END
ea52509f4c42 more basic default behaviour of ENTER, HOME, END;
wenzelm
parents: 37162
diff changeset 
   224
 
line-home.shortcut=HOME
50306
b655d2d0406d updated to jedit-5.0.0;
wenzelm
parents: 50299
diff changeset 
   225
 
lookAndFeel=javax.swing.plaf.nimbus.NimbusLookAndFeel
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 
   226
 
match-bracket.shortcut2=C+9
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 
   227
 
next-bracket.shortcut2=C+e C+9
53883
f1c5f857df3d include MacOSX plugin by default -- disabled by default to avoid multiplatform confusion;
wenzelm
parents: 53772
diff changeset 
   228
 
plugin-blacklist.MacOSX.jar=true
50728
e7b2cfcef94c updated to jedit_build-20130104;
wenzelm
parents: 50506
diff changeset 
   229
 
plugin.MacOSXPlugin.altDispatcher=false
50492
8d8e882c7fbe prevent dedicated MacOSX plugin from switching off vital workarounds;
wenzelm
parents: 50354
diff changeset 
   230
 
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 
   231
 
prev-bracket.shortcut2=C+e C+8
37162
88255b98a22f also set font for printing, which actually works out of the box;
wenzelm
parents: 36792
diff changeset 
   232
 
print.font=IsabelleText
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 
   233
 
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 
   234
 
restore.remote=false
8ff597b3dd80 do not restore old files on startup, which is potentially slow due to automatic rechecking;
wenzelm
parents: 40791
diff changeset 
   235
 
restore=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 
   236
 
select-block.shortcut2=C+8
34702
efa196219dd3 sorted;
wenzelm
parents: 34666
diff changeset 
   237
 
sidekick-tree.dock-position=right
47590
8bdfacbc2fa2 some sidekick options for more advanced completion;
wenzelm
parents: 43287
diff changeset 
   238
 
sidekick.auto-complete-popup-get-focus=true
34702
efa196219dd3 sorted;
wenzelm
parents: 34666
diff changeset 
   239
 
sidekick.buffer-save-parse=true
50730
883963f45ac9 more reactive completion popup by default;
wenzelm
parents: 50728
diff changeset 
   240
 
sidekick.complete-delay=0
47590
8bdfacbc2fa2 some sidekick options for more advanced completion;
wenzelm
parents: 43287
diff changeset 
   241
 
sidekick.complete-instant.toggle=false
50730
883963f45ac9 more reactive completion popup by default;
wenzelm
parents: 50728
diff changeset 
   242
 
sidekick.complete-popup.accept-characters=\\t
47590
8bdfacbc2fa2 some sidekick options for more advanced completion;
wenzelm
parents: 43287
diff changeset 
   243
 
sidekick.complete-popup.insert-characters=
34880
f88fc4fcab86 provide JEDIT_SETTINGS via settings;
wenzelm
parents: 34814
diff changeset 
   244
 
sidekick.splitter.location=721
50318
6be9e490d82a avoid odd warnings due to failure of systray icon;
wenzelm
parents: 50308
diff changeset 
   245
 
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 
   246
 
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 
   247
 
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 
   248
 
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 
   249
 
twoStageSave=false
50306
b655d2d0406d updated to jedit-5.0.0;
wenzelm
parents: 50299
diff changeset 
   250
 
vfs.browser.dock-position=floating
34334
68e172602b86 essential default properties for jEdit;
wenzelm
parents:
diff changeset 
   251
 
view.antiAlias=standard
68e172602b86 essential default properties for jEdit;
wenzelm
parents:
diff changeset 
   252
 
view.blockCaret=true
68e172602b86 essential default properties for jEdit;
wenzelm
parents:
diff changeset 
   253
 
view.caretBlink=false
68e172602b86 essential default properties for jEdit;
wenzelm
parents:
diff changeset 
   254
 
view.eolMarkers=false
68e172602b86 essential default properties for jEdit;
wenzelm
parents:
diff changeset 
   255
 
view.extendedState=0
34753
dd8bdcb7dcba use IsabelleText by default;
wenzelm
parents: 34725
diff changeset 
   256
 
view.font=IsabelleText
34334
68e172602b86 essential default properties for jEdit;
wenzelm
parents:
diff changeset 
   257
 
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 
   258
 
view.fracFontMetrics=false
34334
68e172602b86 essential default properties for jEdit;
wenzelm
parents:
diff changeset 
   259
 
view.gutter.fontsize=12
50306
b655d2d0406d updated to jedit-5.0.0;
wenzelm
parents: 50299
diff changeset 
   260
 
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 
   261
 
view.gutter.selectionAreaWidth=18
34880
f88fc4fcab86 provide JEDIT_SETTINGS via settings;
wenzelm
parents: 34814
diff changeset 
   262
 
view.height=787
34334
68e172602b86 essential default properties for jEdit;
wenzelm
parents:
diff changeset 
   263
 
view.middleMousePaste=true
68e172602b86 essential default properties for jEdit;
wenzelm
parents:
diff changeset 
   264
 
view.showToolbar=false
41631
8ff597b3dd80 do not restore old files on startup, which is potentially slow due to automatic rechecking;
wenzelm
parents: 40791
diff changeset 
   265
 
view.thickCaret=true
34880
f88fc4fcab86 provide JEDIT_SETTINGS via settings;
wenzelm
parents: 34814
diff changeset 
   266
 
view.width=1072
isabelle