wneuper/isa: src/Tools/jEdit/dist-template/properties/jedit.props@6e44af45b8c5

     1 #jEdit properties

     2 buffer.deepIndent=false

     3 buffer.encoding=UTF-8-Isabelle

     4 buffer.indentSize=2

     5 buffer.lineSeparator=\n

     6 buffer.maxLineLen=100

     7 buffer.noTabs=true

     8 buffer.sidekick.keystroke-parse=true

     9 buffer.tabSize=2

    10 console.dock-position=bottom

    11 console.encoding=UTF-8

    12 console.font=IsabelleText

    13 console.fontsize=14

    14 console.height=174

    15 console.width=412

    16 delete-line.shortcut=A+d

    17 delete.shortcut2=C+d

    18 encoding.opt-out.Big5-HKSCS=true

    19 encoding.opt-out.Big5=true

    20 encoding.opt-out.COMPOUND_TEXT=true

    21 encoding.opt-out.EUC-JP=true

    22 encoding.opt-out.EUC-KR=true

    23 encoding.opt-out.GB18030=true

    24 encoding.opt-out.GB2312=true

    25 encoding.opt-out.GBK=true

    26 encoding.opt-out.IBM-Thai=true

    27 encoding.opt-out.IBM00858=true

    28 encoding.opt-out.IBM01140=true

    29 encoding.opt-out.IBM01141=true

    30 encoding.opt-out.IBM01142=true

    31 encoding.opt-out.IBM01143=true

    32 encoding.opt-out.IBM01144=true

    33 encoding.opt-out.IBM01145=true

    34 encoding.opt-out.IBM01146=true

    35 encoding.opt-out.IBM01147=true

    36 encoding.opt-out.IBM01148=true

    37 encoding.opt-out.IBM01149=true

    38 encoding.opt-out.IBM037=true

    39 encoding.opt-out.IBM1026=true

    40 encoding.opt-out.IBM1047=true

    41 encoding.opt-out.IBM273=true

    42 encoding.opt-out.IBM277=true

    43 encoding.opt-out.IBM278=true

    44 encoding.opt-out.IBM280=true

    45 encoding.opt-out.IBM284=true

    46 encoding.opt-out.IBM285=true

    47 encoding.opt-out.IBM297=true

    48 encoding.opt-out.IBM420=true

    49 encoding.opt-out.IBM424=true

    50 encoding.opt-out.IBM437=true

    51 encoding.opt-out.IBM500=true

    52 encoding.opt-out.IBM775=true

    53 encoding.opt-out.IBM850=true

    54 encoding.opt-out.IBM852=true

    55 encoding.opt-out.IBM855=true

    56 encoding.opt-out.IBM857=true

    57 encoding.opt-out.IBM860=true

    58 encoding.opt-out.IBM861=true

    59 encoding.opt-out.IBM862=true

    60 encoding.opt-out.IBM863=true

    61 encoding.opt-out.IBM864=true

    62 encoding.opt-out.IBM865=true

    63 encoding.opt-out.IBM866=true

    64 encoding.opt-out.IBM868=true

    65 encoding.opt-out.IBM869=true

    66 encoding.opt-out.IBM870=true

    67 encoding.opt-out.IBM871=true

    68 encoding.opt-out.IBM918=true

    69 encoding.opt-out.ISO-2022-CN=true

    70 encoding.opt-out.ISO-2022-JP-2=true

    71 encoding.opt-out.ISO-2022-JP=true

    72 encoding.opt-out.ISO-2022-KR=true

    73 encoding.opt-out.ISO-8859-13=true

    74 encoding.opt-out.ISO-8859-2=true

    75 encoding.opt-out.ISO-8859-3=true

    76 encoding.opt-out.ISO-8859-4=true

    77 encoding.opt-out.ISO-8859-5=true

    78 encoding.opt-out.ISO-8859-6=true

    79 encoding.opt-out.ISO-8859-7=true

    80 encoding.opt-out.ISO-8859-8=true

    81 encoding.opt-out.ISO-8859-9=true

    82 encoding.opt-out.JIS_X0201=true

    83 encoding.opt-out.JIS_X0212-1990=true

    84 encoding.opt-out.KOI8-R=true

    85 encoding.opt-out.KOI8-U=true

    86 encoding.opt-out.Shift_JIS=true

    87 encoding.opt-out.TIS-620=true

    88 encoding.opt-out.UTF-16=true

    89 encoding.opt-out.UTF-16BE=true

    90 encoding.opt-out.UTF-16LE=true

    91 encoding.opt-out.UTF-32=true

    92 encoding.opt-out.UTF-32BE=true

    93 encoding.opt-out.UTF-32LE=true

    94 encoding.opt-out.X-UTF-32BE-BOM=true

    95 encoding.opt-out.X-UTF-32LE-BOM=true

    96 encoding.opt-out.windows-1250=true

    97 encoding.opt-out.windows-1251=true

    98 encoding.opt-out.windows-1253=true

    99 encoding.opt-out.windows-1254=true

   100 encoding.opt-out.windows-1255=true

   101 encoding.opt-out.windows-1256=true

   102 encoding.opt-out.windows-1257=true

   103 encoding.opt-out.windows-1258=true

   104 encoding.opt-out.windows-31j=true

   105 encoding.opt-out.x-Big5-Solaris=true

   106 encoding.opt-out.x-EUC-TW=true

   107 encoding.opt-out.x-IBM1006=true

   108 encoding.opt-out.x-IBM1025=true

   109 encoding.opt-out.x-IBM1046=true

   110 encoding.opt-out.x-IBM1097=true

   111 encoding.opt-out.x-IBM1098=true

   112 encoding.opt-out.x-IBM1112=true

   113 encoding.opt-out.x-IBM1122=true

   114 encoding.opt-out.x-IBM1123=true

   115 encoding.opt-out.x-IBM1124=true

   116 encoding.opt-out.x-IBM1381=true

   117 encoding.opt-out.x-IBM1383=true

   118 encoding.opt-out.x-IBM33722=true

   119 encoding.opt-out.x-IBM737=true

   120 encoding.opt-out.x-IBM834=true

   121 encoding.opt-out.x-IBM856=true

   122 encoding.opt-out.x-IBM874=true

   123 encoding.opt-out.x-IBM875=true

   124 encoding.opt-out.x-IBM921=true

   125 encoding.opt-out.x-IBM922=true

   126 encoding.opt-out.x-IBM930=true

   127 encoding.opt-out.x-IBM933=true

   128 encoding.opt-out.x-IBM935=true

   129 encoding.opt-out.x-IBM937=true

   130 encoding.opt-out.x-IBM939=true

   131 encoding.opt-out.x-IBM942=true

   132 encoding.opt-out.x-IBM942C=true

   133 encoding.opt-out.x-IBM943=true

   134 encoding.opt-out.x-IBM943C=true

   135 encoding.opt-out.x-IBM948=true

   136 encoding.opt-out.x-IBM949=true

   137 encoding.opt-out.x-IBM949C=true

   138 encoding.opt-out.x-IBM950=true

   139 encoding.opt-out.x-IBM964=true

   140 encoding.opt-out.x-IBM970=true

   141 encoding.opt-out.x-ISCII91=true

   142 encoding.opt-out.x-ISO-2022-CN-CNS=true

   143 encoding.opt-out.x-ISO-2022-CN-GB=true

   144 encoding.opt-out.x-JIS0208=true

   145 encoding.opt-out.x-JISAutoDetect=true

   146 encoding.opt-out.x-Johab=true

   147 encoding.opt-out.x-MS932_0213=true

   148 encoding.opt-out.x-MS950-HKSCS=true

   149 encoding.opt-out.x-MacArabic=true

   150 encoding.opt-out.x-MacCentralEurope=true

   151 encoding.opt-out.x-MacCroatian=true

   152 encoding.opt-out.x-MacCyrillic=true

   153 encoding.opt-out.x-MacDingbat=true

   154 encoding.opt-out.x-MacGreek=true

   155 encoding.opt-out.x-MacHebrew=true

   156 encoding.opt-out.x-MacIceland=true

   157 encoding.opt-out.x-MacRoman=true

   158 encoding.opt-out.x-MacRomania=true

   159 encoding.opt-out.x-MacSymbol=true

   160 encoding.opt-out.x-MacThai=true

   161 encoding.opt-out.x-MacTurkish=true

   162 encoding.opt-out.x-MacUkraine=true

   163 encoding.opt-out.x-PCK=true

   164 encoding.opt-out.x-SJIS_0213=true

   165 encoding.opt-out.x-UTF-16LE-BOM=true

   166 encoding.opt-out.x-euc-jp-linux=true

   167 encoding.opt-out.x-eucJP-Open=true

   168 encoding.opt-out.x-iso-8859-11=true

   169 encoding.opt-out.x-mswin-936=true

   170 encoding.opt-out.x-windows-50220=true

   171 encoding.opt-out.x-windows-50221=true

   172 encoding.opt-out.x-windows-874=true

   173 encoding.opt-out.x-windows-949=true

   174 encoding.opt-out.x-windows-950=true

   175 encoding.opt-out.x-windows-iso2022jp=true

   176 encodingDetectors=BOM XML-PI buffer-local-property

   177 end.shortcut=

   178 fallbackEncodings=UTF-8 ISO-8859-15 US-ASCII

   179 firstTime=false

   180 home.shortcut=

   181 insert-newline-indent.shortcut=

   182 insert-newline.shortcut=ENTER

   183 isabelle-output.dock-position=bottom

   184 isabelle-raw-output.dock-position=bottom

   185 isabelle.activate.shortcut=CS+ENTER

   186 line-end.shortcut=END

   187 line-home.shortcut=HOME

   188 mode.isabelle.sidekick.showStatusWindow.label=true

   189 print.font=IsabelleText

   190 sidekick-tree.dock-position=right

   191 sidekick.buffer-save-parse=true

   192 sidekick.complete-delay=300

   193 sidekick.splitter.location=721

   194 tip.show=false

   195 twoStageSave=false

   196 view.antiAlias=standard

   197 view.blockCaret=true

   198 view.caretBlink=false

   199 view.eolMarkers=false

   200 view.extendedState=0

   201 view.font=IsabelleText

   202 view.fontsize=18

   203 view.fracFontMetrics=false

   204 view.gutter.fontsize=12

   205 view.height=787

   206 view.middleMousePaste=true

   207 view.showToolbar=false

   208 view.width=1072

author	wenzelm
	Thu, 03 Jun 2010 22:54:33 +0200
changeset 37308	6e44af45b8c5
parent 37191	ea52509f4c42
child 38559	4863a3816fc1
permissions	-rw-r--r--