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";
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));
16 function initializeLayout() {
18 apparea.resize = function(w,h) {
20 resizeItem(apparea,w,h);
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);
32 scriptcell.resize = function(w,h) {
33 if (matita.proofMode || matita.disambMode) {
34 resizeItem(scriptcell,(w*2)/3,h);
36 resizeItem(scriptcell,w,h);
40 sidearea.resize = function(w,h) {
41 disambcell.resize(w/3,h);
42 goalcell.resize(w/3,h);
43 resizeItem(sidearea,w/3,h);
46 disambcell.resize = function(w,h) {
47 if (matita.proofMode) {
48 resizeItem(disambcell,w,h/2);
50 resizeItem(disambcell,w,h);
54 goalcell.resize = function(w,h) {
55 if (matita.disambMode) {
56 resizeItem(goalcell,w,h/2);
58 resizeItem(goalcell,w,h);
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);
72 function updateSide() {
73 scriptcell.resize(workarea.clientWidth,workarea.clientHeight);
74 sidearea.resize(workarea.clientWidth,workarea.clientHeight);
77 if (matita.proofMode || matita.disambMode) {
78 sidearea.style.display = "inline-block";
80 sidearea.style.display = "none";
84 function updateDisamb() {
85 if (matita.disambMode) {
86 disambcell.style.display = "inline-block";
88 disambcell.style.display = "none";
92 function updateGoal() {
93 if (matita.proofMode) {
94 goalcell.style.display = "inline-block";
96 goalcell.style.display = "none";