+ else if (submath.str(0).compare("\\[") == 0) {
+ math_end_waiting = true;
+ math_end = "\\]";
+ math_pos = submath.position(size_t(0));
+ }
+ else if (submath.str(0) == "$") {
+ size_t pos = submath.position(size_t(0));
+ if ((pos == 0) || (interval.par[pos-1] != '\\')) {
+ math_end_waiting = true;
+ math_end = "$";
+ math_pos = pos;
+ }
+ }
+ }
+ }
+ if (isPatternString) {
+ if (math_pos < interval.par.length()) {
+ // Disable language
+ keys["foreignlanguage"].disabled = true;
+ disableLanguageOverride = true;
+ }
+ else
+ disableLanguageOverride = false;
+ }
+ else {
+ if (disableLanguageOverride) {
+ keys["foreignlanguage"].disabled = true;