<?php

// visit ..../filer.php?name.ext to push name.ext to the browser
// each push will generate a line in a log file logging the date/time and IP
// address of the browser

// log file for name.ext is nameext.log

// only handles specific file types, based on extensions.
// currently handles .pdf, .PDF, .txt, .tex, .hs

// for security, checks that the file exists, and disallows / in filename

// pcs 9/3/13

$filename = $_GET['name'];

$legal = file_exists($filename) && (strpos($filename,'/') == FALSE);

if ($legal) {
  $extension = pathinfo($filename, PATHINFO_EXTENSION);

  $logfilename = preg_replace ("/\./", "", $filename) . ".log";
  
  $time = date("G:i:s M j Y");
  $line = "downloaded by " . $_SERVER['REMOTE_ADDR'] . " at $time\n";
  
  if ($extension ==  "pdf" or $extension == "PDF") {
    $type = "application/pdf";
  } else if ($extension == "txt" or $extension == "TXT") {
    $type = "text/plain";
  } else if ($extension == "tex") {
    $type = "text/plain";
  } else if ($extension == "hs") {
    $type = "text/plain";
  }
  
  if ($type) {
    file_put_contents($logfilename, $line, FILE_APPEND);
    
    header("Content-type: $type");
    header("Content-Disposition: inline; filename=$filename");
    header("Content-Length: " . filesize($filename));
    readfile($filename);
  }
} else { // illegal filename
    header("Content-type: $type");
    header("Content-Disposition: inline; filename=$filename");
    header("Content-Length: " . filesize($filename));
    echo "<html><body>Illegal file name!</body></html>";
}  
  
?>