--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/editor.css	Sun Mar 18 12:03:04 2012 -0700
@@ -0,0 +1,75 @@
+
+body, html
+{
+	width: 100%;
+	height: 100%;
+	margin: 0;
+}
+
+body > div
+{
+	margin: 0;
+}
+
+.controls
+{
+	width: 15%;
+	height: 100%;
+	display: inline-block;
+	padding: 0;
+	margin: 0;
+	vertical-align: top;
+}
+
+#src
+{
+	width: 70%;
+	display: inline-block;
+	padding: 0;
+	margin: 0;
+}
+
+ul
+{
+	border-style: solid;
+	border-color: black;
+	border-width: 1px;
+	display: block;
+	padding: 2px;
+	box-sizing: border-box;
+	-moz-box-sizing: border-box;
+	-webkit-box-sizing: border-box;
+	height: 50%;
+	margin: 0;
+	overflow: auto;
+}
+
+ul:first-child
+{
+	border-bottom-width: 0px;
+}
+
+#operators, .showops > #builtin
+{
+	display: none;
+}
+
+.showops > #operators
+{
+	display: block;
+}
+
+li
+{
+	display: inline-block;
+	border-style: solid;
+	border-color: lightgrey;
+	border-width: 1px;
+	padding: 2px;
+	margin: 4px;
+	min-width: 9mm;
+	min-height: 9mm;
+	cursor: pointer;
+}
+
+