matitaB/matita/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         disambcell.resize = function(w,h) {
  47                 if (matita.proofMode) {
  48                         resizeItem(disambcell,w,h/2);
  49                 } else {
  50                         resizeItem(disambcell,w,h);
  51                 }
  52         }
  53
  54         goalcell.resize = function(w,h) {
  55                 if (matita.disambMode) {
  56                         resizeItem(goalcell,w,h/2);
  57                 } else {
  58                         resizeItem(goalcell,w,h);
  59                 }
  60         }
  61
  62         resize();
  63
  64 }
  65
  66 function resize() {
  67         var htmlheight = int_of_px(window.getComputedStyle(body.parentNode,null).height);
  68         var htmlwidth = int_of_px(window.getComputedStyle(body.parentNode,null).width);
  69         apparea.resize(htmlwidth,htmlheight);
  70 }
  71
  72 function updateSide() {
  73         scriptcell.resize(workarea.clientWidth,workarea.clientHeight);
  74         sidearea.resize(workarea.clientWidth,workarea.clientHeight);
  75         updateDisamb();
  76         updateGoal();
  77         if (matita.proofMode || matita.disambMode) {
  78                 sidearea.style.display = "inline-block";
  79         } else {
  80                 sidearea.style.display = "none";
  81         }
  82 }
  83
  84 function updateDisamb() {
  85         if (matita.disambMode) {
  86                 disambcell.style.display = "inline-block";
  87         } else {
  88                 disambcell.style.display = "none";
  89         }
  90 }
  91
  92 function updateGoal() {
  93         if (matita.proofMode) {
  94                 goalcell.style.display = "inline-block";
  95         } else {
  96                 goalcell.style.display = "none";
  97         }
  98 }