From: Wilmer Ricciotti <ricciott@cs.unibo.it>
Date: Fri, 28 Oct 2011 13:49:57 +0000 (+0000)
Subject: Matitaweb: added layout.js (currently manages resizing of UI).
X-Git-Tag: make_still_working~2148
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=e15474b915f237623e1e667fd789d1417d425f74;p=helm.git

Matitaweb: added layout.js (currently manages resizing of UI).
---

diff --git a/matitaB/matita/layout.js b/matitaB/matita/layout.js
new file mode 100644
index 000000000..2271fe8b7
--- /dev/null
+++ b/matitaB/matita/layout.js
@@ -0,0 +1,98 @@
+function resizeItem(item,w,h){  
+  item.style.height = h + "px";
+  item.style.minHeight = h + "px";
+  item.style.maxHeight = h + "px";
+  item.style.width = w + "px";
+  item.style.minWidth = w + "px";
+  item.style.maxWidth = w + "px";
+}
+
+function int_of_px(px) {
+  if(px.length > 2 && px.substr(px.length-2) == "px") {
+    return parseInt(px.substr(0,px.length-2));
+  } else { return px; }
+}
+
+function initializeLayout() {
+
+	apparea.resize = function(w,h) {
+		workarea.resize(w,h);
+		resizeItem(apparea,w,h);
+	}
+
+	workarea.resize = function(w,h) {
+		// proper height = window - (title + top)
+		var myh = int_of_px(window.getComputedStyle(apparea,null).height) - 
+			(titlebar.offsetHeight + toparea.offsetHeight);
+		scriptcell.resize(w,myh);
+		sidearea.resize(w,myh);
+		resizeItem(workarea,w,myh);
+	}
+
+	scriptcell.resize = function(w,h) {
+		if (matita.proofMode || matita.disambMode) {
+			resizeItem(scriptcell,(w*2)/3,h);
+		} else {
+			resizeItem(scriptcell,w,h);
+		}
+	}
+	
+	sidearea.resize = function(w,h) {
+		disambcell.resize(w/3,h);
+		goalcell.resize(w/3,h);
+		resizeItem(sidearea,w/3,h);
+	}
+
+	disambcell.resize = function(w,h) {
+		if (matita.proofMode) {
+			resizeItem(disambcell,w,h/2);
+		} else {
+			resizeItem(disambcell,w,h);
+		}
+	}
+
+	goalcell.resize = function(w,h) {
+		if (matita.disambMode) {
+			resizeItem(goalcell,w,h/2);
+		} else {
+			resizeItem(goalcell,w,h);
+		}
+	}
+
+	resize();
+
+}
+
+function resize() {
+	var htmlheight = int_of_px(window.getComputedStyle(body.parentNode,null).height);  
+	var htmlwidth = int_of_px(window.getComputedStyle(body.parentNode,null).width);
+	apparea.resize(htmlwidth,htmlheight);
+}
+
+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";
+	} else {
+		sidearea.style.display = "none";
+	}
+}
+
+function updateDisamb() {
+	if (matita.disambMode) {
+		disambcell.style.display = "inline-block";
+	} else {
+		disambcell.style.display = "none";
+	}
+}
+
+function updateGoal() {
+	if (matita.proofMode) {
+		goalcell.style.display = "inline-block";
+	} else {
+		goalcell.style.display = "none";
+	}
+}