Matitaweb:

[helm.git] / matitaB / matita / matitaweb.js

diff --git a/matitaB/matita/matitaweb.js b/matitaB/matita/matitaweb.js
index 068b30d708cfb0efb319a900887a10a009f66834..cd25cd15a68b2e349647378de40deb9551c338df 100644 (file)
--- 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();