X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fscripts%2Fpublic_html%2Fshowquery.php;h=886cb3390cb1f5b5c2411be5802c810e6c4994c2;hb=4ee27d158de49af15c1f21ad50474744720a537a;hp=1e385d46ee1ad57e86584aaeaf40def1670671bb;hpb=efa5deb1fc321a117344464ad73f59254d832fb9;p=helm.git

diff --git a/matita/scripts/public_html/showquery.php b/matita/scripts/public_html/showquery.php
index 1e385d46e..886cb3390 100644
--- 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,32 +18,32 @@ 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;
 }
   
 function printer($q){
   static $i = 0;
+  echo "<tr>";
   if ( $i == 0) {
-      echo "<tr>";
       foreach( $q as $name => $txt) {
           echo "<th>$name</th>";
-        }
-      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";      
       }
   }
+  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 +60,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>