matitaB/matita/html/layout.js

   1 function resizeItem(item,w,h){
   2   item.style.height = h + "px";
   3 //  item.style.minHeight = h + "px";
   4 //  item.style.maxHeight = h + "px";
   5   item.style.width = w + "px";
   6 //  item.style.minWidth = w + "px";
   7 //  item.style.maxWidth = w + "px";
   8 }
   9
  10 function int_of_px(px) {
  11   if(px.length > 2 && px.substr(px.length-2) == "px") {
  12     return parseInt(px.substr(0,px.length-2));
  13   } else { return px; }
  14 }
  15
  16 function initializeLayout() {
  17         /*
  18         apparea.resize = function(w,h) {
  19                 workarea.resize(w,h);
  20                 resizeItem(apparea,w,h);
  21         }
  22
  23         workarea.resize = function(w,h) {
  24                 // proper height = window - (title + top)
  25                 var myh = int_of_px(window.getComputedStyle(apparea,null).height) -
  26                         (titlebar.offsetHeight + toparea.offsetHeight);
  27                 scriptcell.resize(w,myh);
  28                 sidearea.resize(w,myh);
  29                 resizeItem(workarea,w,myh);
  30         }
  31
  32         scriptcell.resize = function(w,h) {
  33                 if (matita.proofMode || matita.disambMode) {
  34                         resizeItem(scriptcell,(w*2)/3,h);
  35                 } else {
  36                         resizeItem(scriptcell,w,h);
  37                 }
  38         }
  39
  40         sidearea.resize = function(w,h) {
  41                 disambcell.resize(w/3,h);
  42                 goalcell.resize(w/3,h);
  43                 resizeItem(sidearea,w/3,h);
  44         }
  45         */
  46
  47         disambcell.resizeAll = function() {
  48                 var w = int_of_px(this.parentElement.style.width);
  49                 var h = int_of_px(this.parentElement.style.height);
  50                 // resize only, no show/hide
  51                 /*
  52                 if (matita.disambMode) {
  53                     disambcell.style.display = "inline-block";
  54                 } else {
  55                     disambcell.style.display = "none";
  56                 }
  57                 */
  58                 if (matita.proofMode) {
  59                         resizeItem(disambcell,w-4,(h/2)-4);
  60                 } else {
  61                         resizeItem(disambcell,w-4,h-4);
  62                 }
  63         }
  64
  65         goalcell.resizeAll = function() {
  66                 var w = int_of_px(this.parentElement.style.width);
  67                 var h = int_of_px(this.parentElement.style.height);
  68                 // resize only, no show/hide
  69                 /*
  70                 if (matita.proofMode) {
  71                     goalcell.style.display = "inline-block";
  72                 } else {
  73                     goalcell.style.display = "none";
  74                 }
  75                 */
  76                 if (matita.disambMode) {
  77                         resizeItem(goalcell,w-4,(h/2)-4);
  78                 } else {
  79                         resizeItem(goalcell,w-4,h-4);
  80                 }
  81         }
  82
  83         /*
  84          $(window).bind("resize", resize);
  85
  86         // resize();
  87         */
  88
  89 }
  90
  91 function resize() {
  92         // var htmlheight = int_of_px(window.getComputedStyle(body.parentNode,null).height);
  93         // var htmlwidth = int_of_px(window.getComputedStyle(body.parentNode,null).width);
  94         // apparea.resize(htmlwidth,htmlheight);
  95         apparea.resize($(window).width(),$(window).height());
  96 }
  97
  98 function resizeSide() {
  99         disambcell.resizeAll();
 100         goalcell.resizeAll();
 101 }
 102
 103 function updateSide() {
 104         if (matita.proofMode || matita.disambMode) {
 105                 matitaLayout.show("east");
 106                 updateDisamb();
 107                 updateGoal();
 108         } else {
 109                 matitaLayout.hide("east");
 110         }
 111 }
 112
 113 function updateDisamb() {
 114         if (matita.disambMode) {
 115                 disambcell.style.display = "inline-block";
 116         } else {
 117                 disambcell.style.display = "none";
 118         }
 119 }
 120
 121 function updateGoal() {
 122         if (matita.proofMode) {
 123                 goalcell.style.display = "inline-block";
 124         } else {
 125                 goalcell.style.display = "none";
 126         }
 127 }
 128
 129 function abortLog() {
 130         matitaLayout.hide("south");
 131 }
 132
 133 // a more beautiful procedure to scroll the script to the beginning of unlocked
 134 // only when needed, and showing it at about one third of the height of the
 135 // scrollable pane
 136 function smartScroll() {
 137   var element = $("#unlocked");
 138   var container = element.parent().parent();
 139   var containerTop = container.scrollTop();
 140   var containerBottom = containerTop + container.height();
 141   var elemTop = element.get(0).offsetTop;
 142   if (elemTop < containerTop || elemTop > containerBottom) {
 143     container.scrollTop(elemTop - container.height()/4);
 144   }
 145 }