[Toss-devel-svn] SF.net SVN: toss:[1743] trunk/Toss

[<luk...@us...>]

Revision: 1743
          http://toss.svn.sourceforge.net/toss/?rev=1743&view=rev
Author:   lukaszkaiser
Date:     2012-07-06 01:06:25 +0000 (Fri, 06 Jul 2012)
Log Message:
-----------
Interface corrections in structure explorer.

Modified Paths:
--------------
    trunk/Toss/Client/Drawing.ml
    trunk/Toss/Client/Drawing.mli
    trunk/Toss/Client/JsEval.ml
    trunk/Toss/Client/Style.css
    trunk/Toss/Client/eval.html
    trunk/Toss/Formula/BoolFormula.ml
    trunk/Toss/README
    trunk/Toss/www/contact.xml

Modified: trunk/Toss/Client/Drawing.ml
===================================================================
--- trunk/Toss/Client/Drawing.ml	2012-07-05 00:25:38 UTC (rev 1742)
+++ trunk/Toss/Client/Drawing.ml	2012-07-06 01:06:25 UTC (rev 1743)
@@ -42,6 +42,19 @@
 let defaultCGreen = {red=62 ; green=89 ; blue=24 ; opacity = 1. }
 let defaultCBlue = {red=165 ; green=175 ; blue=170 ; opacity = 1. }
 
+let palette = Hashtbl.create 7
+
+(* Set a color for a name. *)
+let set_color name color =
+  Hashtbl.add palette name color
+
+(* Get the color. If not set before, it is the default one, depending on
+   whether for stroke or fill, or a default red, if name starts with '|'.*) 
+let get_color ?(stroke=false) name =
+  try Hashtbl.find palette name with Not_found ->
+    if String.length name > 0 && name.[0] = '|' then defaultCRed else
+      if stroke then defaultCStroke else defaultCFill
+
 let color_to_str c =
   let op = string_of_float c.opacity in
   let l = String.length op - 1 in
@@ -205,12 +218,11 @@
   let draw_rel (rel, arity) =
     if arity = 1 then
       let elems = Structure.Tuples.elements (Structure.rel_graph rel struc) in
-      let col = match rel with | "|R" -> defaultCRed | "|G" -> defaultCGreen
-        | "|B" -> defaultCBlue | _ -> defaultCFill in
+      let col = get_color rel in
       Aux.concat_map (fun a -> [Circle (pos a.(0), {x=10.; y=10.}, col)]) elems
     else if arity = 2 then
       let tuples = Structure.Tuples.elements (Structure.rel_graph rel struc) in
-      let c = if rel.[0] = '|' then defaultCRed else defaultCStroke in
+      let c = get_color ~stroke:true rel in
       Aux.concat_map (fun a -> arrow c (pos_draw a.(0)) (pos_draw a.(1))) tuples
     else [] in
   elem_drawings @ (Aux.concat_map draw_rel (Structure.rel_signature struc))

Modified: trunk/Toss/Client/Drawing.mli
===================================================================
--- trunk/Toss/Client/Drawing.mli	2012-07-05 00:25:38 UTC (rev 1742)
+++ trunk/Toss/Client/Drawing.mli	2012-07-06 01:06:25 UTC (rev 1743)
@@ -33,7 +33,14 @@
 (** Default stroke color. *)
 val defaultCStroke : color
 
+(** Set the color for a name. *)
+val set_color : string -> color -> unit
 
+(** Get the color. If not set before, it is the default one, depending on
+    whether for stroke or fill, or a default red, if name starts with '|'. *) 
+val get_color : ?stroke : bool -> string -> color
+
+
 (** Shapes. *)
 type shape =
   | Circle of point * point * color (** circle, given middle and radiuses *)

Modified: trunk/Toss/Client/JsEval.ml
===================================================================
--- trunk/Toss/Client/JsEval.ml	2012-07-05 00:25:38 UTC (rev 1742)
+++ trunk/Toss/Client/JsEval.ml	2012-07-06 01:06:25 UTC (rev 1743)
@@ -111,3 +111,27 @@
 let _ = set_handle "mouseup_handle" mouseup_handle
 let _ = set_handle "mousedown_handle" mousedown_handle
 let _ = set_handle "mousemove_handle" mousemove_handle
+
+let set_colors colors_str =
+  let defs = Aux.split_charprop (fun c -> c = ';') (Js.to_string colors_str) in
+  let set_color_def rel c = 
+    let b = function '0' -> 0 | '1' -> 1 | '2' -> 2 | '3' -> 3 | '4' -> 4
+      | '5' -> 5 | '6' -> 6 | '7' -> 7 | '8' -> 8 | '9' -> 9 | 'a' -> 10
+      | 'A' -> 10 | 'b' -> 11 | 'B' -> 11 | 'c' -> 12 | 'C' -> 12 | 'd' -> 13
+      | 'D' -> 13 | 'e' -> 14 | 'E' -> 14 | 'f' -> 15 | 'F' -> 15 | _ -> -1 in
+    if String.length c <> 7 || c.[0] <> '#' then "Incorrect color: " ^ c else
+      let (r1, r0, g1, g0, b1, b0) = 
+        (b c.[1], b c.[2], b c.[3], b c.[4], b c.[5], b c.[6]) in
+      if r0 < 0 || r1 < 0 || g0 < 0 || g1 < 0 || b0 < 0 || b1 < 0 then
+        "Incorrect numbers in color: " ^ c
+      else let col = { Drawing.red = 16*r1+r0 ; Drawing.green = 16*g1+g0 ;
+                       Drawing.blue = 16*b1+b0 ; Drawing.opacity = 1. } in
+           Drawing.set_color rel col;
+           "Set " ^ rel ^ " to " ^ c in
+  let parse_def d = 
+    match Aux.split_charprop (fun c -> c = ':') d with
+      | [rel; c] -> set_color_def (Aux.strip_spaces rel) (Aux.strip_spaces c)
+      | _ -> "Incorrect color definition: " ^ (Aux.normalize_spaces d) in
+  Js.string (String.concat " <br /> " (List.map parse_def defs))
+
+let _ = set_handle "set_colors" set_colors

Modified: trunk/Toss/Client/Style.css
===================================================================
--- trunk/Toss/Client/Style.css	2012-07-05 00:25:38 UTC (rev 1742)
+++ trunk/Toss/Client/Style.css	2012-07-06 01:06:25 UTC (rev 1743)
@@ -43,7 +43,6 @@
 .bt {
     border-color: #260314;
     border-radius: 4px;
-    -moz-border-radius: 4px;
     border-width: 1px;
     color: #260314;
     background-color: #fff1d4;
@@ -64,11 +63,24 @@
     float: right;
 }
 
-.obt, .boldobt, .gamebt, .ebt, .ebts {
+.textar {
+    font-family: Verdana;
+    font-size: 0.9em;
+    width: 33em;
+}
+
+.headerp {
+    width: 100%;
+    border-bottom: 0px solid;
+    padding-top: 0.5em;
+    text-align: center;
+    font-weight: bold;
+}
+
+.obt, .boldobt, .gamebt, .ebt, .ebts, .ebtr, .ebtl {
     text-align: left;
     border-color: #260314;
     border-radius: 4px;
-    -moz-border-radius: 4px;
     border-width: 0px;
     color: #260314;
     background-color: #fff1d4;
@@ -76,7 +88,8 @@
     font-family: Verdana, 'TeXGyreHerosRegular', sans;
 }
 
-.obt:hover, .ebt:hover, .ebts:hover, .boldobt:hover, .gamebt:hover {
+.obt:hover, .ebt:hover, .ebts:hover, .ebtr:hover, .ebtl:hover,
+  .boldobt:hover, .gamebt:hover{
     cursor: pointer;
     text-decoration: underline;
 }
@@ -86,12 +99,22 @@
     font-size: 1em;
 }
 
-.ebt, .ebts {
+.ebt, .ebts, .ebtr, .ebtl {
     /*font-weight: bold;*/
     text-align: center;
     border-width: 1px;
 }
 
+.ebtr {
+  position: absolute;
+  right: 1px;
+}
+
+.ebtl {
+  position: absolute;
+  left: 1px;
+}
+
 .gamebt {
     margin-bottom: 1em;
     padding-top: 0.5em;
@@ -104,7 +127,6 @@
     text-align: left;
     border-color: #260314;
     border-radius: 4px;
-    -moz-border-radius: 4px;
     border-width: 0px;
     color: #260314;
     background-color: #fff1d4;
@@ -120,7 +142,6 @@
 .dbt {
     border-color: #fff1d4;
     border-radius: 4px;
-    -moz-border-radius: 4px;
     border-width: 0px;
     color: #fff1d4;
     background-color: #400827;
@@ -235,7 +256,6 @@
     top: -1em;
     background-color: rgba(255, 241, 228, 0.8);
     border-radius: 4px;
-    -moz-border-radius: 4px;
     opacity: 1;
 }
 
@@ -263,7 +283,6 @@
     font-size: 0.8em;
     border-color: #fff1d4;
     border-radius: 4px;
-    -moz-border-radius: 4px;
     border-width: 1px;
     position: relative;
     top: 2px;
@@ -284,9 +303,6 @@
     padding-left: 0.2em;
     padding-right: 0.2em;
     border-radius: 0px;
-    -moz-border-radius: 0px;
-    /*font-size: 0.9em;
-    -moz-border-radius: 6px 6px 0px 0px; */
 }
 
 #speed {
@@ -300,8 +316,7 @@
     padding: 0px;
     margin: 0px;
     border-color: #fff1d4;
-    /*border-radius: 4px;
-    -moz-border-radius: 4px;*/
+    /*border-radius: 4px; */
     border-width: 0px;
 }
 
@@ -328,7 +343,6 @@
     margin: 0px;
     border-color: #fff1d4;
     border-radius: 4px;
-    -moz-border-radius: 4px;
     border-width: 0px;
 }
 
@@ -349,7 +363,6 @@
 .forminput, .hiddenforminput {
     border-color: #fff1d4;
     border-radius: 4px;
-    -moz-border-radius: 4px;
     border-width: 2px;
     position: relative;
     top: 2px;
@@ -392,7 +405,6 @@
     background-color: #ffffff;
     border-color: #fff1d4;
     border-radius: 4px;
-    -moz-border-radius: 4px;
     border-width: 1px;
 }
 
@@ -516,8 +528,6 @@
     padding-bottom: 0.2em;
     padding-left: 0.2em;
     padding-right: 0.2em;
-    /*font-size: 0.9em;
-    -moz-border-radius: 6px 6px 0px 0px; */
 }
 
 #bottom {
@@ -570,9 +580,6 @@
     border-color: #fff1d4;
     border-style: solid;
     border-width: 0px 0px 0px 2px;
-    /*border-width: 0px 2px 2px 2px;
-    border-radius: 0px 0px 6px 6px;
-    -moz-border-radius: 0px 0px 6px 6px;*/
 }
 
 #toss-link {
@@ -819,7 +826,6 @@
     width: 6em;
     border-color: #260314;
     border-radius: 4px;
-    -moz-border-radius: 4px;
     border-width: 1px;
     color: #260314;
     background-color: #fff1d4;
@@ -899,13 +905,6 @@
     padding: 0px;
 }
 
-#board-left {
-    position: relative;
-    left: 2em;
-    top: 5em;
-    width: 30em;
-}
-
 #board {
     padding-top: 1em;
     min-width: 10em;
@@ -1009,9 +1008,9 @@
 }
 
 #canvas {
-    width: 29em;
-    height: 29em;
-    border: 2px solid  #260314;
+    width: 30em;
+    height: 30em;
+    border: 1px solid  #260314;
 }
 
 /* SVG styling */

Modified: trunk/Toss/Client/eval.html
===================================================================
--- trunk/Toss/Client/eval.html	2012-07-05 00:25:38 UTC (rev 1742)
+++ trunk/Toss/Client/eval.html	2012-07-06 01:06:25 UTC (rev 1743)
@@ -5,6 +5,7 @@
   <title>Toss Relational Structures Explorer</title>
   <meta name="Description" content="Explore Relational Structures." />
   <meta http-equiv="X-UA-Compatible" content="chrome=1" />
+  <meta name="viewport" content="initial-scale=0.75" />
   <link rel="icon" type="image/vnd.microsoft.icon" href="favicon.ico" />
   <link rel="stylesheet" type="text/css" href="Style.css" media="screen" title="Default"/>
   <script type="text/javascript">
@@ -46,22 +47,46 @@
     var canvas = document.getElementById("canvas");
     var ctx = canvas.getContext("2d");
     ctx.clearRect(0, 0, canvas.width, canvas.height);
+    ctx.fillStyle = "#ffe4aa";
+    ctx.strokeStyle = "#260314";
+    ctx.lineWidth = 5;
+    ctx.lineCap = "round";
+    ctx.lineJoin = "round";
 }
 
-function draw_it () {
+function draw_it_msg (msg) {
+  if (msg) {
+    document.getElementById ("working").style.display = 'block'; 
+    document.getElementById ("working").innerHTML = 'Working...';
+  }
   var rels = document.getElementById ("relations").value;
   var pos = document.getElementById ("positions").value;
   var elemsF = document.getElementById ("no-elems-start").value;
   var elemsT = document.getElementById ("no-elems-end").value;
   var struc = "[ " + elemsF + " - " + elemsT + " |  | - ] with \n" +
     rels + " with \n" + pos;
-  ASYNCH ("draw_struc", ["", struc], true, function (a) { 
-     var ctx = document.getElementById("canvas").getContext("2d");
-     eval (a[0])
-  })
+  if (msg) {
+    ASYNCH ("draw_struc", ["", struc], true, function (a) { 
+       document.getElementById ("working").style.display = 'none';
+       var ctx = document.getElementById("canvas").getContext("2d");
+       eval (a[0])
+       toggle_to_show ("view");
+    })
+  } else {
+    ASYNCH ("draw_struc", ["", struc], true, function (a) { 
+       var ctx = document.getElementById("canvas").getContext("2d");
+       eval (a[0])
+    })
+  }
 }
 
+function draw_it () {
+  draw_it_msg (true);
+}
+
 function find_draw_it () {
+  document.getElementById ("working").style.display = 'block';
+  document.getElementById ("working").innerHTML = 'Working...';
   var rels = document.getElementById ("relations").value;
   var pos = document.getElementById ("positions").value;
   var elemsF = document.getElementById ("no-elems-start").value;
@@ -70,8 +95,10 @@
   var struc = "[ " + elemsF + " - " + elemsT + " |  | - ] with \n" +
     rels + " with \n" + pos;
   ASYNCH ("draw_struc", [so, struc], true, function (a) { 
+     document.getElementById ("working").style.display = 'none';
      var ctx = document.getElementById("canvas").getContext("2d");
      eval (a[0]);
+     toggle_to_show ("view");
      if (a[1] !== "Error") { put_msg (a[1], 2000) }
   })
 }
@@ -165,42 +192,59 @@
   }
 }
 
-
 function handle_elem_click (eid) { console.log (eid); }
 
+function example_basic () {
+  document.getElementById ("struc-name").value = "Basic";
+  document.getElementById ("relations").value =
+    "E(x, y) = (&y = &x + 1) ∨ (&x=15 ∧ &y=1)";
+  document.getElementById ("positions").value = ":x(a) = &a;\n" +
+    ":y(a) = &a · (10 - &a) / 10";
+  document.getElementById ("no-elems-start").value = "1";
+  document.getElementById ("no-elems-end").value = "15";
+  draw_it_msg (false);
+}
+
 function example_primes () {
-  document.getElementById ("struc-name").value = "Prime Numbers";
+  document.getElementById ("struc-name").value = "Primes";
   document.getElementById ("relations").value =
     "P(z) = &z > 1 and ∀ x,y \n    (&x · &y = &z → (&x = 1 ∨ &y = 1))";
   document.getElementById ("positions").value = ":x(a) = &a; \n:y(a) = 0";
   document.getElementById ("no-elems-start").value = "1";
   document.getElementById ("no-elems-end").value = "10";
-  draw_it ();
+  draw_it_msg (false);
 }
 
 function example_tc () {
-  document.getElementById ("struc-name").value = "Transitive Closure";
+  document.getElementById ("struc-name").value = "Simple TC";
   document.getElementById ("relations").value =
     "E(x, y) = &y = &x + 1;\n" +
     "S(x, y) = x ≠ y ∧ tc x,y E(x, y)";
   document.getElementById("positions").value=":x(a) = 5·&a;\n:y(a) = &a·&a / 2";
   document.getElementById ("no-elems-start").value = "1";
   document.getElementById("no-elems-end").value = "4";
-  draw_it ();
+  draw_it_msg (false);
 }
 
-function example_basic () {
-  document.getElementById ("struc-name").value = "Basic Example";
-  document.getElementById ("relations").value =
-    "E(x, y) = (&y = &x + 1) ∨ (&x=15 ∧ &y=1)";
-  document.getElementById ("positions").value = ":x(a) = &a;\n" +
-    ":y(a) = &a · (10 - &a) / 10";
+function example_heart () {
+  document.getElementById ("struc-name").value = "Heart";
+  document.getElementById ("relations").value = 
+    "E(x, y) = (&y = &x + 1 ∧ &x ≠ 18) ∨ (&x=37 ∧ &y=18)";
+  document.getElementById ("positions").rows = 7;
+  document.getElementById ("positions").value =
+    ":x(a) = :(&a ≤ 18) · (:(&a ≤ 10) · &a - :(&a > 10) · (&a-20))\n" +
+    " - let :b = &a - 18 in :(&a > 18) · (:(:b ≤ 10) · :b - \n  " +
+    " :(:b > 10) · (:b - 20) - 2); \n\n" +
+    ":y(a) = :(&a ≤ 18) · (:(&a ≤ 10) ·&a · (10 - &a) / 10 - \n" +
+    "  :(&a > 10)·(&a - 10)) + let :b = &a - 18 in :(&a > 18)·( \n" +
+    "  :(:b ≤ 10)·:b · (10-:b) / 10 - :(:b > 10)·(:b - 10) )";
   document.getElementById ("no-elems-start").value = "1";
-  document.getElementById ("no-elems-end").value = "15";
-  draw_it ();
+  document.getElementById ("no-elems-end").value = "37";
+  draw_it_msg (false);
 }
 
 function example_matching () {
+  document.getElementById ("so-name").value = "Matching";
   document.getElementById ("second-order").value = 
     "∀ x,y ( |M(x, y) -> (\n" +
     "  ( E(x, y) ∨ E(y, x) ) ∧ ¬∃ z (z≠y ∧ |M(x, z) )\n" +
@@ -209,6 +253,7 @@
 }
 
 function example_2col () {
+  document.getElementById ("so-name").value = "2-coloring";
   document.getElementById ("second-order").value = 
     "∀ x,y ( (|R(x) ∨ |G(x)) ∧ ( E(x,y) → " +
     "\n    ¬( (|R(x) ∧ |R(y)) ∨ (|G(x) ∧ |G(y)) ) ) )";
@@ -216,26 +261,19 @@
 }
 
 function example_3col () {
+  document.getElementById ("so-name").value = "3-coloring";
   document.getElementById ("second-order").value = 
     "∀ x,y ( ( |R(x) ∨ |G(x) ∨ |B(x)) ∧ ( E(x,y) → " +
     "\n    ¬( (|R(x) ∧ |R(y)) ∨ (|G(x) ∧ |G(y)) ∨ (|B(x) ∧ |B(y)) ) ) )";
   find_draw_it ();
 }
 
-function example_heart () {
-  document.getElementById ("struc-name").value = "Heart Drawing";
-  document.getElementById ("relations").value = 
-    "E(x, y) = (&y = &x + 1 ∧ &x ≠ 18) ∨ (&x=37 ∧ &y=18)";
-  document.getElementById ("positions").value =
-    ":x(a) = :(&a ≤ 18) · (:(&a ≤ 10) · &a - :(&a > 10) · (&a - 20)) \n" +
-    " - let :b = &a - 18 in :(&a > 18) · (:(:b ≤ 10) · :b - \n  " +
-    " :(:b > 10) · (:b - 20) - 2); \n\n" +
-    ":y(a) = :(&a ≤ 18) · (:(&a ≤ 10) ·&a · (10 - &a) / 10 - \n  " +
-    "  :(&a > 10)·(&a - 10)) + let :b = &a - 18 in \n" +
-    " :(&a > 18) · (:(:b ≤ 10) ·:b · (10 - :b) / 10 - :(:b > 10)·(:b - 10))";
-  document.getElementById ("no-elems-start").value = "1";
-  document.getElementById ("no-elems-end").value = "37";
-  draw_it ();
+function example_tc_so () {
+  document.getElementById ("so-name").value = "TC";
+  document.getElementById ("second-order").value = 
+    "∀ x,y,z ( ( E(x, y) → |Tc(x, y) ) ∧\n" + 
+    "  ( (|Tc(x, y) ∧ |Tc(y, z)) -> |Tc(x, z) ) )";
+  find_draw_it ();
 }
 
 function add_field (field, s) {
@@ -311,8 +349,8 @@
       var n = k.substring (16, k.length);
       var li = document.createElement('li');
       li.innerHTML ='<button class="obt" onclick="load_struc('+"'"+ n +"'"+')">'
-        + n +'</button> (<button class="obt" onclick="del_struc('+ "'"+ n +
-        "'" +')" title="Delete this structure.">-</button>)';
+        + n +'</button> <button class="ebtr" onclick="del_struc('+ "'"+ n +"'"+
+        ')" style="width: 4em;" title="Delete this structure.">Del</button>';
       saved.appendChild (li);
     }
   }
@@ -327,8 +365,8 @@
       var n = k.substring (16, k.length);
       var li = document.createElement('li');
       li.innerHTML ='<button class="obt" onclick="load_so('+"'"+ n +"'"+')">'
-        + n +'</button> (<button class="obt" onclick="del_so('+ "'"+ n +
-        "'" +')" title="Delete this formula.">-</button>)';
+        + n +'</button> <button class="ebtr" onclick="del_so('+ "'"+ n +
+        "'" +')" style="width: 4em;" title="Delete this formula.">Del</button>';
       saved.appendChild (li);
     }
   }
@@ -352,28 +390,21 @@
   list_stored_struc ();
 }
 
-function toggle_edit_view () {
-  var bt = document.getElementById("editbt");
-  if (bt.innerHTML == "Edit") {
-    document.getElementById('edit').style.display = 'block';
-    document.getElementById('board-left').style.display = 'none';
-    bt.innerHTML = "View";
-  } else {
-    document.getElementById('edit').style.display = 'none';
-    document.getElementById('board-left').style.display = 'block';
-    bt.innerHTML = "Edit";
-  }
-}
-
 function adjust_to_width () {
   var e = document.getElementById ("edit");
   var em_size = 
     document.defaultView.getComputedStyle(e,null).getPropertyValue('font-size');
   var em_size_int = parseInt (em_size.substring (0, em_size.length - 2));
-  if (window.innerWidth > 80 * em_size_int) { // enough space for view
-    document.getElementById('board-left').style.left = '35em';
-    document.getElementById('board-left').style.display = 'block';
-    document.getElementById('editbt').style.display = 'none';
+  if (window.innerWidth > 80 * em_size_int) { // enough space for left view
+    document.getElementById('div_right_col_full').style.position = 'absolute';
+    document.getElementById('div_right_col_full').style.top = '-1em';
+    document.getElementById('div_right_col_full').style.left = '35em';
+  } else {
+    toggle ("struc");
+    toggle ("formula");
+    toggle ("colors");
+    put_msg ("This page is best viewed on a screen > 80em wide.<br\>" +
+             "It then switches to two-column layout.", 4000)
   }
 }
 
@@ -385,39 +416,96 @@
   }, time);
 }
 
-function show_help () {
-  document.getElementById ("working").style.textAlign = "left";
+function hide_working () {
+  document.getElementById ("working").style.display = 'none';
+  document.getElementById ("working").style.textAlign = "center";
+  document.getElementById ("working").style.fontWeight = "bold";
+}
+
+function toggle (name) {
+  var bt = document.getElementById ("hide_" + name + "_bt");
+  if (bt.innerHTML == "Hide") {
+    bt.innerHTML = "Show";
+    document.getElementById ("div_" + name + "_full").style.display = 'none';
+  } else {
+    bt.innerHTML = "Hide";
+    document.getElementById ("div_" + name + "_full").style.display = 'block';
+  }
+}
+
+function toggle_to_show (name) {
+  var bt = document.getElementById ("hide_" + name + "_bt");
+  if (bt.innerHTML !== "Hide") { toggle (name); }
+}
+
+function show_help (content) {
+  document.getElementById ("working").style.textAlign = "justify";
   document.getElementById ("working").style.fontWeight = "normal";
   document.getElementById("working").innerHTML = '\
-<b>Welcome to Relational Structures Explorer</b> \
-<p><b>Relational structures</b> consist of a set of <em>elements</em> and \
-of <em>relations</em> defined by <em>formulas</em>.</p> \
-<p><b>Elements</b> are numbered. You can change their range and you can access \
-the number of the element corresponding to a variable <em>x</em> in a formula \
-by writing <em>&x</em> or <em>:nbr(x)</em>.</p> \
-<p><b>Formulas</b> are written in first-order logic. You can use relation \
-symbols, Boolean combinations and quantifiers. Additionally, you can use \
-arithmetic operations (+-*/^) on element numbers and element positions.</p> \
-<p><b>Positions</b> of elements are determined by their <em>x</em> and \
-<em>y</em> coordinates. Define and access them as in <b>:x(a)</b> and \
-<b>:y(a)</b>. You can again use arithmetic operations and also conditionals \
-on formulas, written <b>:(formula)</b>.</p> \
-<p><b>Relation Finder</b>, placed at the bottom, automatically finds relations \
-that satisfy the given property. Use <b>|</b> in front of the relation symbol \
-to be found, as in <b>|R(x)</b>.</p> \
-';
+<b>Relational Structures Explorer Help</b> &nbsp; &nbsp;\
+<button class="obt" style="position: absolute; right: 1em;" onclick="hide_working()">Hide</button> ' + content;
   document.getElementById ("working").style.display = "block";
-  setTimeout (function () { 
-    document.getElementById ("working").style.display = "none";
-    document.getElementById ("working").style.textAlign = "center";
-    document.getElementById ("working").style.fontWeight = "bold";
-  }, 20000);
 }
+
+function show_help_view () {
+  show_help('\
+<p><b>Structure view</b> shows the elements and relations in the structure.\
+  You can move the elements with your mouse, but old positions will be restored\
+  when the structure is redrawn.</p>\
+  ');
+}
+
+function show_help_saved () {
+  show_help('\
+<p><b>Saved structures and formulas</b> are stored in the browser local \
+  storage. Press the <b>Save</b> button in the respective edit field to save \
+  a structure or a formula, and later the <b>Del</b> button to delete it.</p>\
+  ');
+}
+
+function show_help_struc () {
+  show_help('\
+<p><b>Structure editor</b> allows to edit the relations in the structure and \
+  to set the positions of elements. It uses formulas of extended first-order \
+  logic with counting. Write <b>&a</b> or <b>:nbr(a)</b> to access the number \
+  of the element which is assigned to the variable <b>a</b>, and <b>:x(a)</b> \
+  and <b>:y(a)</b> for the x- and y-coordinate of its position. Look at the \
+  example structures to see more of the syntax we use.</p>\
+  ');
+}
+
+function show_help_formula () {
+  show_help('\
+<p><b>Formula evaluator</b> allows to check formulas and to find relations \
+  defined in second-order logic. To define a new relation, put <b>|</b> in \
+  front of the relation symbol, e.g., write <b>∃&nbsp;x,y |R(x,y)</b>. The new \
+  relation will be added to the structure (click example formulas to try).</p> \
+  ');
+}
+
+function show_help_colors () {
+  show_help('\
+<p><b>Color selector</b> allows to assign colors to relations, by giving \
+  a list of the form <b>Relation : #xcolor</b> where <b>xcolor</b> must \
+  be 6-characters long and a valid rgb value in hexadecimal.</p> \
+  ');
+}
+
+function select_colors (silent) {
+  var color_defs = document.getElementById('colors').value;
+  if (silent) {
+    ASYNCH ("set_colors", [color_defs], true, function (a) { ; })
+  } else {
+    ASYNCH ("set_colors", [color_defs], true, function (a) { 
+      put_msg (a, 5000);
+    })
+  }
+}
 //-->
 </script>
 </head>
 
-<body onload="init_canvas (); list_stored (); draw_it (); adjust_to_width()">
+<body onload="init_canvas (); select_colors (true) ; list_stored (); draw_it_msg (false); adjust_to_width()">
 <div id="main">
 
 <div id="top">
@@ -429,12 +517,26 @@
 <span style="position: relative; left: 2em; top: 0.5em; font-size: 1.2em">
   Relational Structures Explorer</span>
 <span id="toprighttab" style="display: block;">
-  <button class="obt" id="editbt" onclick="toggle_edit_view()">View</button>
-  <button class="obt" id="editbt" onclick="show_help()">Help</button>
 </span>
 </div>
 
-<div id="board-left" style="display: none;">
+
+<div id="working" style="display: none; width: 30em;"></div>
+
+<div id="edit" style="position: relative; top: 2.5em; left: 2em;
+                      width: 30em; margin-bottom: 6em;">
+
+<div id="div_right_col_full" style="width: 30em;">
+
+<p class="headerp">
+  <button class="ebtl" style="width: 4em;" title="Show/Hide structure view."
+          id="hide_view_bt" onclick="toggle('view')">Hide</button>
+  View Structure
+  <button class="ebtr" style="width: 4em;" title="Structure viewing help."
+          onclick="show_help_view()">Help</button>
+</p>
+
+<div id="div_view_full" style="width: 30em;">
 <canvas id="canvas" height="1100" width="1100"
         onmouseup="mouseup_handle(event)"
         onmousedown="mousedown_handle(event)"
@@ -446,10 +548,50 @@
 </canvas>
 </div>
 
-<div id="working" style="display: none; width: 30em;"></div>
+<p class="headerp">
+  <button class="ebtl" style="width: 4em;" title="Show/Hide color selector."
+          id="hide_colors_bt" onclick="toggle ('colors')">Hide</button>
+  Select Colors
+  <button class="ebtr" style="width: 4em;" title="Color selector help."
+            onclick="show_help_colors()">Help</button>
+</p>
 
-<div id="edit" style="position: absolute; top: 4em; left: 2em;">
+<div id="div_colors_full">
+<p>Colors
+  <span style="position: absolute; right: 2px;">
+  <button class="ebts" style="background-color: #e5effa;";
+          onclick="add_field('colors', '#e5effa')">&nbsp;</button><button
+      class="ebts" style="background-color: #a5afaa;";
+      onclick="add_field('colors', '#a5afaa')">&nbsp;</button><button
+    class="ebts" style="background-color: #93a605;";
+    onclick="add_field('colors', '#93a605')">&nbsp;</button><button
+      class="ebts" style="background-color: #3e5916;";
+      onclick="add_field('colors', '#3e5916')">&nbsp;</button><button
+    class="ebts" style="background-color: #f28705;";
+    onclick="add_field('colors', '#f28705')">&nbsp;</button><button
+      style="background-color: #f25c05;"; class="ebts"
+      onclick="add_field('colors', '#f25c05')">&nbsp;</button><button
+    style="background-color: #260314;"; class="ebts" 
+    onclick="add_field('colors', '#260314')">&nbsp;</button>
+  &nbsp; <button class="ebt" onclick="select_colors(false)" style="width: 4em;"
+                 title="Select these colors.">Select</button>
+  </span>
+</p>
+<textarea id="colors" rows="1" cols="60" class="textar">
+|R : #f25c05 ; |G : #3e5916  ; |B : #a5afaa</textarea> 
+</div>
 
+</div> <!-- end right column -->
+
+<p class="headerp">
+  <button class="ebtl" style="width: 4em;" title="Show/Hide structure editing."
+          id="hide_struc_bt" onclick="toggle('struc')">Hide</button>
+  Edit Structure
+  <button class="ebtr" style="width: 4em;" title="Structure editing help."
+          onclick="show_help_struc()">Help</button>
+</p>
+
+<div id="div_struc_full">
 <p>Name &nbsp; &nbsp; &nbsp; &nbsp;
   <input id="struc-name" type="text" size="20" value="My Structure 1"
          style="width: 12em"></input>
@@ -475,8 +617,6 @@
   <span style="position: absolute; right: 2px;">
   <button class="ebts" title="Not equal. You can also write '<>' or '!='."
           onclick="add_field('relations', '≠')">≠</button><button
-    class="ebts" title="Less or equal. You can also write '=<'."
-    onclick="add_field('relations', '≤')">≤</button><button
       class="ebts" title="Conjunction. You can also write 'and' or '&'."
       onclick="add_field('relations', '∧')">∧</button><button
     class="ebts" title="Disjunction. You can also write 'or' or '|'."
@@ -493,7 +633,7 @@
                  title="Redraw current structure.">Draw</button>
   </span>
 </p>
-<textarea id="relations" rows="3" cols="60">
+<textarea id="relations" rows="3" cols="60" class="textar">
 E(x, y) = (&y = &x + 1) ∨ (&x=15 ∧ &y=1)
 </textarea> 
 
@@ -501,8 +641,6 @@
   <span style="position: absolute; right: 2px;">
   <button class="ebts" title="Not equal. You can also write '<>' or '!='."
           onclick="add_field('positions', '≠')">≠</button><button
-    class="ebts" title="Less or equal. You can also write '=<'."
-    onclick="add_field('positions', '≤')">≤</button><button
       class="ebts" title="Conjunction. You can also write 'and' or '&'."
       onclick="add_field('positions', '∧')">∧</button><button
     class="ebts" title="Disjunction. You can also write 'or' or '|'."
@@ -519,14 +657,23 @@
                  title="Redraw current structure.">Draw</button>
   </span>
 </p>
-<textarea id="positions" rows="3" cols="60">
+<textarea id="positions" rows="3" cols="60" class="textar">
 :x(a) = &a;
 :y(a) = &a · (10 - &a) / 10
 </textarea> 
+</div>
 
+<p class="headerp">
+  <button class="ebtl" style="width: 4em;" title="Show/Hide formula evaluator."
+          id="hide_formula_bt" onclick="toggle ('formula')">Hide</button>
+  Evaluate Formulas
+  <button class="ebtr" style="width: 4em;" title="Formula evaluator help."
+            onclick="show_help_formula()">Help</button>
+</p>
 
-<p style="width:100%; border-top: 1px solid; padding-top: 1em;">
-  Formula Name &nbsp; &nbsp; &nbsp; &nbsp;
+<div id="div_formula_full">
+<p>
+  Formula Name &nbsp; &nbsp;
   <input id="so-name" type="text" size="20" value="My Formula 1"
          style="width: 12em"></input>
   <span style="position: absolute; right: 2px;">
@@ -539,8 +686,6 @@
   <span style="position: absolute; right: 2px;">
   <button class="ebts" title="Not equal. You can also write '<>' or '!='."
           onclick="add_field('second-order', '≠')">≠</button><button
-    class="ebts" title="Less or equal. You can also write '=<'."
-    onclick="add_field('second-order', '≤')">≤</button><button
       class="ebts" title="Conjunction. You can also write 'and' or '&'."
       onclick="add_field('second-order', '∧')">∧</button><button
     class="ebts" title="Disjunction. You can also write 'or' or '|'."
@@ -554,42 +699,54 @@
     title="Universal Quantifier. You can also write 'all' or '\A'."
     class="ebts" onclick="add_field('second-order', '∀')">∀</button>
   &nbsp; <button class="ebt" onclick="find_draw_it()" style="width: 4em;"
-                 title="Find relations that satisfy the formula.">Find</button>
+                 title="Evaluate the formula.">Eval</button>
   </span>
 </p>
-<textarea id="second-order" rows="3" cols="60">
+<textarea id="second-order" rows="3" cols="60" class="textar">
 </textarea> 
 
 </div>
 
-<div style="position: absolute;  top: 4em; right: 0.5em; text-align: left">
-<p>Your Structures</p>
+<p class="headerp">
+  <button class="ebtl" style="width: 4em;" title="Show/Hide examples & saved."
+          id="hide_saved_bt" onclick="toggle('saved')">Hide</button>
+  Examples & Saved
+  <button class="ebtr" title="Saved structures and formulas help."
+          style="width: 4em;" onclick="show_help_saved()">Help</button>
+</p>
+
+<div id="div_saved_full">
+<p>Saved Structures</p>
 <ul id="saved-strucs" style="list-style: square; margin-left: -1.5em">
 <li>Nothing here yet</li>
 </ul>
 
-<p>Examples</p>
-<ul style="list-style: square; margin-left: -1.5em">
-<li><button class="obt" onclick="example_basic()">Basic Example</button></li>
-<li><button class="obt" onclick="example_primes()">Prime Numbers</button></li>
-<li><button class="obt" onclick="example_tc()">Transitive Closure</button></li>
-<li><button class="obt" onclick="example_heart()">Heart Drawing</button></li>
-</ul>
+<p>Examples
+<span style="position: absolute; right: 1px;">
+<button class="ebt" onclick="example_basic()">Basic</button>
+<button class="ebt" onclick="example_primes()">Primes</button>
+<button class="ebt" onclick="example_tc()">Simple TC</button>
+<button class="ebt" onclick="example_heart()">Heart</button>
+</span>
+</p>
 
-<p style="border-top: 1px solid; padding-top: 1em">Your Formulas</p>
+<p style="padding-right: 1.5em; text-align: left">Saved Formulas</p>
 <ul id="saved-so" style="list-style: square; margin-left: -1.5em">
 <li>Nothing here yet</li>
 </ul>
 
-<p>Examples</p>
-<ul style="list-style: square; margin-left: -1.5em">
-<li><button class="obt" onclick="example_2col()">2-coloring</button></li>
-<li><button class="obt" onclick="example_3col()">3-coloring</button></li>
-<li><button class="obt" onclick="example_matching()">Matching</button></li>
-</ul>
+<p>Examples
+<span style="position: absolute; right: 1px;">
+<button class="ebt" onclick="example_tc_so()">TC</button>
+<button class="ebt" onclick="example_2col()">2-coloring</button>
+<button class="ebt" onclick="example_3col()">3-coloring</button>
+<button class="ebt" onclick="example_matching()">Matching</button>
+</span>
+</p>
 
 </div>
 
+</div>
 
 <div id="bottom">
   <div id="bottomright">

Modified: trunk/Toss/Formula/BoolFormula.ml
===================================================================
--- trunk/Toss/Formula/BoolFormula.ml	2012-07-05 00:25:38 UTC (rev 1742)
+++ trunk/Toss/Formula/BoolFormula.ml	2012-07-06 01:06:25 UTC (rev 1743)
@@ -136,10 +136,12 @@
 let rec to_nnf ?(neg=false) = function
   | BVar v -> if neg then BVar (-1 * v) else BVar v
   | BNot phi -> if neg then to_nnf ~neg:false phi else to_nnf ~neg:true phi
-  | BAnd (flist) when neg -> BOr (List.map (to_nnf ~neg:true) flist)
-  | BAnd (flist) -> BAnd (List.map (to_nnf ~neg:false) flist)
-  | BOr (flist) when neg -> BAnd (List.map (to_nnf ~neg:true) flist)
-  | BOr (flist) -> BOr (List.map (to_nnf ~neg:false) flist)
+  | BAnd (flist) when neg ->
+    BOr (List.rev (List.rev_map (to_nnf ~neg:true) flist))
+  | BAnd (flist) -> BAnd (List.rev (List.rev_map (to_nnf ~neg:false) flist))
+  | BOr (flist) when neg ->
+    BAnd (List.rev (List.rev_map (to_nnf ~neg:true) flist))
+  | BOr (flist) -> BOr (List.rev (List.rev_map (to_nnf ~neg:false) flist))
 
 
 (* Helper function to flatten multiple or's and and's and sort by compare. *)
@@ -640,7 +642,8 @@
   List.filter (fun x -> List.for_all (fun y -> x=y || not(subset y x)) cnf) cnf
 
 let find_model phi =
-  let arg = flatten (to_nnf ~neg:true phi) in
+  let phi1 = to_nnf ~neg:true phi in
+  let arg = flatten phi1 in
   let (sep, aux_phi) = pg_auxcnf_of_bool_formula arg in
   match Sat.sat (listcnf_of_boolcnf aux_phi) with
     | None -> None
@@ -1005,8 +1008,8 @@
 let rec elim_quant_rec = function
   | QVar (v) -> BVar (v)
   | QNot (f) -> BNot (elim_quant_rec f)
-  | QAnd (l) -> BAnd (List.map elim_quant_rec l)
-  | QOr (l) -> BOr (List.map elim_quant_rec l)
+  | QAnd (l) -> BAnd (List.rev_map elim_quant_rec l)
+  | QOr (l) -> BOr (List.rev_map elim_quant_rec l)
   | QEx (vars, qphi) ->
     Hashtbl.clear has_vars_mem;
     let inside, len = elim_quant_rec qphi, List.length vars in

Modified: trunk/Toss/README
===================================================================
--- trunk/Toss/README	2012-07-05 00:25:38 UTC (rev 1742)
+++ trunk/Toss/README	2012-07-06 01:06:25 UTC (rev 1743)
@@ -28,6 +28,7 @@
 - Diana Fischer
 - Tobias Ganzow
 - Simon Leßenich
+- Sasha Rubin
 - Michał Wójcik
 
 Yet another group of people worked on the oldest version of Toss (around 2004).

Modified: trunk/Toss/www/contact.xml
===================================================================
--- trunk/Toss/www/contact.xml	2012-07-05 00:25:38 UTC (rev 1742)
+++ trunk/Toss/www/contact.xml	2012-07-06 01:06:25 UTC (rev 1743)
@@ -93,6 +93,7 @@
       <item>Diana Fischer</item>
       <item>Tobias Ganzow</item>
       <item>Simon Leßenich</item>
+      <item>Sasha Rubin</item>
       <item>Michał Wójcik</item>
     </itemize>
     <par>Yet another group of people, who worked on the oldest version of Toss

This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.