Matitaweb: several improvements in the UI.

[helm.git] / matitaB / matita / html / layout.js

diff --git a/matitaB/matita/html/layout.js b/matitaB/matita/html/layout.js
index 1952115577c3046f0b53a4e37388d42d2ab252b2..bedd11ca7467a461107def680ec95a59246e7d22 100644 (file)
--- a/matitaB/matita/html/layout.js
+++ b/matitaB/matita/html/layout.js
@@ -14,7 +14,7 @@ function int_of_px(px) {
 }
 
 function initializeLayout() {
-
+        /*
        apparea.resize = function(w,h) {
                workarea.resize(w,h);
                resizeItem(apparea,w,h);
@@ -42,26 +42,49 @@ function initializeLayout() {
                goalcell.resize(w/3,h);
                resizeItem(sidearea,w/3,h);
        }
+       */
 
-       disambcell.resize = function(w,h) {
+       disambcell.resizeAll = function() {
+               var w = int_of_px(this.parentElement.style.width);
+               var h = int_of_px(this.parentElement.style.height);
+               // resize only, no show/hide
+               /*
+               if (matita.disambMode) {
+                    disambcell.style.display = "inline-block";
+               } else {
+                   disambcell.style.display = "none";
+               }
+               */
                if (matita.proofMode) {
-                       resizeItem(disambcell,w,h/2);
+                       resizeItem(disambcell,w-4,(h/2)-4);
                } else {
-                       resizeItem(disambcell,w,h);
+                       resizeItem(disambcell,w-4,h-4);
                }
        }
 
-       goalcell.resize = function(w,h) {
+       goalcell.resizeAll = function() {
+               var w = int_of_px(this.parentElement.style.width);
+               var h = int_of_px(this.parentElement.style.height);
+               // resize only, no show/hide
+               /*
+               if (matita.proofMode) {
+                    goalcell.style.display = "inline-block";
+               } else {
+                   goalcell.style.display = "none";
+               }
+               */
                if (matita.disambMode) {
-                       resizeItem(goalcell,w,h/2);
+                       resizeItem(goalcell,w-4,(h/2)-4);
                } else {
-                       resizeItem(goalcell,w,h);
+                       resizeItem(goalcell,w-4,h-4);
                }
        }
 
-       $(window).bind("resize", resize);
+       /*
+        $(window).bind("resize", resize);
 
        // resize();
+       */
 
 }
 
@@ -72,15 +95,18 @@ function resize() {
        apparea.resize($(window).width(),$(window).height());
 }
 
+function resizeSide() {
+       disambcell.resizeAll();
+       goalcell.resizeAll();
+}
+
 function updateSide() {
-       scriptcell.resize(workarea.clientWidth,workarea.clientHeight);
-       sidearea.resize(workarea.clientWidth,workarea.clientHeight);
-       updateDisamb();
-       updateGoal();
        if (matita.proofMode || matita.disambMode) {
-               sidearea.style.display = "inline-block";
+               matitaLayout.show("east");
+               updateDisamb();
+               updateGoal();
        } else {
-               sidearea.style.display = "none";
+               matitaLayout.hide("east");
        }
 }
 
@@ -99,3 +125,21 @@ function updateGoal() {
                goalcell.style.display = "none";
        }
 }
+
+function abortLog() {
+       matitaLayout.hide("south");
+}
+
+// a more beautiful procedure to scroll the script to the beginning of unlocked
+// only when needed, and showing it at about one third of the height of the
+// scrollable pane
+function smartScroll() {
+  var element = $("#unlocked");
+  var container = element.parent().parent();
+  var containerTop = container.scrollTop(); 
+  var containerBottom = containerTop + container.height(); 
+  var elemTop = element.get(0).offsetTop;
+  if (elemTop < containerTop || elemTop > containerBottom) {
+    container.scrollTop(elemTop - container.height()/4);
+  }
+}