X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fscripts%2Fpublic_html%2Fcommon.php;h=d56c9d40bf5b5d4b1eab1df4afb59737547c4048;hb=974bd74ea4b4cf56863d25b1fe5c3c50886e8e12;hp=5b9f51e5dc68cc488bb66d2b4ee79528a2ebf3bc;hpb=efa5deb1fc321a117344464ad73f59254d832fb9;p=helm.git diff --git a/matita/scripts/public_html/common.php b/matita/scripts/public_html/common.php index 5b9f51e5d..d56c9d40b 100644 --- a/matita/scripts/public_html/common.php +++ b/matita/scripts/public_html/common.php @@ -1,8 +1,60 @@ $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()); @@ -25,15 +77,4 @@ function time_2_cents($t) { return ((int) $t_cents) + ((int) $t_secs) * 100 + ((int)$t_minutes) * 6000 ; } -function array_to_combo($l,$a) { - echo ""; -} - ?>