1<?php 2 3$_GET["lang"] = "en"; 4if (!isset($_GET["lang"])) { 5 header("Location: http://php.net"); 6 exit; 7} 8if (empty($_SERVER["DOCUMENT_ROOT"])) { 9 $_SERVER["DOCUMENT_ROOT"] = __DIR__ . "/../"; 10} 11include __DIR__ . '/../include/prepend.inc'; 12if (!isset($ACTIVE_ONLINE_LANGUAGES[$_GET["lang"]])) { 13 header("Location: http://php.net"); 14} 15$lang = $_GET["lang"]; 16 17/* 18$types = array( 19 "phpdoc:varentry", 20 "refentry", 21 "phpdoc:exceptionref", 22 "phpdoc:classref", 23 "section", 24 "chapter", 25 "book", 26 "reference", 27 "set", 28 "appendix", 29 "article", 30); 31 */ 32 33$indexfile = $_SERVER["DOCUMENT_ROOT"] . "/manual/$lang/search-index.json"; 34$descfile = $_SERVER["DOCUMENT_ROOT"] . "/manual/$lang/search-description.json"; 35 36/* {{{ Cache this */ 37$time = max(filemtime($indexfile), filemtime($descfile)); 38$tsstring = gmdate("D, d M Y H:i:s ", $time) . "GMT"; 39if (isset($_SERVER["HTTP_IF_MODIFIED_SINCE"]) && 40 ($_SERVER["HTTP_IF_MODIFIED_SINCE"] == $tsstring)) { 41 header("HTTP/1.1 304 Not Modified"); 42 exit; 43} 44 45header("Last-Modified: " . $tsstring); 46header("Content-Type: application/javascript"); 47/* }}} */ 48 49$s = file_get_contents($indexfile); 50$js = json_decode($s, true); 51 52$index = []; 53foreach ($js as $item) { 54 if ($item[0]) { 55 /* key: ID/filename, 0=>*/ 56 $index[$item[1]] = [$item[0], "", $item[2]]; 57 } 58} 59 60$s = file_get_contents($descfile); 61$js = json_decode($s, true); 62 63foreach ($js as $k => $item) { 64 if ($item && isset($index[$k])) { 65 $index[$k][1] = $item; 66 } 67} 68 69echo json_encode($index); 70
