NEW FEATURE: provide an RSS feed for each user showing in which games it's his turn

[e-DoKo.git] / include / output.php

diff --git a/include/output.php b/include/output.php
index 57b3152c035ea29efc511af39670308606951e23..61fef6004fbe5d60d8c1087ec5db8ad54edc1570 100644 (file)
--- a/include/output.php
+++ b/include/output.php
@@ -380,39 +380,44 @@ function output_footer()
 
 function output_status()
 {
-  global $defaulttimezone,$INDEX,$WIKI;
-   if(isset($_SESSION["name"]))
-     {
-       $name = $_SESSION["name"];
-
-       /* logout info */
-       echo "\n<div class=\"status\">\n";
-       echo $name,"\n";
-       echo " | <a href=\"".$INDEX."\"> mypage </a>\n";
-       echo " | <a href=\"".$INDEX."?action=prefs\">settings</a>\n";
-       echo " | <a href=\"".$INDEX."?action=new\">new game</a>\n";
-       echo " | <a href=\"".$INDEX."?action=stats\">statistics</a>\n";
-       echo " | <a href=\"".$WIKI."\">wiki</a>\n";
-       echo " |&nbsp;&nbsp;&nbsp; <a href=\"".$INDEX."?action=logout\">logout</a>\n";
-       echo "</div>\n";
-
-       /* last logon time */
-       $myid  = DB_get_userid("name",$name);
-       $zone  = DB_get_user_timezone($myid);
-
-       $time     = DB_get_user_timestamp($myid);
-       date_default_timezone_set($defaulttimezone);
-       $unixtime = strtotime($time);
-       date_default_timezone_set($zone);
-
-       echo "<div class=\"lastlogin\"><span>last login: ".date("r",$unixtime)."</span></div>\n";
-     }
-   else
-     {
-       echo "\n<div class=\"status\">\n";
-       echo "<a href=\"".$INDEX."\">login</a>\n";
-       echo "</div>\n";
-     }
+  global $defaulttimezone, $INDEX, $WIKI, $RSS;
+
+  if(isset($_SESSION["name"]))
+    {
+      $name = $_SESSION["name"];
+
+      /* last logon time */
+      $myid  = DB_get_userid("name",$name);
+      $zone  = DB_get_user_timezone($myid);
+
+      $time     = DB_get_user_timestamp($myid);
+      date_default_timezone_set($defaulttimezone);
+      $unixtime = strtotime($time);
+      date_default_timezone_set($zone);
+
+      /* rss token */
+      $token = get_user_token($myid);
+
+      /* logout info */
+      echo "\n<div class=\"status\">\n";
+      echo $name,"\n";
+      echo " | <a href=\"".$INDEX."\"> mypage </a>\n";
+      echo " | <a href=\"".$INDEX."?action=prefs\">settings</a>\n";
+      echo " | <a href=\"".$INDEX."?action=new\">new game</a>\n";
+      echo " | <a href=\"".$INDEX."?action=stats\">statistics</a>\n";
+      echo " | <a href=\"".$WIKI."\">wiki</a>\n";
+      echo " | <a href=\"".$RSS."?uid=".$myid."&amp;token=".$token."\">rss</a>\n";
+      echo " |&nbsp;&nbsp;&nbsp; <a href=\"".$INDEX."?action=logout\">logout</a>\n";
+      echo "</div>\n";
+
+      echo "<div class=\"lastlogin\"><span>last login: ".date("r",$unixtime)."</span></div>\n";
+    }
+  else
+    {
+      echo "\n<div class=\"status\">\n";
+      echo "<a href=\"".$INDEX."\">login</a>\n";
+      echo "</div>\n";
+    }
   return;
 }