$resultStr); echo json_encode($HTMLJSON); ?>