src/Pure/Admin/build_jedit.scala
changeset 73983 e2913fc81142
parent 73982 c1277bb04507
child 73987 fc363a3b690a
equal deleted inserted replaced
73982:c1277bb04507 73983:e2913fc81142
     3 
     3 
     4 Build auxiliary jEdit component.
     4 Build auxiliary jEdit component.
     5 */
     5 */
     6 
     6 
     7 package isabelle
     7 package isabelle
       
     8 
       
     9 
       
    10 import java.nio.charset.Charset
       
    11 
       
    12 import scala.jdk.CollectionConverters._
     8 
    13 
     9 
    14 
    10 object Build_JEdit
    15 object Build_JEdit
    11 {
    16 {
    12   /* modes */
    17   /* modes */
   194       })
   199       })
   195     }
   200     }
   196 
   201 
   197 
   202 
   198     /* resources */
   203     /* resources */
       
   204 
       
   205     val keep_encodings = List("ISO-8859-1", "ISO-8859-15", "US-ASCII", "UTF-8", "windows-1252")
       
   206     val drop_encodings =
       
   207       Charset.availableCharsets().keySet().asScala.toList.sorted.filterNot(keep_encodings.contains)
   199 
   208 
   200     File.write(jedit_patched_dir + Path.explode("properties/jEdit.props"),
   209     File.write(jedit_patched_dir + Path.explode("properties/jEdit.props"),
   201 """#jEdit properties
   210 """#jEdit properties
   202 autoReloadDialog=false
   211 autoReloadDialog=false
   203 buffer.deepIndent=false
   212 buffer.deepIndent=false
   215 console.encoding=UTF-8
   224 console.encoding=UTF-8
   216 console.font=Isabelle DejaVu Sans Mono
   225 console.font=Isabelle DejaVu Sans Mono
   217 console.fontsize=14
   226 console.fontsize=14
   218 delete-line.shortcut=A+d
   227 delete-line.shortcut=A+d
   219 delete.shortcut2=C+d
   228 delete.shortcut2=C+d
   220 encoding.opt-out.Big5-HKSCS=true
   229 """ + drop_encodings.map(a => "encoding.opt-out." + a + "=true").mkString("\n") + """
   221 encoding.opt-out.Big5=true
       
   222 encoding.opt-out.COMPOUND_TEXT=true
       
   223 encoding.opt-out.EUC-JP=true
       
   224 encoding.opt-out.EUC-KR=true
       
   225 encoding.opt-out.GB2312=true
       
   226 encoding.opt-out.GB18030=true
       
   227 encoding.opt-out.GBK=true
       
   228 encoding.opt-out.IBM-Thai=true
       
   229 encoding.opt-out.IBM00858=true
       
   230 encoding.opt-out.IBM037=true
       
   231 encoding.opt-out.IBM01140=true
       
   232 encoding.opt-out.IBM01141=true
       
   233 encoding.opt-out.IBM01142=true
       
   234 encoding.opt-out.IBM01143=true
       
   235 encoding.opt-out.IBM01144=true
       
   236 encoding.opt-out.IBM01145=true
       
   237 encoding.opt-out.IBM01146=true
       
   238 encoding.opt-out.IBM01147=true
       
   239 encoding.opt-out.IBM01148=true
       
   240 encoding.opt-out.IBM01149=true
       
   241 encoding.opt-out.IBM273=true
       
   242 encoding.opt-out.IBM277=true
       
   243 encoding.opt-out.IBM278=true
       
   244 encoding.opt-out.IBM280=true
       
   245 encoding.opt-out.IBM284=true
       
   246 encoding.opt-out.IBM285=true
       
   247 encoding.opt-out.IBM297=true
       
   248 encoding.opt-out.IBM420=true
       
   249 encoding.opt-out.IBM424=true
       
   250 encoding.opt-out.IBM437=true
       
   251 encoding.opt-out.IBM500=true
       
   252 encoding.opt-out.IBM775=true
       
   253 encoding.opt-out.IBM850=true
       
   254 encoding.opt-out.IBM852=true
       
   255 encoding.opt-out.IBM855=true
       
   256 encoding.opt-out.IBM857=true
       
   257 encoding.opt-out.IBM860=true
       
   258 encoding.opt-out.IBM861=true
       
   259 encoding.opt-out.IBM862=true
       
   260 encoding.opt-out.IBM863=true
       
   261 encoding.opt-out.IBM864=true
       
   262 encoding.opt-out.IBM865=true
       
   263 encoding.opt-out.IBM866=true
       
   264 encoding.opt-out.IBM868=true
       
   265 encoding.opt-out.IBM869=true
       
   266 encoding.opt-out.IBM870=true
       
   267 encoding.opt-out.IBM871=true
       
   268 encoding.opt-out.IBM918=true
       
   269 encoding.opt-out.IBM1026=true
       
   270 encoding.opt-out.IBM1047=true
       
   271 encoding.opt-out.ISO-2022-CN=true
       
   272 encoding.opt-out.ISO-2022-JP-2=true
       
   273 encoding.opt-out.ISO-2022-JP=true
       
   274 encoding.opt-out.ISO-2022-KR=true
       
   275 encoding.opt-out.ISO-8859-2=true
       
   276 encoding.opt-out.ISO-8859-3=true
       
   277 encoding.opt-out.ISO-8859-4=true
       
   278 encoding.opt-out.ISO-8859-5=true
       
   279 encoding.opt-out.ISO-8859-6=true
       
   280 encoding.opt-out.ISO-8859-7=true
       
   281 encoding.opt-out.ISO-8859-8=true
       
   282 encoding.opt-out.ISO-8859-9=true
       
   283 encoding.opt-out.ISO-8859-13=true
       
   284 encoding.opt-out.JIS_X0201=true
       
   285 encoding.opt-out.JIS_X0212-1990=true
       
   286 encoding.opt-out.KOI8-R=true
       
   287 encoding.opt-out.KOI8-U=true
       
   288 encoding.opt-out.Shift_JIS=true
       
   289 encoding.opt-out.TIS-620=true
       
   290 encoding.opt-out.UTF-16=true
       
   291 encoding.opt-out.UTF-16BE=true
       
   292 encoding.opt-out.UTF-16LE=true
       
   293 encoding.opt-out.UTF-32=true
       
   294 encoding.opt-out.UTF-32BE=true
       
   295 encoding.opt-out.UTF-32LE=true
       
   296 encoding.opt-out.X-UTF-32BE-BOM=true
       
   297 encoding.opt-out.X-UTF-32LE-BOM=true
       
   298 encoding.opt-out.windows-31j=true
       
   299 encoding.opt-out.windows-1250=true
       
   300 encoding.opt-out.windows-1251=true
       
   301 encoding.opt-out.windows-1253=true
       
   302 encoding.opt-out.windows-1254=true
       
   303 encoding.opt-out.windows-1255=true
       
   304 encoding.opt-out.windows-1256=true
       
   305 encoding.opt-out.windows-1257=true
       
   306 encoding.opt-out.windows-1258=true
       
   307 encoding.opt-out.x-Big5-Solaris=true
       
   308 encoding.opt-out.x-EUC-TW=true
       
   309 encoding.opt-out.x-IBM737=true
       
   310 encoding.opt-out.x-IBM834=true
       
   311 encoding.opt-out.x-IBM856=true
       
   312 encoding.opt-out.x-IBM874=true
       
   313 encoding.opt-out.x-IBM875=true
       
   314 encoding.opt-out.x-IBM921=true
       
   315 encoding.opt-out.x-IBM922=true
       
   316 encoding.opt-out.x-IBM930=true
       
   317 encoding.opt-out.x-IBM933=true
       
   318 encoding.opt-out.x-IBM935=true
       
   319 encoding.opt-out.x-IBM937=true
       
   320 encoding.opt-out.x-IBM939=true
       
   321 encoding.opt-out.x-IBM942=true
       
   322 encoding.opt-out.x-IBM942C=true
       
   323 encoding.opt-out.x-IBM943=true
       
   324 encoding.opt-out.x-IBM943C=true
       
   325 encoding.opt-out.x-IBM948=true
       
   326 encoding.opt-out.x-IBM949=true
       
   327 encoding.opt-out.x-IBM949C=true
       
   328 encoding.opt-out.x-IBM950=true
       
   329 encoding.opt-out.x-IBM964=true
       
   330 encoding.opt-out.x-IBM970=true
       
   331 encoding.opt-out.x-IBM1006=true
       
   332 encoding.opt-out.x-IBM1025=true
       
   333 encoding.opt-out.x-IBM1046=true
       
   334 encoding.opt-out.x-IBM1097=true
       
   335 encoding.opt-out.x-IBM1098=true
       
   336 encoding.opt-out.x-IBM1112=true
       
   337 encoding.opt-out.x-IBM1122=true
       
   338 encoding.opt-out.x-IBM1123=true
       
   339 encoding.opt-out.x-IBM1124=true
       
   340 encoding.opt-out.x-IBM1381=true
       
   341 encoding.opt-out.x-IBM1383=true
       
   342 encoding.opt-out.x-IBM33722=true
       
   343 encoding.opt-out.x-ISCII91=true
       
   344 encoding.opt-out.x-ISO-2022-CN-CNS=true
       
   345 encoding.opt-out.x-ISO-2022-CN-GB=true
       
   346 encoding.opt-out.x-JIS0208=true
       
   347 encoding.opt-out.x-JISAutoDetect=true
       
   348 encoding.opt-out.x-Johab=true
       
   349 encoding.opt-out.x-MS932_0213=true
       
   350 encoding.opt-out.x-MS950-HKSCS=true
       
   351 encoding.opt-out.x-MacArabic=true
       
   352 encoding.opt-out.x-MacCentralEurope=true
       
   353 encoding.opt-out.x-MacCroatian=true
       
   354 encoding.opt-out.x-MacCyrillic=true
       
   355 encoding.opt-out.x-MacDingbat=true
       
   356 encoding.opt-out.x-MacGreek=true
       
   357 encoding.opt-out.x-MacHebrew=true
       
   358 encoding.opt-out.x-MacIceland=true
       
   359 encoding.opt-out.x-MacRoman=true
       
   360 encoding.opt-out.x-MacRomania=true
       
   361 encoding.opt-out.x-MacSymbol=true
       
   362 encoding.opt-out.x-MacThai=true
       
   363 encoding.opt-out.x-MacTurkish=true
       
   364 encoding.opt-out.x-MacUkraine=true
       
   365 encoding.opt-out.x-PCK=true
       
   366 encoding.opt-out.x-SJIS_0213=true
       
   367 encoding.opt-out.x-UTF-16LE-BOM=true
       
   368 encoding.opt-out.x-euc-jp-linux=true
       
   369 encoding.opt-out.x-eucJP-Open=true
       
   370 encoding.opt-out.x-iso-8859-11=true
       
   371 encoding.opt-out.x-mswin-936=true
       
   372 encoding.opt-out.x-windows-874=true
       
   373 encoding.opt-out.x-windows-949=true
       
   374 encoding.opt-out.x-windows-950=true
       
   375 encoding.opt-out.x-windows-50220=true
       
   376 encoding.opt-out.x-windows-50221=true
       
   377 encoding.opt-out.x-windows-iso2022jp=true
       
   378 encodingDetectors=BOM XML-PI buffer-local-property
   230 encodingDetectors=BOM XML-PI buffer-local-property
   379 end.shortcut=
   231 end.shortcut=
   380 expand-abbrev.shortcut2=CA+SPACE
   232 expand-abbrev.shortcut2=CA+SPACE
   381 expand-folds.shortcut=
   233 expand-folds.shortcut=
   382 fallbackEncodings=UTF-8 ISO-8859-15 US-ASCII
   234 fallbackEncodings=UTF-8 ISO-8859-15 US-ASCII