<?php // $Id:$
session_start();
$pTipoUtilizador = $_SESSION['tipoUtilizador'];
if ($pTipoUtilizador=="anonymous" || $pTipoUtilizador=="regular") { // separa por tipo de utilizador
  require('headersubUsers.inc');
  require('menusubUsers.inc');
  echo "<meta http-equiv='refresh' content='0; url=../users.php' />";
  exit;  // os anonimos não têem acesso a esta página
}
else {
  require('headersubAdmins.inc');
  require('menusubAdmins.inc');
}
?>


<center>
<h3 class="maketitle">Geometric theorems - Insert a New Theorem</h3>
</center>

<hr/>



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

<?php

// Obtêm os valores do formulário.
$pTeoId            = $_POST['TeoId'];
$pDateSubmission   = $_POST['DateSubmission'];
$pUserId           = $_POST['UserId'];
$pPrvIdNameVersion = $_POST['PrvIdNameVersion'];
$pBibref           = $_POST['BibrefPrv'];
$pCode             = $_POST['CodePrv'];


// Como obter de um campo múltipo os valores individuais através de exp. reg.

// ProverId
preg_match("§([A-Za-z0-9 _.]+) -- ([A-Za-z0-9 _.]+) -- ([A-Za-z0-9 _.]+)§",$pPrvIdNameVersion,$matches);

$pPrvId = $matches[1];

// Formata os valores para posterior inserção na Tabela
if (!get_magic_quotes_gpc())
  { //    $pNumeroIdentificacao = addslashes($pNumeroIdentificacao);
    $pTeoId           = addslashes($pTeoId);
    $pPrvId           = addslashes($pPrvId);
    $pCode            = addslashes($pCode);
    $pDateSubmission  = addslashes($pDateSubmission);
    $pBibref          = addslashes($pBibref);
    $pUserId          = addslashes($pUserId);
  }


// Começa-se por introduzir os dados gerais e depois vai-se, provador a
// provador, processar a prova e fazer a inserção desta. Se Houver
// Erros É Necessário Desfazer (I.E. Transações) A Inserção Já Efectuada,
// só no caso de tudo correr bem é que se fecha a Transação

// Inicio da transaccao
@ mysql_query("BEGIN");

// Inserção dos dados gerais

// Para as referências bibliográficas tem-se de usar a tabela bibproofs

$sqlInsertProof = 
  "INSERT INTO demonstrations
       (teoId,proverId,code,dateSubmission,userId)
        VALUES 
       ('$pTeoId','$pPrvId','$pCode','$pDateSubmission','$pUserId')";


$resultadoInsertProof = mysql_query($sqlInsertProof,$ligacao);


if (!$resultadoInsertProof) {
  echo 'Error - Proof not inserted! (L81)';
  // TRANSAÇÕES - ROLLBACK
  @ mysql_query("ROLLBACK"); 
  echo "<meta http-equiv=\"refresh\" content=\"2; url=../forms.php\" />";
  exit;
}

// Obtêm o valor do demId
$sqlLastInsert = "SELECT LAST_INSERT_ID()";
$resultadoLastInsert = mysql_query($sqlLastInsert,$ligacao);
$linhaLastInsert = mysql_fetch_assoc($resultadoLastInsert);
$pDemId=$linhaLastInsert['LAST_INSERT_ID()'];


// começa por apagar o resultado anterior


$vNameParaApagar     = 'proof'.$pUserId.'.*';
system("rm $vNameParaApagar");


echo "<p>Processing the proof, please wait</p>\n";
flush(); // limpa o buffer de saída para ter a certeza de que a
	 // mensagem anterior é mostrada

// O restante processamento é dependente do provador escolhido

if ($pPrvId==2) { // GCLCprover
  echo "<p>GCLCprover -- Processing, please wait";
  flush(); 
  require('iInsertPrfGeoThmGCLCprover.php');
}
elseif ($pPrvId==3) { // GCLCprover+euk2gclc 
  // ---> tenho de ver isto com mais cuidado
  echo "GCLCprover+euk2gclc -- Processing, please wait";
  flush(); 
  require('iInsertPrfGeoThmGCLCproverEuk.php');
}
elseif ($pPrvId==4) { //Coq+JNarboux (por antecipação)
  echo "Coq+Area Method (by J. Narboux) -- Processing, please wait";
  flush(); 
  require('iInsertPrfGeoThmCoqJN.php');
}

// está tudo bem volta à página dos formulários

echo "<p>Proof inserted</p>";
echo "<meta http-equiv=\"refresh\" content=\"2; url=../forms.php\" />";

?>


<hr/>

<p>&nbsp;</p>

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