1) removed many debug prints

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

diff --git a/matitaB/matita/matitaweb.js b/matitaB/matita/matitaweb.js
index 837c687cb9385dc22af1948d924a041deb6b997e..d9bd38aa80e94dac072b197f10cb86b1d0555032 100644 (file)
--- a/matitaB/matita/matitaweb.js
+++ b/matitaB/matita/matitaweb.js
@@ -535,6 +535,27 @@ function gotoBottom()
 }
 
 
+function gotoTop()
+{
+       processor = function(xml) {
+               if (is_defined(xml)) {
+                 if (xml.childNodes[0].textContent != "ok") {
+                     debug("goto top failed");
+                  }
+                  else
+                     unlocked.innerHTML = locked.innerHTML + unlocked.innerHTML
+                     locked.innerHTML = ""
+                     hideSequent();
+                     unlocked.scrollIntoView(true);
+               } else {
+                       debug("goto top failed");
+               } 
+                resume();
+       };
+       pause();
+       callServer("top",processor,"body=" + (unlocked.innerHTML.html_to_matita()).sescape());
+  
+}
 function gotoPos(offset)
 {
         if (!is_defined(offset)) {