matita.disambMode = true;
updateSide();
- throw "Stop";
+ throw "Wait";
}
else if (is_defined(disamberr)) {
// must be fixed in a daemon: it makes sense to return a
matita.disambMode = true;
next_cp(0);
}
- throw "Stop";
+ throw "Wait";
}
else {
var error = xml.getElementsByTagName("error")[0];
debug("advance failed");
}
} catch (e) {
- // nothing to do
+ if (e == "Stop")
+ resume();
+ else
+ pause();
};
- resume();
};
pause();
callServer("advance",processor,"body=" + (unlocked.innerHTML.html_to_matita()).sescape());
var tryagainbutton = document.createElement("input");
tryagainbutton.setAttribute("type","button");
if (new_curcp > 0) {
- tryagainbutton.setAttribute("value","Try something else");
+ tryagainbutton.setAttribute("value","None of the above");
} else {
tryagainbutton.setAttribute("value","Restart");
}
cancelbutton.setAttribute("onclick","cancel_disambiguate()");
var backbutton = document.createElement("input");
backbutton.setAttribute("type","button");
- backbutton.setAttribute("value","<< Back");
+ backbutton.setAttribute("value","<< Go back");
backbutton.setAttribute("onclick","next_cp(" + cpno + ")");
disambcell.appendChild(backbutton);
} catch (er) {
init_autotraces();
populate_goalarray(metasenv);
- resume();
+ if (er == "Stop")
+ resume();
+ else
+ pause();
+
}
} else {
init_autotraces();