equal
deleted
inserted
replaced
410 Debug.DISABLE_SEARCH_DIALOG_POOL = true |
410 Debug.DISABLE_SEARCH_DIALOG_POOL = true |
411 |
411 |
412 |
412 |
413 /* strict initialization */ |
413 /* strict initialization */ |
414 |
414 |
415 // adhoc patch of confusing message |
|
416 val orig_plugin_error = jEdit.getProperty("plugin-error.start-error") |
|
417 jEdit.setProperty("plugin-error.start-error", "Cannot start plugin: {0}") |
|
418 |
|
419 init_options() |
415 init_options() |
420 init_resources() |
416 init_resources() |
421 init_session() |
417 init_session() |
422 PIDE._plugin = this |
418 PIDE._plugin = this |
423 |
|
424 jEdit.setProperty("plugin-error.start-error", orig_plugin_error) |
|
425 |
419 |
426 |
420 |
427 /* non-strict initialization */ |
421 /* non-strict initialization */ |
428 |
422 |
429 try { |
423 try { |