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   static $i = 0;
  32   if ( $i == 0) {
  33       echo "<tr>";
  34       foreach( $q as $name => $txt) {
  35           echo "<th>$name</th>";
  36         }
  37       echo "</tr>\n";
  38   } else {
  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   }
  48   $i++;
  49 }
  50
  51 ?>
  52 <html>
  53   <head>
  54   <link type="text/css" rel="stylesheet" href="style.css"/>
  55   </head>
  56   <body>
  57     <h1>QUERY results</h1>
  58 <? foreach( $qs as $name => $q) { ?>
  59     <h2><? echo $name; ?></h2>
  60     <p>
  61     <tt><? print $q; ?></tt>
  62     </p>
  63     <table border=1>
  64     <?  query($q,"printer"); ?>
  65     </table>
  66 <? } ?>
  67     <p><a href="bench.php">BACK to the query page</a></p>
  68   </body>
  69 </html>