From cd644cf892ccd05a6411f73a76e41924ade236fa Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sat, 24 Dec 2005 14:40:26 +0000 Subject: [PATCH] beauty\! --- helm/matita/scripts/public_html/showquery.php | 21 +++++++++++++++++-- helm/matita/scripts/public_html/style.css | 20 ++++++++++++++++++ 2 files changed, 39 insertions(+), 2 deletions(-) diff --git a/helm/matita/scripts/public_html/showquery.php b/helm/matita/scripts/public_html/showquery.php index bd54d6a63..e7db764d8 100644 --- a/helm/matita/scripts/public_html/showquery.php +++ b/helm/matita/scripts/public_html/showquery.php @@ -10,6 +10,18 @@ $qs[$x[0]] = $x[1]; } +function prettify($s) { + 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 + return $s; +} + ?> @@ -30,10 +42,15 @@ echo "$name"; } echo "\n"; + $i=0; foreach ($q as $k => $v) { - echo ""; + $i = $i + 1; + if ( $i%2 == 0) + echo ""; + else + echo ""; foreach( $v as $name => $txt) { - echo "$txt"; + echo "" . prettify($txt) . ""; } echo "\n"; } diff --git a/helm/matita/scripts/public_html/style.css b/helm/matita/scripts/public_html/style.css index 17c66f428..dc2df470d 100644 --- a/helm/matita/scripts/public_html/style.css +++ b/helm/matita/scripts/public_html/style.css @@ -33,3 +33,23 @@ li { ul { list-style-type: upper-roman; } + +table, td { + border-style:none; + padding: 2px 6px 2px 6px; +} + +tr.odd { + background-color:#EEEEEE; +} +tr.even { + background-color:#CECECE; +} + +th { + border-style:solid; + border-width:0px 0px 1px 0px; + border-color: gray; +} + + -- 2.39.2