Grammalecte  Diff

Differences From Artifact [3152c4204d]:

To Artifact [382be936c1]:


40
41
42
43
44
45
46








47
48
49
50
51
52
53
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61







+
+
+
+
+
+
+
+







            this.xGCEWorker = new BasePromiseWorker('chrome://promiseworker/content/gce_worker.js');
            let that = this;
            let xPromise = this.xGCEWorker.post('loadGrammarChecker', [prefs.getCharPref("sGCOptions"), "Thunderbird"]);
            xPromise.then(
                function (aVal) {
                    console.log(aVal);
                    prefs.setCharPref("sGCOptions", aVal);
                    // spelling dictionary
                    if (prefs.getCharPref("sMainDicName")) {
                        let sMainDicName = prefs.getCharPref("sMainDicName");
                        if (sMainDicName == "fr-classic.json" || sMainDicName == "fr-reform.json") {
                            that.xGCEWorker.post("setDictionary", ["main", sMainDicName]);
                        }
                    }
                    // personal dictionary
                    if (prefs.getBoolPref("bPersonalDictionary")) {
                        let sDicJSON = oFileHandler.loadFile("fr.personal.json");
                        if (sDicJSON) {
                            that.xGCEWorker.post('setDictionary', ["personal", sDicJSON]);
                        }
                    }
                },
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
830
831
832
833
834
835
836

837
838
839
840
841
842
843







-







                    }
                    document.getElementById('res_o_ma_word').textContent = n1;
                }
                document.getElementById("o_group_misc").checked = false;
                this.switchGroup("o_group_misc");
            }
            document.getElementById('textformatter-progressbar').value = document.getElementById('textformatter-progressbar').max;
            document.getElementById('textformatter-progressbar').value = "Formatage terminé.";
            // end of processing

            //window.setCursor("auto"); // restore pointer
            const t1 = Date.now();
            document.getElementById('textformatter-timer').textContent = this.getTimeRes((t1-t0)/1000);
        }
        catch (e) {