X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fscripts%2Fpublic_html%2Fshowquery.php;h=dfa0b473068144d1e12e90c6718e45822b7a3d60;hb=536be1abc85882d042c31e301299c90786c9a355;hp=7f4a411241944a790f0615026620b8332e0495be;hpb=d40d7f30d3a6656a9612388ee7b512fb4ca1e5e4;p=helm.git
diff --git a/helm/software/matita/scripts/public_html/showquery.php b/helm/software/matita/scripts/public_html/showquery.php
index 7f4a41124..dfa0b4730 100644
--- a/helm/software/matita/scripts/public_html/showquery.php
+++ b/helm/software/matita/scripts/public_html/showquery.php
@@ -7,46 +7,13 @@
$qs = array();
foreach($nqs as $v){
$x = explode("@@@",$v);
- $qs[$x[0]] = $x[1];
+ if ($x[1] == NULL) {
+ $qs["Unnamed"] = $x[0];
+ } else {
+ $qs[$x[0]] = $x[1];
+ }
}
-function prettify($s,$name) {
- if (preg_match("/^[0-9]{12}$/",$s)) {
- $year = substr($s,0,4);
- $month = substr($s,4,2);
- $day = substr($s,6,2);
- $hour = substr($s,8,2);
- $minute = substr($s,10,2);
- return $day . "/" . $month . "/" . $year . " " . $hour . ":" . $minute;
- } else if ($name == "sum_time" || $name == "sum_timeuser" || $name == "time" || $name == "time_user" ){
- $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){
- global $i;
- echo "";
- if ( $i == 0) {
- foreach( $q as $name => $txt) {
- echo "| $name | ";
- }
- }
- echo "
\n";
- if ( $i%2 == 0)
- echo "";
- else
- echo "
";
- foreach( $q as $name => $txt) {
- echo "| " . prettify($txt,$name) . " | ";
- }
- echo "
\n";
- $i++;
-}
-
?>
@@ -57,7 +24,7 @@ function printer($q){
$q) { $i=0;?>
-
+