helm/software/matita/scripts/public_html/showquery.php

   1 <?php require("common.php");
   2
   3   $query = stripslashes($_GET['query']);
   4
   5   $nqs = explode('###',$query);
   6
   7   $qs = array();
   8   foreach($nqs as $v){
   9     $x = explode("@@@",$v);
  10     $qs[$x[0]] = $x[1];
  11   }
  12
  13 function prettify($s,$name) {
  14   if (preg_match("/^[0-9]{12}$/",$s)) {
  15     $year = substr($s,0,4);
  16     $month = substr($s,4,2);
  17     $day = substr($s,6,2);
  18     $hour = substr($s,8,2);
  19     $minute = substr($s,10,2);
  20     return $day . "/" . $month . "/" . $year . " " . $hour . ":" . $minute;
  21   } else if ($name == "sum_time" || $name == "sum_timeuser"){
  22     $min = floor($s / 6000);
  23     $sec = floor(($s - $min * 6000) / 100);
  24     $cents = $s % 100;
  25     return $min . "m" . $sec . "." . $cents . "s";
  26   } else
  27     return $s;
  28 }
  29
  30 function printer($q){
  31   global $i;
  32   echo "<tr>";
  33   if ( $i == 0) {
  34       foreach( $q as $name => $txt) {
  35           echo "<th>$name</th>";
  36       }
  37   }
  38   echo "</tr>\n";
  39   if ( $i%2 == 0)
  40      echo "<tr class=\"even\">";
  41   else
  42      echo "<tr class=\"odd\">";
  43   foreach( $q as $name => $txt) {
  44      echo "<td>" . prettify($txt,$name) . "</td>";
  45   }
  46   echo "</tr>\n";
  47   $i++;
  48 }
  49
  50 ?>
  51 <html>
  52   <head>
  53   <link type="text/css" rel="stylesheet" href="style.css"/>
  54   </head>
  55   <body>
  56     <h1>QUERY results</h1>
  57 <? foreach( $qs as $name => $q) { $i=0;?>
  58     <h2><? echo $name; ?></h2>
  59     <p>
  60     <tt><? print $q; ?></tt>
  61     </p>
  62     <table border=1>
  63     <?  query($q,"printer"); ?>
  64     </table>
  65 <? } ?>
  66     <p><a href="bench.php">BACK to the query page</a></p>
  67   </body>
  68 </html>