src/Tools/jEdit/dist-template/properties/jedit.props
author wenzelm
Fri, 26 Jun 2009 20:54:42 +0200
changeset 34626 7124433be8be
parent 34623 a356a8ee6f00
child 34652 5fe5e00ec430
permissions -rw-r--r--
opt-out obscure encodings;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
34334
68e172602b86 essential default properties for jEdit;
wenzelm
parents:
diff changeset
     1
#jEdit properties
34626
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
     2
encoding.opt-out.Big5-HKSCS=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
     3
encoding.opt-out.Big5=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
     4
encoding.opt-out.COMPOUND_TEXT=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
     5
encoding.opt-out.EUC-JP=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
     6
encoding.opt-out.EUC-KR=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
     7
encoding.opt-out.GB18030=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
     8
encoding.opt-out.GB2312=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
     9
encoding.opt-out.GBK=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
    10
encoding.opt-out.IBM-Thai=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
    11
encoding.opt-out.IBM00858=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
    12
encoding.opt-out.IBM01140=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
    13
encoding.opt-out.IBM01141=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
    14
encoding.opt-out.IBM01142=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
    15
encoding.opt-out.IBM01143=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
    16
encoding.opt-out.IBM01144=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
    17
encoding.opt-out.IBM01145=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
    18
encoding.opt-out.IBM01146=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
    19
encoding.opt-out.IBM01147=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
    20
encoding.opt-out.IBM01148=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
    21
encoding.opt-out.IBM01149=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
    22
encoding.opt-out.IBM037=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
    23
encoding.opt-out.IBM1026=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
    24
encoding.opt-out.IBM1047=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
    25
encoding.opt-out.IBM273=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
    26
encoding.opt-out.IBM277=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
    27
encoding.opt-out.IBM278=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
    28
encoding.opt-out.IBM280=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
    29
encoding.opt-out.IBM284=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
    30
encoding.opt-out.IBM285=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
    31
encoding.opt-out.IBM297=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
    32
encoding.opt-out.IBM420=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
    33
encoding.opt-out.IBM424=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
    34
encoding.opt-out.IBM437=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
    35
encoding.opt-out.IBM500=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
    36
encoding.opt-out.IBM775=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
    37
encoding.opt-out.IBM850=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
    38
encoding.opt-out.IBM852=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
    39
encoding.opt-out.IBM855=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
    40
encoding.opt-out.IBM857=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
    41
encoding.opt-out.IBM860=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
    42
encoding.opt-out.IBM861=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
    43
encoding.opt-out.IBM862=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
    44
encoding.opt-out.IBM863=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
    45
encoding.opt-out.IBM864=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
    46
encoding.opt-out.IBM865=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
    47
encoding.opt-out.IBM866=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
    48
encoding.opt-out.IBM868=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
    49
encoding.opt-out.IBM869=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
    50
encoding.opt-out.IBM870=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
    51
encoding.opt-out.IBM871=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
    52
encoding.opt-out.IBM918=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
    53
encoding.opt-out.ISO-2022-CN=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
    54
encoding.opt-out.ISO-2022-JP-2=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
    55
encoding.opt-out.ISO-2022-JP=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
    56
encoding.opt-out.ISO-2022-KR=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
    57
encoding.opt-out.ISO-8859-13=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
    58
encoding.opt-out.ISO-8859-2=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
    59
encoding.opt-out.ISO-8859-3=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
    60
encoding.opt-out.ISO-8859-4=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
    61
encoding.opt-out.ISO-8859-5=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
    62
encoding.opt-out.ISO-8859-6=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
    63
encoding.opt-out.ISO-8859-7=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
    64
encoding.opt-out.ISO-8859-8=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
    65
encoding.opt-out.ISO-8859-9=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
    66
encoding.opt-out.JIS_X0201=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
    67
encoding.opt-out.JIS_X0212-1990=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
    68
encoding.opt-out.KOI8-R=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
    69
encoding.opt-out.KOI8-U=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
    70
encoding.opt-out.Shift_JIS=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
    71
encoding.opt-out.TIS-620=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
    72
encoding.opt-out.UTF-16=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
    73
encoding.opt-out.UTF-16BE=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
    74
encoding.opt-out.UTF-16LE=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
    75
encoding.opt-out.UTF-32=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
    76
encoding.opt-out.UTF-32BE=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
    77
encoding.opt-out.UTF-32LE=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
    78
encoding.opt-out.X-UTF-32BE-BOM=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
    79
encoding.opt-out.X-UTF-32LE-BOM=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
    80
encoding.opt-out.windows-1250=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
    81
encoding.opt-out.windows-1251=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
    82
encoding.opt-out.windows-1253=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
    83
encoding.opt-out.windows-1254=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
    84
encoding.opt-out.windows-1255=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
    85
encoding.opt-out.windows-1256=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
    86
encoding.opt-out.windows-1257=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
    87
encoding.opt-out.windows-1258=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
    88
encoding.opt-out.windows-31j=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
    89
encoding.opt-out.x-Big5-Solaris=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
    90
encoding.opt-out.x-EUC-TW=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
    91
encoding.opt-out.x-IBM1006=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
    92
encoding.opt-out.x-IBM1025=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
    93
encoding.opt-out.x-IBM1046=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
    94
encoding.opt-out.x-IBM1097=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
    95
encoding.opt-out.x-IBM1098=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
    96
encoding.opt-out.x-IBM1112=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
    97
encoding.opt-out.x-IBM1122=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
    98
encoding.opt-out.x-IBM1123=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
    99
encoding.opt-out.x-IBM1124=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
   100
encoding.opt-out.x-IBM1381=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
   101
encoding.opt-out.x-IBM1383=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
   102
encoding.opt-out.x-IBM33722=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
   103
encoding.opt-out.x-IBM737=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
   104
encoding.opt-out.x-IBM834=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
   105
encoding.opt-out.x-IBM856=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
   106
encoding.opt-out.x-IBM874=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
   107
encoding.opt-out.x-IBM875=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
   108
encoding.opt-out.x-IBM921=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
   109
encoding.opt-out.x-IBM922=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
   110
encoding.opt-out.x-IBM930=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
   111
encoding.opt-out.x-IBM933=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
   112
encoding.opt-out.x-IBM935=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
   113
encoding.opt-out.x-IBM937=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
   114
encoding.opt-out.x-IBM939=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
   115
encoding.opt-out.x-IBM942=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
   116
encoding.opt-out.x-IBM942C=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
   117
encoding.opt-out.x-IBM943=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
   118
encoding.opt-out.x-IBM943C=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
   119
encoding.opt-out.x-IBM948=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
   120
encoding.opt-out.x-IBM949=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
   121
encoding.opt-out.x-IBM949C=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
   122
encoding.opt-out.x-IBM950=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
   123
encoding.opt-out.x-IBM964=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
   124
encoding.opt-out.x-IBM970=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
   125
encoding.opt-out.x-ISCII91=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
   126
encoding.opt-out.x-ISO-2022-CN-CNS=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
   127
encoding.opt-out.x-ISO-2022-CN-GB=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
   128
encoding.opt-out.x-JIS0208=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
   129
encoding.opt-out.x-JISAutoDetect=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
   130
encoding.opt-out.x-Johab=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
   131
encoding.opt-out.x-MS932_0213=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
   132
encoding.opt-out.x-MS950-HKSCS=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
   133
encoding.opt-out.x-MacArabic=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
   134
encoding.opt-out.x-MacCentralEurope=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
   135
encoding.opt-out.x-MacCroatian=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
   136
encoding.opt-out.x-MacCyrillic=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
   137
encoding.opt-out.x-MacDingbat=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
   138
encoding.opt-out.x-MacGreek=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
   139
encoding.opt-out.x-MacHebrew=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
   140
encoding.opt-out.x-MacIceland=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
   141
encoding.opt-out.x-MacRoman=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
   142
encoding.opt-out.x-MacRomania=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
   143
encoding.opt-out.x-MacSymbol=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
   144
encoding.opt-out.x-MacThai=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
   145
encoding.opt-out.x-MacTurkish=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
   146
encoding.opt-out.x-MacUkraine=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
   147
encoding.opt-out.x-PCK=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
   148
encoding.opt-out.x-SJIS_0213=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
   149
encoding.opt-out.x-UTF-16LE-BOM=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
   150
encoding.opt-out.x-euc-jp-linux=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
   151
encoding.opt-out.x-eucJP-Open=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
   152
encoding.opt-out.x-iso-8859-11=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
   153
encoding.opt-out.x-mswin-936=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
   154
encoding.opt-out.x-windows-50220=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
   155
encoding.opt-out.x-windows-50221=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
   156
encoding.opt-out.x-windows-874=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
   157
encoding.opt-out.x-windows-949=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
   158
encoding.opt-out.x-windows-950=true
7124433be8be opt-out obscure encodings;
wenzelm
parents: 34623
diff changeset
   159
encoding.opt-out.x-windows-iso2022jp=true
34334
68e172602b86 essential default properties for jEdit;
wenzelm
parents:
diff changeset
   160
buffer.deepIndent=false
34623
a356a8ee6f00 renamed UTF-8-isabelle to UTF-8-Isabelle;
wenzelm
parents: 34619
diff changeset
   161
buffer.encoding=UTF-8-Isabelle
34334
68e172602b86 essential default properties for jEdit;
wenzelm
parents:
diff changeset
   162
buffer.indentSize=2
68e172602b86 essential default properties for jEdit;
wenzelm
parents:
diff changeset
   163
buffer.lineSeparator=\n
68e172602b86 essential default properties for jEdit;
wenzelm
parents:
diff changeset
   164
buffer.maxLineLen=100
68e172602b86 essential default properties for jEdit;
wenzelm
parents:
diff changeset
   165
buffer.noTabs=true
68e172602b86 essential default properties for jEdit;
wenzelm
parents:
diff changeset
   166
buffer.tabSize=2
34619
e89b6ec97910 added IsabelleEncoding -- a clone of utf-8 for now;
wenzelm
parents: 34613
diff changeset
   167
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
   168
firstTime=false
14d70378f1c7 modified netbeans build such that dist can be used as settings-directory for jedit;
immler@in.tum.de
parents: 34425
diff changeset
   169
tip.show=false
34334
68e172602b86 essential default properties for jEdit;
wenzelm
parents:
diff changeset
   170
encodingDetectors=BOM XML-PI buffer-local-property
68e172602b86 essential default properties for jEdit;
wenzelm
parents:
diff changeset
   171
delete-line.shortcut=A+d
68e172602b86 essential default properties for jEdit;
wenzelm
parents:
diff changeset
   172
delete.shortcut2=C+d
68e172602b86 essential default properties for jEdit;
wenzelm
parents:
diff changeset
   173
view.antiAlias=standard
68e172602b86 essential default properties for jEdit;
wenzelm
parents:
diff changeset
   174
view.blockCaret=true
68e172602b86 essential default properties for jEdit;
wenzelm
parents:
diff changeset
   175
view.caretBlink=false
68e172602b86 essential default properties for jEdit;
wenzelm
parents:
diff changeset
   176
view.eolMarkers=false
68e172602b86 essential default properties for jEdit;
wenzelm
parents:
diff changeset
   177
view.extendedState=0
68e172602b86 essential default properties for jEdit;
wenzelm
parents:
diff changeset
   178
view.font=Lucida Sans Typewriter
68e172602b86 essential default properties for jEdit;
wenzelm
parents:
diff changeset
   179
view.fontsize=18
68e172602b86 essential default properties for jEdit;
wenzelm
parents:
diff changeset
   180
view.fracFontMetrics=true
68e172602b86 essential default properties for jEdit;
wenzelm
parents:
diff changeset
   181
view.gutter.fontsize=12
68e172602b86 essential default properties for jEdit;
wenzelm
parents:
diff changeset
   182
view.middleMousePaste=true
68e172602b86 essential default properties for jEdit;
wenzelm
parents:
diff changeset
   183
view.showToolbar=false
34425
1a574ef87254 tuned sidekick properties;
wenzelm
parents: 34423
diff changeset
   184
buffer.sidekick.keystroke-parse=true
1a574ef87254 tuned sidekick properties;
wenzelm
parents: 34423
diff changeset
   185
sidekick.buffer-save-parse=true
34613
71fb6ab6ec57 default sidekick.complete-delay;
wenzelm
parents: 34556
diff changeset
   186
sidekick.complete-delay=300
34556
09a5984250a2 seperate node for syntax-highlighting
immler@in.tum.de
parents: 34512
diff changeset
   187
mode.isabelle.sidekick.showStatusWindow.label=true
34423
ec74cd63f7cb default docking of sidekick and isabelle-state;
wenzelm
parents: 34334
diff changeset
   188
sidekick-tree.dock-position=right
ec74cd63f7cb default docking of sidekick and isabelle-state;
wenzelm
parents: 34334
diff changeset
   189
isabelle-state.dock-position=bottom