Bug 158303

Description Toshihiro Izumi 2006-09-22 09:48:25 EDT

(This is following bug #153027)
Window->Preferences->PHP->PHP Manual->Edit->Change "File Extension"
This doesn't work under a certain condition.
Because org.eclipse.php.ui.util.PHPManualFactory#getManual doesn't check the file extension.

>public static PHPManual getManual() {
>    String storedSite = PreferenceConstants.getPreferenceStore().getString(PreferenceConstants.PHP_MANUAL_SITE);
>    if (manual == null || !fStoredSite.equals(storedSite)) {
>        manual = null;
>        fStoredSite = storedSite;

If manual is not null (already created) and url(storedSite) is not changed, getManual() returns previous instance of PHPManual which has old values, not creates new instance which has new values.

Problematic case:
step 1. In Preferences, add new manual site with wrong file extension
step 2. In php editor, open manual -> 404 error [getManual() creates instance]
step 3. In Preferences, edit/correct file extension
step 4. In php editor, open manual -> 404 error [url is not changed, getManual() returns old instance]

While the instance of PHPManual is alive, it is impossible to escape this 404 error. To restart eclipse (or change manual site and open manual and change back site) is necessary.

According to #153027, this is the specification. I don't think this is good design. Change of file extension should work immediately.