<?php // $Id: uUpdateBibref.php,v 1.1 2005/10/27 10:11:19 geothms Exp geothms $
session_start();
$pTipoUtilizador = $_SESSION['tipoUtilizador'];
if ($pTipoUtilizador=="anonymous" || $pTipoUtilizador=="regular") { // separa por tipo de utilizador
  require('headersubsubUsers.inc');
  require('menusubsubUsers.inc');
}
else {
  require('headersubsubAdmins.inc');
  require('menusubsubAdmins.inc');
}
?>


<hr/>



<?php
require('loginsub.php');
?>


<center>
<h3 class="maketitle">Geometric Proof Details</h3>
</center>

<hr/>

<?php
$argumento = $_GET['argumento'];

// cria uma pesquisa
$sqlDem = "SELECT teoId,proverId,code,codeXML,proof,dateSubmission,
                  proof,proofXML,userId,bibref,status
             FROM demonstrations
            WHERE demId='$argumento'";


$resultadoDem = mysql_query($sqlDem,$ligacao);
$ncamposDem =mysql_num_fields($resultadoDem);
$linhaDem = mysql_fetch_assoc($resultadoDem);

$pThmId          = trim($linhaDem['teoId']);
$pPrvId          = trim($linhaDem['proverId']);
$pCode           = trim($linhaDem['code']);
$pProof          = trim($linhaDem['proof']);
$pDateSubmission = trim($linhaDem['dateSubmission']);
$pUserId         = trim($linhaDem['userId']);
$pBibref         = trim($linhaDem['bibref']);
$pStatus         = trim($linhaDem['status']);
$ficheiroCodeXML = $linhaDem["codeXML"]; 
$ficheiroPDF     = $linhaDem["proof"]; 
// não esquecer que o ficheiro XML foi guardado compactado (bz2)
$ficheiroBZ2     = $linhaDem["proofXML"]; 




// Obtém o nome do Teorema
$sqlThm = "SELECT teoName
             FROM theorems
            WHERE teoId='$pThmId'";
$resultadoThm = mysql_query($sqlThm,$ligacao);
$linhaThm = mysql_fetch_assoc($resultadoThm);


// Obtém o nome do Provador
$sqlPrv = "SELECT name,version
             FROM provers
            WHERE proverId='$pPrvId'";
$resultadoPrv = mysql_query($sqlPrv,$ligacao);
$linhaPrv = mysql_fetch_assoc($resultadoPrv);

// Obtém o identificador do Utilizador
$sqlUsr = "SELECT name,email
             FROM users
            WHERE userId='$pUserId'";
$resultadoUsr = mysql_query($sqlUsr,$ligacao);
$linhaUsr = mysql_fetch_assoc($resultadoUsr);


$pThmName    = trim($linhaThm['teoName']);

$pPrvName    = trim($linhaPrv['name']);
$pPrvVersion = trim($linhaPrv['version']);

$pUserName   = trim($linhaUsr['name']);
$pUserEmail  = trim($linhaUsr['email']);

// Escreve o ficheiro ".code" referente ao código - comum

// Nome do ficheiro do código em formato XML  
$vNameProofCode = 'proofCode'.$pUserId.'.txt';

ob_start();
print $pCode."\n";
$texfile=fopen($vNameProofCode,"w");
fwrite($texfile,ob_get_contents()); 
fclose($texfile); 
ob_end_clean(); 

//
// Processamento dos ficheiros referente ao código em formato XML e
// das provas em formato PDF e XML - dependente do Provador
//
if ($pPrvId==2) // GCLCprover
  require('processFilesGCLCprover.php');
elseif ($pPrvId==3) // GCLCprover+euk2gclc 
// ---> tenho de ver isto com mais cuidado
  require('processFilesGCLCproverEuk.php');
elseif ($pPrvId==4) //Coq+JNarboux (por antecipação)
  require('processFilesCoqJN.php');
//
//

echo "<!-- ficha -->";
echo "<table width='100%' bgcolor='white' cellpadding='4' cellspacing='4'>";
echo "<tr>";
echo "<td width='100%' colspan='6' align='center'><span class='titulo'>Geometric Proofs Info</span></td>"; 
echo "</tr>";
echo "<tr>";
echo "<tr>";
echo "<td width='16.6%'><span class='ficha'>Theorem Id</span></td>";
echo "<td width='16.6%'>$pThmId</td>";
echo "<td width='16.6%'><span class='ficha'>Theorem Name</span></td>";
echo "<td width='50%' colspan='3'>$pThmName</td>";
echo "</tr>";

echo "<tr>";
echo "<td width='16.6%'><span class='ficha'>Prover Name</span></td>";
echo "<td width='33.3%' colspan='2'>$pPrvName</td>";
echo "<td width='16.6%'><span class='ficha'>Prover Version</span></td>";
echo "<td width='33.3%' colspan='2'>$pPrvVersion</td>";
echo "</tr>";
echo "<tr>";
echo "<td width='16.6%' colspan='1'><span class='ficha'>Code</span></td>";
echo "<td width='83.4%' colspan='5'><a href='$vNameProofCode'>code.txt (text File)</a> </td>";
echo "</tr>";
//
// Ficheiro XML com o código - dependente do Provador
//
if ($pPrvId==2) // GCLCprover
  require('codeXMLGCLCprover.php');
elseif ($pPrvId==3) // GCLCprover+euk2gclc -> CUIDADO
  require('codeXMLGCLCproverEuk.php');
elseif ($pPrvId==4) //Coq+JNarboux (por antecipação)
  require('codeXMLCoqJN.php');
//
//
echo "<tr>";
echo "<td width='16.6%' colspan='1'><span class='ficha'>Proof Status</span></td>";
if ($pStatus='Proved') 
  echo "<td width='83.4%' colspan='5'><font color='green'><b>$pStatus</b></font></td>";
else
  echo "<td width='83.4%' colspan='5'><font color='red'><b>$pStatus</b></font></td>";
echo "</tr>";
//
// E agora a apresentação da prova em PDF e XML - depende do provador
//
if ($pPrvId==2) // GCLCprover
  require('proofGCLCprover.php');
elseif ($pPrvId==3) // GCLCprover+euk2gclc 
// ---> tenho de ver isto com mais cuidado
  require('proofGCLCproverEuk.php');
elseif ($pPrvId==4) //Coq+JNarboux (por antecipação)
  require('proofCoqJN.php');
//
//
echo "<tr>"; 
echo "<td width='16.6%' colspan='1'><span class='ficha'>Date of Submission</span></td>";
echo "<td width='33.3%' colspan='2'>$pDateSubmission</td>"; 
echo "<td width='33.3%' colspan='2'>Bibliographic Reference</td>"; 
echo "<td width='16.6%' colspan='1'>$pBibref</td>"; 
echo "</tr>";
echo "<tr>";
echo "<td width='16.6%' colspan='1'><span class='ficha'>Contributor's Name</span></td>";
echo "<td width='83.4%' colspan='5'>$pUserName</td>";
//echo "<td width='16.6%' colspan='1'><span class='ficha'>Email</span></td>";
//echo "<td width='33.3%' colspan='2'>$pUserEmail</td>";
echo "</tr>";
//
// Medidas de Eficiência - depende do provador
//
if ($pPrvId==2) // GCLCprover
  require('measuresEfficiencyGCLCprover.php');
elseif ($pPrvId==3) // GCLCprover+euk2gclc 
// ---> tenho de ver isto com mais cuidado
  require('measuresEfficiencyGCLCproverEuk.php');
elseif ($pPrvId==4) //Coq+JNarboux (por antecipação)
  require('measuresEfficiencyCoqJN.php');
echo "</table>";
?>

<hr/>

<?php
  require('footer.inc');
?>
