Even though the result of fetchCachedDeclarationData was ignored due to #133, we were still performing the request, which takes some time on FF to deserialize (or something), depending on what happened to be on the user's cache (because the cache is never written to, only read). This moves the disabling earlier, so that the cache is not read at all (since this means deserializing an old version of the mathlib JSON data, then ignoring it and fetching another version of the mathlib JSON data).
Also fixes an issue where the undefined pattern is passed to decodeURIComponent (resulting in "undefined" which is mishandled by subsequent code).
Even though the result of
fetchCachedDeclarationDatawas ignored due to #133, we were still performing the request, which takes some time on FF to deserialize (or something), depending on what happened to be on the user's cache (because the cache is never written to, only read). This moves the disabling earlier, so that the cache is not read at all (since this means deserializing an old version of the mathlib JSON data, then ignoring it and fetching another version of the mathlib JSON data).Also fixes an issue where the
undefinedpattern is passed todecodeURIComponent(resulting in"undefined"which is mishandled by subsequent code).