X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fscripts%2Fpublic_html%2Fcommon.php;h=d56c9d40bf5b5d4b1eab1df4afb59737547c4048;hb=c52baa34c7363fa58f81aea95bb0d72e10afdaf1;hp=f2a9be030ea5e26c36788fa13b2bbbd8c9945baa;hpb=55b82bd235d82ff7f0a40d980effe1efde1f5073;p=helm.git diff --git a/helm/software/matita/scripts/public_html/common.php b/helm/software/matita/scripts/public_html/common.php index f2a9be030..d56c9d40b 100644 --- a/helm/software/matita/scripts/public_html/common.php +++ b/helm/software/matita/scripts/public_html/common.php @@ -1,28 +1,69 @@ $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 "
" . $q . ""); + return; } $rc = mysql_query($q,$db); if(!$rc) { die("Query failed: " . mysql_error()); } - $result = array(); while( $row = mysql_fetch_array($rc, MYSQL_ASSOC)){ - $result[] = $row; + $f($row); } mysql_free_result($rc); mysql_close($db); - if ($group_by){ - return group_array_by_mark($result); - } else { - return $result; - } } function time_2_cents($t) { @@ -36,54 +77,4 @@ function time_2_cents($t) { return ((int) $t_cents) + ((int) $t_secs) * 100 + ((int)$t_minutes) * 6000 ; } -function sum_time($t1, $t2) { - $matches1 = array(); - $matches2 = array(); - $rex = "/^(\d+)m(\d\d?)\.(\d{2})s$/"; - $m1 = preg_match($rex,$t1,$matches1); - $m2 = preg_match($rex,$t2,$matches2); - if ($m1 != 0 && $m2 != 0) { - $t1_minutes = $matches1[1]; - $t2_minutes = $matches2[1]; - $t1_secs = $matches1[2]; - $t2_secs = $matches2[2]; - $t1_cents = $matches1[3]; - $t2_cents = $matches2[3]; - $time1 = ((int) $t1_cents) + ((int) $t1_secs) * 100 + ((int)$t1_minutes) * 6000 ; - $time2 = ((int) $t2_cents) + ((int) $t2_secs) * 100 + ((int)$t2_minutes) * 6000 ; - $sum = $time1 + $time2; - $min = $sum / 6000; - $sec = ($sum % 6000) / 100; - $cent = ($sum % 6000) % 100; - return sprintf("%dm%02d.%02ds",$min,$sec,$cent); - } else { - return $t1; - } -} - -function group_array_by_mark($a) { - $rc = array(); - foreach ($a as $x) { - if ($rc[$x['mark']] == NULL) { - $rc[$x['mark']] = $x; - } else { - foreach ($rc[$x['mark']] as $k => $v) { - $rc[$x['mark']][$k] = sum_time($v, $x[$k]); - } - } - } - return array_values($rc); -} - -function array_to_combo($l,$a) { - echo ""; -} - ?>