X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fscripts%2Fpublic_html%2Fcommon.php;h=48121b5498ad748ff80ffff815bdd6fef0bfb483;hb=61f668ed13ab3e78e97df426988392055afb0523;hp=ca853603da39838e3ab1cc239fa555b3f8c090ff;hpb=7fbb1eb57d3d8fffdf5398bc3b16adea58f143ed;p=helm.git diff --git a/helm/software/matita/scripts/public_html/common.php b/helm/software/matita/scripts/public_html/common.php index ca853603d..48121b549 100644 --- a/helm/software/matita/scripts/public_html/common.php +++ b/helm/software/matita/scripts/public_html/common.php @@ -1,14 +1,59 @@ $v){ echo ""; } } +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 (preg_match("/time/",$name)){ + $min = floor($s / 6000); + $sec = floor(($s - $min * 6000) / 100); + $cents = $s % 100; + return $min . "m" . $sec . "." . $cents . "s"; + } else + return rtrim($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++; +} + + function query($q,$f) { $db = mysql_pconnect("localhost","helm"); mysql_select_db("matita"); + if (!preg_match("/^(select|describe)[^\n;]*;?$/i",$q)) { + echo "Query not allowed!"; + return; + } $rc = mysql_query($q,$db); if(!$rc) { die("Query failed: " . mysql_error());