/***********************************************
* AnyLink Drop Down Menu-  Dynamic Drive (www.dynamicdrive.com)
* This notice MUST stay intact for legal use
* Visit http://www.dynamicdrive.com/ for full source code
***********************************************/

//Contents for menu 1
var menu1=new Array()
menu1[0]='<a href="/misc.php">&nbsp;&nbsp;&nbsp;Miscellaneous</a>'
menu1[1]='<a href="/thanks.php">&nbsp;&nbsp;&nbsp;Thanks</a>'

//Contents for menu 2
var menu2=new Array()
menu2[0]='<a href="/resume.php" target="_blank">&nbsp;&nbsp;&nbsp;Professional Resume</a>'
menu2[1]='<a href="/academic_CV.pdf" target="_blank">&nbsp;&nbsp;&nbsp;Academic CV</a>'
//menu2[1]='<a href="/profile.php">&nbsp;&nbsp;&nbsp;Profile</a>'
menu2[2]='<a href="/development.php">&nbsp;&nbsp;&nbsp;Freelance Developer</a>'

//Contents for menu 3
var menu3=new Array()
menu3[0]='<a href="/code.php">&nbsp;&nbsp;&nbsp;Software/Code</a>'
//menu3[1]='<a href="/semantic_web.php">&nbsp;&nbsp;&nbsp;Semantic Web</a>'
menu3[2]='<a href="/howtos.php">&nbsp;&nbsp;&nbsp;HOWTOs</a>'

//Contents for menu 4
var menu4=new Array()
menu4[0]='<a href="/philosophy.php">&nbsp;&nbsp;&nbsp;Papers</a>'
//menu4[1]='<a href="/theorem_provers.php">&nbsp;&nbsp;&nbsp;Theorem Provers</a>'




var menuwidth='165px' //default menu width
var menubgcolor='#467AA7'  //menu bgcolor
var disappeardelay=250  //menu disappear speed onMouseout (in miliseconds)
var hidemenu_onclick="yes" //hide menu when user clicks within menu?

/////No further editting needed

var ie4=document.all
var ns6=document.getElementById&&!document.all

if (ie4||ns6)
document.write('<div id="dropmenudiv" style="visibility:hidden;width:'+menuwidth+';background-color:'+menubgcolor+'" onMouseover="clearhidemenu()" onMouseout="dynamichide(event)"></div>')

function getposOffset(what, offsettype){
var totaloffset=(offsettype=="left")? what.offsetLeft : what.offsetTop;
var parentEl=what.offsetParent;
while (parentEl!=null){
totaloffset=(offsettype=="left")? totaloffset+parentEl.offsetLeft : totaloffset+parentEl.offsetTop;
parentEl=parentEl.offsetParent;
}
return totaloffset;
}


function showhide(obj, e, visible, hidden, menuwidth){
if (ie4||ns6)
dropmenuobj.style.left=dropmenuobj.style.top="-500px"
if (menuwidth!=""){
dropmenuobj.widthobj=dropmenuobj.style
dropmenuobj.widthobj.width=menuwidth
}
if (e.type=="click" && obj.visibility==hidden || e.type=="mouseover")
obj.visibility=visible
else if (e.type=="click")
obj.visibility=hidden
}

function iecompattest(){
return (document.compatMode && document.compatMode!="BackCompat")? document.documentElement : document.body
}

function clearbrowseredge(obj, whichedge){
var edgeoffset=0
if (whichedge=="rightedge"){
var windowedge=ie4 && !window.opera? iecompattest().scrollLeft+iecompattest().clientWidth-15 : window.pageXOffset+window.innerWidth-15
dropmenuobj.contentmeasure=dropmenuobj.offsetWidth
if (windowedge-dropmenuobj.x < dropmenuobj.contentmeasure)
edgeoffset=dropmenuobj.contentmeasure-obj.offsetWidth
}
else{
var topedge=ie4 && !window.opera? iecompattest().scrollTop : window.pageYOffset
var windowedge=ie4 && !window.opera? iecompattest().scrollTop+iecompattest().clientHeight-15 : window.pageYOffset+window.innerHeight-18
dropmenuobj.contentmeasure=dropmenuobj.offsetHeight
if (windowedge-dropmenuobj.y < dropmenuobj.contentmeasure){ //move up?
edgeoffset=dropmenuobj.contentmeasure+obj.offsetHeight
if ((dropmenuobj.y-topedge)<dropmenuobj.contentmeasure) //up no good either?
edgeoffset=dropmenuobj.y+obj.offsetHeight-topedge
}
}
return edgeoffset
}

function populatemenu(what){
if (ie4||ns6)
dropmenuobj.innerHTML=what.join("")
}


function dropdownmenu(obj, e, menucontents, menuwidth){
if (window.event) event.cancelBubble=true
else if (e.stopPropagation) e.stopPropagation()
clearhidemenu()
dropmenuobj=document.getElementById? document.getElementById("dropmenudiv") : dropmenudiv
populatemenu(menucontents)

if (ie4||ns6){
showhide(dropmenuobj.style, e, "visible", "hidden", menuwidth)
dropmenuobj.x=getposOffset(obj, "left")
dropmenuobj.y=getposOffset(obj, "top")
dropmenuobj.style.left=dropmenuobj.x-clearbrowseredge(obj, "rightedge")+"px"
dropmenuobj.style.top=dropmenuobj.y-clearbrowseredge(obj, "bottomedge")+obj.offsetHeight+"px"
}

return clickreturnvalue()
}

function clickreturnvalue(){
if (ie4||ns6) return false
else return true
}

function contains_ns6(a, b) {
while (b.parentNode)
if ((b = b.parentNode) == a)
return true;
return false;
}

function dynamichide(e){
if (ie4&&!dropmenuobj.contains(e.toElement))
delayhidemenu()
else if (ns6&&e.currentTarget!= e.relatedTarget&& !contains_ns6(e.currentTarget, e.relatedTarget))
delayhidemenu()
}

function hidemenu(e){
if (typeof dropmenuobj!="undefined"){
if (ie4||ns6)
dropmenuobj.style.visibility="hidden"
}
}

function delayhidemenu(){
if (ie4||ns6)
delayhide=setTimeout("hidemenu()",disappeardelay)
}

function clearhidemenu(){
if (typeof delayhide!="undefined")
clearTimeout(delayhide)
}

if (hidemenu_onclick=="yes")
document.onclick=hidemenu























/*****************************************************************************/
//SD - functions I added

function validateInput(frm)
{
   var strQuery;
   var strSignedFormula;
   strQuery = '[';
   var blnInputOK;
   var strErrorMessage = 'One or more input formulas are not well-formed. They have been highlighted yellow.';
   blnInputOK = true;

   for(var i=0;i<frm.length-2;i++)
   {
      if(frm.elements[i].type == 'text')
      {
         sndValidateReq(frm.elements[i].value);
	 alert('');
         if(document.frmProver.areFormulasValid.value == '0')
         {
            frm.elements[i].style.backgroundColor = '#FFFFCC';
            blnInputOK = false;
         }
         else
         {
            frm.elements[i].style.backgroundColor = 'white';
         }
	 document.frmProver.areFormulasValid.value == '1';
      }
   }

   if(blnInputOK)
   {
      for(var i=0;i<frm.length-2;i++)
      {
         if(frm.elements[i].type == 'text')
         {
            if(frm.elements[i].name == 'conclusion')
            {
               strSignedFormula = '('+frm.elements[i].value+',false)';
               strQuery = strQuery + strSignedFormula+']'
            }
            else
            {
               strSignedFormula = '('+frm.elements[i].value+',true)';
               strQuery = strQuery + strSignedFormula+','
            }
         }
      }

      alert(strQuery);
      sndTableauxReq(strQuery);
      return false;

   }
   else
   {
      alert(strErrorMessage);
      return false;
   }
}




function createRequestObject()
{
   var ro;
   var browser = navigator.appName;
   if(browser == "Microsoft Internet Explorer")
   {
      ro = new ActiveXObject("Microsoft.XMLHTTP");
   }
   else
   {
      ro = new XMLHttpRequest();
   }

   return ro;
}




function sndValidateReq(formula)
{
   var http = createRequestObject();
   http.open('get', '/cgi-bin/wff?formula='+formula);
   http.onreadystatechange = function()
   {
      if(http.readyState == 4)
      {
         var response = http.responseText;
         document.frmProver.areFormulasValid.value = response;
      }
   }
   http.send(null);
}




function sndTableauxReq(formulas)
{
   var http = createRequestObject();
   http.open('get', '/cgi-bin/cl_prover?formulas='+formulas);
   http.onreadystatechange = function()
   {
      if(http.readyState == 4)
      {
         var response = http.responseText;
         if (response ==  '1')
         {
            document.frmProver.validityNotification.value = 'This argument is valid';
         }
         else
         {
            document.frmProver.validityNotification.value = 'This argument is invalid';
         }
      }
   }
   http.send(null);
}

/*****************************************************************************/