]> matita.cs.unibo.it Git - helm.git/blob - matitaB/matita/html/layout.js
missing notation file
[helm.git] / 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 }