moved to the new table

diff --git a/matita/scripts/public_html/bench.php b/matita/scripts/public_html/bench.php
index ed5572b9f827415b3e7c4c4e70babc0be41295f1..f11994ec158f9b068425232b583d3dbdf32e3279 100644 (file)
--- a/matita/scripts/public_html/bench.php
+++ b/matita/scripts/public_html/bench.php
@@ -97,45 +97,65 @@ function links_of($name,$q,$limits){
   <tr>
     <td>Marks:</td>
     <td> 
-      <? array_to_combo("mark",
-            query("select distinct mark from bench order by mark desc;")); ?>
+      <select name="mark">";
+        <option value="--">--</option>";
+        <?query("select distinct mark from bench order by mark desc;",
+            "array_to_combo");?>
+      </select>      
     </td>
   </tr>
   <tr>
     <td>Compilations:</td>
     <td> 
-      <? array_to_combo("compilation",
-           query("select distinct compilation from bench;")); ?>
+      <select name="compilation">";
+        <option value="--">--</option>";
+          <?query("select distinct compilation from bench;","array_to_combo");?>
+      </select>      
     </td>
   </tr>
   <tr>
     <td>Options:</td>
     <td>  
-      <?array_to_combo("options",query("select distinct options from bench;"));?>
+      <select name="options">";
+        <option value="--">--</option>";
+          <?query("select distinct options from bench;","array_to_combo");?>
+      </select>      
     </td>
   </tr>
   <tr>
     <td>Tests:</td>
     <td>    
-      <? array_to_combo("test",query("select distinct test from bench;")); ?>
+      <select name="test">";
+        <option value="--">--</option>";
+          <?query("select distinct test from bench;","array_to_combo");?>
+      </select>      
     </td>
   </tr>
   <tr>
     <td>Test results:</td>
     <td>
-      <? array_to_combo("result",query("select distinct result from bench;")); ?>
+      <select name="result">";
+        <option value="--">--</option>";
+          <?query("select distinct result from bench;","array_to_combo"); ?>
+      </select>      
     </td>
   </tr>
   <tr>
     <td>Group By: </td>
     <td>
-      <? array_to_combo("groupby",array(array("mark","options"))); ?>
+      <select name="groupby">";
+        <option value="--">--</option>";
+        <? array_to_combo(array("mark"));array_to_combo(array("options")); ?>
+      </select>      
     </td>
   </tr>
   <tr>
     <td>Limit: </td>
     <td>
-      <? array_to_combo("limit",array($limits)); ?>
+      <select name="limit">";
+        <option value="--">--</option>";
+      <? foreach(array($limits) as $l) {array_to_combo($l);} ?>
+      </select>      
     </td>
   </tr>
   <tr>

diff --git a/matita/scripts/public_html/common.php b/matita/scripts/public_html/common.php
index 5b9f51e5dc68cc488bb66d2b4ee79528a2ebf3bc..ca853603da39838e3ab1cc239fa555b3f8c090ff 100644 (file)
--- a/matita/scripts/public_html/common.php
+++ b/matita/scripts/public_html/common.php
@@ -1,5 +1,11 @@
 <?php
 
+function array_to_combo($a) {
+  foreach($a as $k => $v){
+    echo "<option value=\"{$v}\">{$v}</option>";
+  }
+}
+
 function query($q,$f) {
   $db = mysql_pconnect("localhost","helm");
   mysql_select_db("matita");
@@ -25,15 +31,4 @@ function time_2_cents($t) {
   return ((int) $t_cents) + ((int) $t_secs) * 100 + ((int)$t_minutes) * 6000 ;
 }
 
-function array_to_combo($l,$a) {
-  echo "<select name=\"$l\">";
-  echo "<option value=\"--\">--</option>";
-  foreach ($a as $k => $v) {
-    foreach( array_keys($v) as $k1 => $i) {
-      echo "<option value=\"{$v[$i]}\">{$v[$i]}</option>";
-    }
-  }
-  echo "</select>";
-}
-
 ?>

diff --git a/matita/scripts/public_html/showquery.php b/matita/scripts/public_html/showquery.php
index 1e385d46ee1ad57e86584aaeaf40def1670671bb..007f37217daa968adc5444d4a26bfcc82b94e4f9 100644 (file)
--- a/matita/scripts/public_html/showquery.php
+++ b/matita/scripts/public_html/showquery.php
@@ -10,7 +10,7 @@
     $qs[$x[0]] = $x[1];
   }
 
-function prettify($s) {
+function prettify($s,$name) {
   if (preg_match("/^[0-9]{12}$/",$s)) {
     $year = substr($s,0,4);
     $month = substr($s,4,2);
@@ -18,6 +18,11 @@ function prettify($s) {
     $hour = substr($s,8,2);
     $minute = substr($s,10,2);
     return $day . "/" . $month . "/" . $year . " " . $hour . ":" . $minute;
+  } else if ($name == "sum_time" || $name == "sum_timeuser"){
+    $min = floor($s / 6000);
+    $sec = floor(($s - $min * 6000) / 100);
+    $cents = $s % 100;
+    return $min . "m" . $sec . "." . $cents . "s";
   } else
     return $s;
 }
@@ -31,18 +36,14 @@ function printer($q){
         }
       echo "</tr>\n";
   } else {
-      $i=0;
-      foreach ($q as $k => $v) {
-        $i = $i + 1;
-        if ( $i%2 == 0)
-          echo "<tr class=\"even\">";      
-        else
-          echo "<tr class=\"odd\">";
-        foreach( $v as $name => $txt) {
-          echo "<td>" . prettify($txt) . "</td>";
-        }
-        echo "</tr>\n";      
+      if ( $i%2 == 0)
+        echo "<tr class=\"even\">";      
+      else
+        echo "<tr class=\"odd\">";
+      foreach( $q as $name => $txt) {
+        echo "<td>" . prettify($txt,$name) . "</td>";
       }
+      echo "</tr>\n";      
   }
   $i++;
 }
@@ -60,7 +61,7 @@ function printer($q){
     <tt><? print $q; ?></tt>
     </p>
     <table border=1>
-    <?  query($q,&$printer); ?>
+    <?  query($q,"printer"); ?>
     </table>
 <? } ?>
     <p><a href="bench.php">BACK to the query page</a></p>