<?php 
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 Problem</h3>
</center>

<hr/>


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

<?php


// Este ficheiro ainda precisa de um tratamento para ficar mais
// modular, nomeadamente no tratamento das ficguras e das
// demonstrações - ver os ficheiros de inserção das provas feitos já
// um por provador.




// XXX 
// Isto devia implicar um "lock" na tabela referente aos
// teoremas, isto para não haver o perigo de problemas com os
// identificadores de teoremas, por exemplo dois utilizadores que
// requesitam um número com A primeiro que B e depois B introduz o
// teorema primeiro que A
// XXX 

// Vai construir o identificador para um novo teorema
//cria uma pesquisa
$sql = "SELECT max(teoId)
          FROM theorems
      ORDER BY teoId";

$resultado = mysql_query($sql,$ligacao);

$linha = mysql_fetch_assoc($resultado);
$maxTeoId=trim($linha['max(teoId)']);

// retirar a componente númerica do identificador
preg_match("§GEO([0-9]+)§",$maxTeoId,$matches);

// O números máximo para o identificador de "theorems"
$nlinhas = $matches[1];

$nlinhas=$nlinhas+1;

require('formata_num.inc');

// Para colocar o números na forma 00XX, isto é sempre com quatro
// casas decimais e com zeros à esquerda a preencher.
$nlinhas=leading_zero($nlinhas,4);

// Obtêm os valores do formulário.
// A teoId é construída automáticamente GEO+n de linhas da tabela + 1
$pTeoId             = 'GEO'.$nlinhas;
// referentes ao Teorema
$pTeoName           = $_POST['TeoName'];
$pBibRef            = $_POST['Bibref'];
$pCategory          = $_POST['Category'];
$pDescription       = $_POST['Description'];
// Referentes ao Utilizador e gerais
$pDateSubmission   = $_POST['DateSubmission'];
$pUserId           = $_POST['UserId'];
// referentes ao DGS
$pDrwIdNameVersion = $_POST['DrwIdNameVersion'];
$pBibrefDrw        = $_POST['BibrefDrw'];
$pCodeDrw          = $_POST['CodeDrw'];
// referentes ao ATP
$pPrvIdNameVersion = $_POST['PrvIdNameVersion'];
$pBibrefPrv        = $_POST['BibrefPrv'];
$pCodePrv          = $_POST['CodePrv'];


// echo "TeoId            ".$pTeoId            ."<br>";
// echo "TeoName          ".$pTeoName          ."<br>";
// echo "BibRef           ".$pBibRef           ."<br>";
// echo "Category         ".$pCategory         ."<br>";
// echo "Description      ".$pDescription      ."<br>";
// echo "DateSubmission   ".$pDateSubmission   ."<br>";
// echo "UserId           ".$pUserId           ."<br>";
// echo "DrwIdNameVersion ".$pDrwIdNameVersion ."<br>";
// echo "BibrefDrw        ".$pBibrefDrw        ."<br>";
// echo "CodeDrw          ".$pCodeDrw          ."<br>";
// echo "PrvIdNameVersion ".$pPrvIdNameVersion ."<br>";
// echo "BibrefPrv        ".$pBibrefPrv        ."<br>";
// echo "CodePrv          ".$pCodePrv          ."<br>";

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

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

$pDrawerId = $matches[1];

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

$pProverId = $matches[1];

// Formata os valores para posterior inserção na Tabela
if (!get_magic_quotes_gpc())
  { //    $pNumeroIdentificacao = addslashes($pNumeroIdentificacao);
    $pTeoId          = addslashes($pTeoId);
    $pTeoName        = addslashes($pTeoName);
    $pBibRef         = addslashes($pBibRef);
    $pCategory       = addslashes($pCategory);
    $pDescription    = addslashes($pDescription);
    $pDateSubmission = addslashes($pDateSubmission);
    $pUserId         = addslashes($pUserId);
    $pDrawerId       = addslashes($pDrawerId);	 
    $pBibrefDrw      = addslashes($pBibrefDrw);
    $pCodeDrw        = addslashes($pCodeDrw);
    $pProverId       = addslashes($pProverId);
    $pBibrefPrv      = addslashes($pBibrefPrv);
    $pCodePrv        = addslashes($pCodePrv);
  }


// Inserção dos Valores relativos ao enunciado

// Inicio da transacção
@ mysql_query("BEGIN");

// Primeiro a informação sem a ref. bib.
$sqlInsertGeoTheorem = 
     "INSERT INTO theorems
       (teoId,userId,category,description,teoName,dateSubmission)
      VALUES 
       ('$pTeoId','$pUserId','$pCategory','$pDescription','$pTeoName',
        '$pDateSubmission')";

$resultadoInsertGeoTheorem = mysql_query($sqlInsertGeoTheorem,$ligacao);

//Depois a referência bibliográfica (nesta fase só uma)

$sqlInsertGeoTheoremBibRef = 
     "INSERT INTO bibtheorem
       (teoId,bibrefId)
      VALUES 
       ('$pTeoId','$pBibRef')";

$resultadoInsertGeoTheoremBibRef = mysql_query($sqlInsertGeoTheoremBibRef,$ligacao);

if ($resultadoInsertGeoTheorem && $resultadoInsertGeoTheoremBibRef) {
  echo '<h3>New Problem Inserted.</h3>'; 
  echo "<p>Please wait - Processing the Figure and the Proof</p>";
  // Está tudo bem - Termina a transacção.
  @mysql_query("COMMIT");
}
else {
  echo '<p>Error - new problem not inserted in the database</p>';
  // Transações - ROLLBACK
  @ mysql_query("ROLLBACK");
  echo "<meta http-equiv='refresh' content='2; url=../interaction.php' />\n";
  exit;
}
    


// Inserção dos valores relativos à Figura

// Inicio da transacção
@ mysql_query("BEGIN");

$sqlInsertFigure = 
     "INSERT INTO figures
       (teoId,drawerId,code,dateSubmission,userId)
      VALUES 
       ('$pTeoId','$pDrawerId','$pCodeDrw','$pDateSubmission','$pUserId')";


$resultadoInsertFigure = mysql_query($sqlInsertFigure,$ligacao);

// Vai obter o identificador da última figura inserida
$sqlLastInsert = "SELECT LAST_INSERT_ID()";
$resultadoLastInsert = mysql_query($sqlLastInsert,$ligacao);
$linha = mysql_fetch_assoc($resultadoLastInsert);
$pFigureIdLast = $linha['LAST_INSERT_ID()'];

$sqlInsertFigureBibRef = 
     "INSERT INTO bibfigure
       (figureId,bibref)
      VALUES 
       ('$pFigureIdLast','$pBibrefDrw')";


$resultadoInsertFigureBibRef = mysql_query($sqlInsertFigureBibRef,$ligacao);

if (!$resultadoInsertGeoTheorem or !$resultadoInsertGeoTheoremBibRef) {
  echo "<p>Error - new theorem\'s figure not inserted in the database</p>";
  // Transações - ROLLBACK
  @ mysql_query("ROLLBACK");
  echo "<meta http-equiv='refresh' content='2; url=../interaction.php' />\n";
  exit;
}

// Vai criar o ficheiro jpeg com a figura para guardar na base de dados.

// Escreve o ficheiro "txt" referente ao código
// começa por apagar os ficheiros anteriores
// 
// Os nomes dos ficheiros tem apenso o identificador de utilizador
// para desta forma permitir a escrita de ficheiros por mais do que um
// utilizador ao mesmo tempo.


$vNameCode = 'figure'.$pUserId.'.code';
$vNameErr = 'figure'.$pUserId.'.err';
$vNameErrors = 'figure'.$pUserId.'.errors';
$vNamePIC = 'figure'.$pUserId.'.pic';
$vNameTeX = 'figure'.$pUserId.'.tex';
$vNameDVI = 'figure'.$pUserId.'.dvi';
$vNamePS = 'figure'.$pUserId.'.ps';
$vNameEPSI = 'figure'.$pUserId.'.epsi';
$vNameJPG = 'figure'.$pUserId.'.jpg';

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

// Vai processar o código com o programa de desenho
// Consoante o programa de desenho
// 2 - Eukleides - 1.0.2
// 3 - GCLC - 5.00
ob_start();
if ($pDrawerId==2) 
  system("/usr/local/bin/eukleides $vNameCode > $vNamePIC 2> $vNameErr");
elseif ($pDrawerId==3) {
  system("/usr/local/bin/gclc $vNameCode $vNamePIC > $vNameErrors");
  system("grep Syntax $vNameErrors > $vNameErr");
}

ob_end_clean(); 

$filename = $vNameErr;

// Vai verificar se houve erros ou não
if  (file_exists($filename) and filesize($filename)>0) { // há erros 
  $file = fopen ($filename, "r");
  $contents = fread ($file, filesize ($filename));
  echo $contents;
  //system("rm figure.err");
  echo "<center>\n";
  echo "<p>There are errors in the figure's code. The figure was not inserted in the database</p>\n";
  echo "</center>\n";
  echo "<meta http-equiv='refresh' content='2; url=../interaction.php' />\n";
 }
 else { // Caso não haja erros vai processar a figura
   // Vai produzir o texto LaTeX referente à Figura
   ob_start();
   print "\documentclass[11pt]{article}\n";
   if ($pDrawerId==2)
     print "\usepackage{pstricks}\n";
   elseif ($pDrawerId==3) 
     print "\usepackage{gclc}\n";
   print "\pagestyle{empty}\n";
   print "\begin{document}\n";
   print "\input{ $vNamePIC }\n";
   print "\end{document}\n";
   
   $texfile=fopen($vNameTeX,"w");
   fwrite($texfile,ob_get_contents()); 
   fclose($texfile); 
   
   $vNameTeX = 'figure'.$pUserId.'.tex';
   $vNameDVI = 'figure'.$pUserId.'.dvi';
   $vNamePS = 'figure'.$pUserId.'.ps';
   $vNameEPSI = 'figure'.$pUserId.'.epsi';
   $vNameJPG = 'figure'.$pUserId.'.jpg';

   system("latex $vNameTeX"); 
   system("dvips $vNameDVI -o $vNamePS"); 
   system("ps2epsi $vNamePS $vNameEPSI");
   system("convert $vNameEPSI $vNameJPG");
   ob_end_clean();    
   
   // Agora vai produzir os ficheiros XML e SVG  - para já só para o GCLC
   
   $vNameXML = 'figure'.$pUserId.'.xml';
   $vNameXMLaux = 'fig'.$pUserId.'.xml';
   
   $vNameSVG = 'figure'.$pUserId.'.svg';

   ob_start();   
   if ($pDrawerId==2) { // No caso do Eukleides deixa o ficheiro XML em branco 
     system("rm $vNameXML"); 
     system("cat ' ' > $vNameXML"); 
     system("rm $vNameSVG"); 
     system("cat ' ' > $vNameSVG"); 
     // ainda tenho de resolver os problemas com o eps2svg
     //system("eps2svg $vNameEPSI");
    }
   elseif ($pDrawerId==3) {
     // primeiro cria o XML correspondente ao GCLC
     system("/usr/local/bin/gclc $vNameCode $vNameXML -xml");
     // depois faz o "rendering" do XML em linguagem natural
     // modifica o estilo de saída para a Natural Language
     system("sed -e 's/GeoConsHTML.xsl/GeoConsNL.xsl/g' $vNameXML > $vNameXMLaux"); 
     // agora cria o SVG correspondente ao GCLC
     system("/usr/local/bin/gclc $vNameCode $vNameSVG -svg");    
   }
   ob_end_clean(); 
  
  
   // e agora a escrita do ficheiro referente à imagem
   $fpJPG   = fopen($vNameJPG, 'r');
   $contentJPG = fread($fpJPG, filesize($vNameJPG));
   $contentJPG = addslashes($contentJPG);
   fclose($fpJPG);
   
   // e do ficheiro XML
   $fpXML = fopen($vNameXMLaux,'r');
   $contentXML = fread($fpXML,filesize($vNameXMLaux));
   $contentXML = addslashes($contentXML);
   fclose($fpXML);
   
   // e do ficheiro SVG
   $fpSVG = fopen($vNameSVG,'r');
   $contentSVG = fread($fpSVG,filesize($vNameSVG));
   $contentSVG = addslashes($contentSVG);
   fclose($fpSVG);
   
   // e agora a inserção dos três

   $sqlfigure = "UPDATE figures
                    SET codeXML = '$contentXML',
                        figure = '$contentJPG',
                        figureSVG = '$contentSVG'
                  WHERE figureId = $pFigureIdLast";
   
   $resultadofigure = mysql_query($sqlfigure,$ligacao);
   
   if (!$resultadofigure) {
     echo "<p>1-Error - figure not inserted</p>";
     echo "<meta http-equiv='refresh' content='2; url=../interaction.php' />\n";
     exit;
   }
   else { // Está tudo bem
     echo '<h3>New Theorem\'s Figure Inserted.</h3>'; 
     echo "<p>Please wait - Processing the Figure and the Proof</p>";
     // Está tudo bem - Termina a transacção.
     @mysql_query("COMMIT");
   }     
 }   

// Fim - inserção da figura

// A inserção só é feita se o processamento do código se efectuar sem
// problemas.


// Vai criar o ficheiro pdf com a demonstração para guardar na base de
// dados.
// Escreve o ficheiro "txt" referente ao código
// começa por apagar os ficheiros anteriores
// 
// Os nomes dos ficheiros tem apenso o identificador de utilizador
// para desta forma permitir a escrita de ficheiros por mais do que um
// utilizador ao mesmo tempo.


$vNameProofCode = 'proof'.$pUserId.'.code';
$vNameProofCodeXML = 'proofCode'.$pUserId.'.xml';
$vNameProofProof = 'proof'.$pUserId.'_proof.tex';
$vNameProofErr = 'proof'.$pUserId.'.err';
$vNameProofErrors = 'proof'.$pUserId.'.errors';
$vNameProofPIC = 'proof'.$pUserId.'.pic';
$vNameProofTeX = 'proof'.$pUserId.'.tex';
$vNameProofDVI = 'proof'.$pUserId.'.dvi';
$vNameProofPS = 'proof'.$pUserId.'.ps';
$vNameProofPDF = 'proof'.$pUserId.'.pdf';
$vNameProofProofXML = 'proof'.$pUserId.'_proof.xml';
$vNameProofXML = 'proof'.$pUserId.'.xml';
$vNameProofBZ2 = $vNameProofXML.'.bz2';

$vNameProofCodeXMLAux = 'proof'.$pUserId.'.codeaux';
$vNameProofCodeConv = 'proof'.$pUserId.'.codeconv';
$vNameErrorsConv = 'proof'.$pUserId.'.errorsconv';


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

// Vai processar o código com o ATP
// Consoante o programa de desenho
// 2 - GCLC - 1.0 
// 3 - GCLC + euktogclcprover - 1.0.1.0 (os primeiro dois são para o
// gclc os dois últimos para o conversor)
ob_start();
if ($pProverId==2) {
  // aplica o  provador GCLCprover 1.0
  system("/usr/local/bin/gclc $vNameProofCode $vNameProofCodeXML > $vNameProofErrors");
  // verifica se há erros
  system("grep Syntax $vNameProofErrors > $vNameProofErr");
}
elseif ($pProverId==3) {
  // primeiro aplica o conversor euktogclcprover 1.0
  system("/usr/local/bin/euktogclcprover $vNameProofCode > $vNameProofCodeConv 2> $vNameErrorsConv");
  system("cp $vNameProofCodeConv $vNameProofCode");
  // depois aplica o provador GCLCprover 1.0
  system("/usr/local/bin/gclc $vNameProofCode $vNameProofCodeXML > $vNameProofErrors");
  system("grep Syntax $vNameProofErrors > $vNameProofErr");
}
ob_end_clean(); 

// modifica o estilo de saída para a Natural Language
// É o conteúdo do ficheiro modificado que é inserido na BD
system("sed -e 's/GeoConsHTML.xsl/GeoConsNL.xsl/g' $vNameProofCodeXML > $vNameProofCodeXMLAux");


$filename = $vNameProofErr;

// Vai verificar se houve erros ou não
if  (file_exists($filename) and filesize($filename)>0) { // há erros 
  $file = fopen ($filename, "r");
  $contents = fread ($file, filesize ($filename));
  echo $contents;
  //system("rm proof.err");
  echo "<center>\n";
  echo "<p>There are errors in the proof's code. The proof was not inserted in the database</p>\n";
  echo "</center>\n";
  echo "<meta http-equiv='refresh' content='2; url=../interaction.php' />\n";
  exit;
 }
 else { // Caso não haja erros vai processar a prova
// Vai produzir o texto LaTeX referente à Prova
// Pré-processa o ficheiro proof$IdUser_proof.tex gerado pelo gclc 
// pelo sed para substituir o estilo por omissão do gclc pelo estilo
// landscape
   ob_start();
   system("sed -e 's/{gclc_proof}/\[landscape\]{gclcproof}/g' $vNameProofProof > $vNameProofTeX");  

   system("latex $vNameProofTeX"); 
   system("latex $vNameProofTeX"); 
   system("dvips $vNameProofDVI"); 
   system("ps2pdf $vNameProofPS"); 

   ob_end_clean(); 

   // Vai agora criar o ficheiro XML
   echo "<p>Processing the XML file, please wait</p>\n";
   system("/usr/local/bin/gclc  $vNameProofCode $vNameProofCodeXML -xml > $vNameProofErrors");
   
   system("cp $vNameProofProofXML $vNameProofXML");
   // vai conprimir o ficheiro com o bzip2, é necessário apagar o
   // ficheiro comprimido, caso exista.
   system("rm $vNameProofBZ2");
   system("bzip2 $vNameProofXML");

   // trata agora da inclusão dos dados referentes à demonstração, com
   // excepção do ficheiro pdf que ainda tem de ser gerado

   // Inicio da transacção
   @ mysql_query("BEGIN");

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

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

   // Obtêm o valor do demId da última inserção feita
   $sqlLastInsert = "SELECT LAST_INSERT_ID()";
   $resultadoLastInsert = mysql_query($sqlLastInsert,$ligacao);
   $linha = mysql_fetch_assoc($resultadoLastInsert);
   $pProofIdLast = $linha['LAST_INSERT_ID()'];

   $sqlInsertProofBibRef = 
     "INSERT INTO bibproofs
       (demId,bibrefId)
      VALUES 
       ('$pProofIdLast','$pBibrefPrv')";
   

   $resultadoInsertProofBibRef = mysql_query($sqlInsertProofBibRef,$ligacao);

   if ($resultadoInsertProof && $resultadoInsertProofBibRef) {
     echo '<h3>New Theorem\'s Proof Inserted.</h3>'; 
     echo "<p>Please wait - Processing the Proof</p>";
     // Está tudo bem - Termina a transacção.
     @mysql_query("COMMIT");
   }
   else {
     echo '<p>Error - Proof not inserted! - generic data</p>';
     // Transações - ROLLBACK
     @ mysql_query("ROLLBACK");
     echo "<meta http-equiv='refresh' content='2; url=../interaction.php' />\n";
     exit;
   }


   // Agora a inserção do código em formato XML
   $fpCodeXML      = fopen($vNameProofCodeXMLAux, 'r');
   $contentCodeXML = fread($fpCodeXML, filesize($vNameProofCodeXMLAux));
   $contentCodeXML = addslashes($contentCodeXML);
   fclose($fpCodeXML);
      
   // e agora a inserção da prova em formato PDF
   $fpPDF      = fopen($vNameProofPDF, 'r');
   $contentPDF = fread($fpPDF,filesize($vNameProofPDF));
   $contentPDF = addslashes($contentPDF);
   fclose($fpPDF);
   
   // Agora a inserção da prova em formato XML comprimido
   $fpBZ2      = fopen($vNameProofBZ2, 'r');
   $contentBZ2 = fread($fpBZ2, filesize($vNameProofBZ2));
   $contentBZ2 = addslashes($contentBZ2);
   fclose($fpBZ2);

   // Inicio da transacção
   @ mysql_query("BEGIN");

   $sqlproof = "UPDATE demonstrations
                   SET codeXML  = '$contentCodeXML',
                       proof    = '$contentPDF',
                       proofXML = '$contentBZ2'    
                 WHERE demId = $pProofIdLast";
   
   
   $resultadoproof = mysql_query($sqlproof,$ligacao);
   
   if (!$resultadoproof) {
     echo "<p>3-Error - proof not inserted</p>";
     // Transações - ROLLBACK
     @ mysql_query("ROLLBACK");
     echo "<meta http-equiv='refresh' content='2; url=../interaction.php' />\n";
     exit;
   }


   // Fim - inserção da prova
   
   // Preenchimento do campo "status"
   
   // vai obter o resultado da tentativa de prova
   ob_start();
   $vResult=system("./provedDisproved < $vNameProofTeX");
   ob_end_clean();
   //   1 = proved (if the conjecture was proved valid)
   //   0 = disproved (if the conjecture was proved invalid)
   //   2 = Failed to prove the conjecture (if neither of above two)
   if ($vResult==1) 
     $vStatus="Proved";
   elseif ($vResult==0)
     $vStatus="Disproved";
   else
     $vStatus="Failed to prove the conjecture";
   
   $sqlproofstatus = "UPDATE demonstrations
                         SET status = '$vStatus'
                       WHERE demId = $pProofIdLast";
   
   $resultadoproofstatus = mysql_query($sqlproofstatus,$ligacao);
   
   if (!$resultadoproofstatus) {
     echo "<p>4 - Error - proof not inserted</p>";
     // Transações - ROLLBACK
     @ mysql_query("ROLLBACK");
     echo "<meta http-equiv='refresh' content='2; url=../interaction.php' />\n";
     exit;
   }
   
   // E agora os resultados das medidas de eficiência
   
   if ($pProverId==2 || $pProverId==3) {
     // 2 - para o  provador GCLCprover 1.0
     // ou
     // 3 - para o provador GCLCprover 1.0 após o conversor euktogclcprover 1.0
     ob_start();
     $elimSteps=system("./nEliminationSteps < $vNameProofTeX");
     $geoSteps=system("./nGeometricSteps < $vNameProofTeX");
     $algSteps=system("./nAlgebraicSteps < $vNameProofTeX");
     $totalSteps=system("./nTotalSteps < $vNameProofTeX");
     $sTime=system("./sTime < $vNameProofTeX");
     ob_end_clean();
   }
   
   // Vai obter os dados do Computador de serviço 
   // isto é na tabela "computador" estão os dados do meu computador
   // actual, aquele aonde os programas estão a ser executados.
   
   $sqlComputer = "SELECT CPUBrand,CPUType,speed,RAM
                     FROM computer";
   
   $resultadoComputer = mysql_query($sqlComputer,$ligacao);
   $linhaComputer = mysql_fetch_assoc($resultadoComputer);
   
   $pCPUBrand = trim($linhaComputer['CPUBrand']);
   $pCPUType  = trim($linhaComputer['CPUType']);
   $pSpeed    = trim($linhaComputer['speed']);
   $pRAM      = trim($linhaComputer['RAM']);
   
   $computerSpecs = $pCPUBrand." ".$pCPUType.", ".$pSpeed."GHz, ".$pRAM."GB";
   
   $sqlProofMeasures = "INSERT INTO measures
                           (measuresId,elimSteps,geoSteps,algSteps,timeCPU,
                            computerSpecs)
                          VALUES
                           ('$pProofIdLast','$elimSteps','$geoSteps',
                            '$algSteps','$sTime','$computerSpecs')";
   
   
   $resultadoProofMeasures = mysql_query($sqlProofMeasures,$ligacao);
   
   if (!$resultadoProofMeasures) {
     echo "<p>5 - Error - proof not inserted --- measures</p>";
     // Transações - ROLLBACK
     @ mysql_query("ROLLBACK");
     echo "<meta http-equiv='refresh' content='2; url=../interaction.php' />\n";
     exit;
   }
   
   // Se chegou até aqui então pode-se fechar a transacção.
   @mysql_query("COMMIT");   
 }


if ($resultadoInsertProof && $resultadoInsertFigure) {
  echo '<h3>New Figure & Proof Inserted.</h3>'; 
  echo "<meta http-equiv='refresh' content='2; url=listingGeoThms.php' />\n";
 }
 else {
   if ($resultadoInsertFigure)
     echo '<p>New Figure Inserted.</p>'; 
   else {
     echo '<p>6 - Error - Figure not inserted!</p>';
     echo "<meta http-equiv='refresh' content='2; url=../interaction.php' />\n";
     exit;
   }
   if ($resultadoInsertProof)
     echo '<p>New Proof Inserted.</p>'; 
   else {
     echo '<p>7 - Error - Proof not inserted!</p>';
     echo "<meta http-equiv='refresh' content='2; url=../interaction.php' />\n";
     exit;
   }
 }
?>


<hr/>

<p>&nbsp;</p>

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