X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matitaB%2Fmatita%2Fmatitaweb.js;h=cd25cd15a68b2e349647378de40deb9551c338df;hb=c81b0e8dbfe80e2350e9322afa8316f39f98c3b3;hp=068b30d708cfb0efb319a900887a10a009f66834;hpb=935c8d1b73726bb49b99e5c2dbebdea0d617fa1a;p=helm.git

diff --git a/matitaB/matita/matitaweb.js b/matitaB/matita/matitaweb.js
index 068b30d70..cd25cd15a 100644
--- a/matitaB/matita/matitaweb.js
+++ b/matitaB/matita/matitaweb.js
@@ -644,7 +644,7 @@ function advOneStep(xml) {
 
 	    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 
@@ -655,7 +655,7 @@ function advOneStep(xml) {
               matita.disambMode = true;
               next_cp(0);
             }
-	    throw "Stop";
+	    throw "Wait";
 	}
         else {
             var error = xml.getElementsByTagName("error")[0]; 
@@ -678,9 +678,11 @@ function advanceForm1()
 			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());
@@ -794,7 +796,7 @@ function next_cp(curcp) {
 	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");
 	}
@@ -844,7 +846,7 @@ function show_failures() {
 	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);
@@ -1056,7 +1058,11 @@ function gotoPos(offset)
 		    } catch (er) {
 			init_autotraces();
 			populate_goalarray(metasenv);
-			resume();
+			if (er == "Stop") 
+				resume();
+			else
+				pause();
+
 		    }
 		} else {
 			init_autotraces();