// js/derUni.js   functions for use in derivations...
window.status=''

function locator() {
if ( navigator.appVersion.indexOf('MSIE 4.')==-1 ) {
   location='#probs'
	}
else document.forms[0].elements[document.forms[0].length - 2].focus()
}

	var elmtFocus // focus point set for
function wrong(type,n,l) {
wrongLine = true
f=n
if (type == 'j') window.status = 'There is a problem with the justification of line ' + n + '.'
var e = document.der.elements[type + n + l]
	elmtFocus=e
     e.value += '???';
     e.focus();
	e.select();
     thm[n]=null
	if ( navigator.appName != "Netscape") {
     e.blur();
     e.focus();
	e.select();
	}
}

function checkDependence(n,l,k)  {
	if (thm[n] != null && thm[n] != '' ) {
     for (var i = n+1; i<k; i++) {
          if ( thm[i] != null && thm[i] != '' && ( between(n,j1[i]) || between(n,j2[i]) || between(n,j3[i]) ) ) {
               document.der.elements['s'+i+level[i]].value += '??'
               thm[i]='?'
          	}
     		}
		}
}

function cl() {
window.status='';  elmtFocus=''
	for ( var i=0; i<derLength+1; i++ ) {
  		level[i] = 1; rule[i] = null; thm[i] = null; subs[i] = null; subT[i] = null; j[i] = null; j1[i] = null; j2[i] = null; j3[i] = null; term[i] = false;CS = null;
		comp = null; comp1 = null; comp2 = null; compOrder = null; compOrder1 = null; compOrder2 = null; cmp1 = null; cmp2 = null;
		}
for (var i=0; i<document.der.elements.length; i++ ) {
	if (document.der.elements[i].name.charAt(0)=='s') document.der.elements[i].value=''
	if (document.der.elements[i].name.charAt(0)=='j') document.der.elements[i].value=''
	}
}

	var currProbNum // begins as the button name; substring yields prob num (3 lines below)
function der(sent, just) {
	cl()
	var mn = (typeof currProbNum == 'string') ? '(' + currProbNum.substring(8) + ') ' : ''
	document.der.h.value= mn + 'Click here for a hint'
	hint = mn + hint
if ((typeof rewriteNoLogicFont == 'function') && document.cookie.indexOf('fontSTARTno')>-1) {
	for ( var i=0; i<just.length; i++ ) {
		document.der.elements["s"+(i+1)+"1"].value = rewriteNoLogicFont(sent[i]);
		if (typeof subD == 'object' ) document.der.elements["s"+(i+1)+"2"].value = rewriteNoLogicFont(subD[i]);
		if (typeof subsubD == 'object' ) document.der.elements["s"+(i+1)+"3"].value = rewriteNoLogicFont(subsubD[i]);
		document.der.elements["j"+(i+1)].value = rewriteNoLogicFontJust(just[i]);
		if ( just[i] == 'Premise' ) {
			thm[i+1] = sent[i]
			rule[i+1] = 'Premise'
			}
		}
	}
else {
	for ( var i=0; i<just.length; i++ ) {
		document.der.elements["s"+(i+1)+"1"].value = sent[i];
		if (typeof subD == 'object' ) document.der.elements["s"+(i+1)+"2"].value = subD[i];
		if (typeof subsubD == 'object' ) document.der.elements["s"+(i+1)+"3"].value = subsubD[i];
		document.der.elements["j"+(i+1)].value = just[i];
		if ( just[i] == 'Premise' ) {
			thm[i+1] = sent[i]
			rule[i+1] = 'Premise'
			}
		}
	}
	document.der.elements["j"+f].focus()
	goal=goalIs()
}

function newProblem(n,name)  {
	y=derLength
	if ( typeof derWidth == 'undefined' ) derWidth = derWidthIs()
	derLength=n-1;
	for ( var i=0; i<derLength+1; i++ ) {
  		level[i] = 1; rule[i] = null; thm[i] = null; subs[i] = null; subT[i] = null; j[i] = null; j1[i] = null; j2[i] = null; j3[i] = null; term[i] = false;CS = null;
		comp = null; comp1 = null; comp2 = null; compOrder = null; compOrder1 = null; compOrder2 = null; cmp1 = null; cmp2 = null;
		}
	derLength=y
	for (i=1;i<=n;i++) {
		term[i]=true
	}
	document.der.elements['j' + n].value='~~~~~~~~~~~~~~~~~~~~~~~~~'
	for ( var i=2; i<=derWidth; i++ ) {
		document.der.elements['s' + n + i].value='~~~~~~~~~~~~~~~~~~~~~~~~~'
	}
	document.der.elements['s' + n + '1'].value='~~~~~ ' + name + ' ~~~~~~~~~~~~~~~'
	document.der.elements['j' + (n+1)].focus()
}

function derWidthIs() {
if (typeof derWidth != 'number' ) {
	derWidth = 1
for ( var i=2; i<6; i++ ) {
   if ( typeof document.der.elements['s' + 1 + i ] != 'undefined' ) {
   	derWidth++
		}
	}
return derWidth
}
}

function check(value,n) {
	if (value == 'new' || value == 'NEW' ) {
		y = prompt("Enter the exercise name.","")
		if (y==null || y == '') y='New Exercise'
		newProblem(n,y)
	}
	else if (value != '~~~~~~~~~~~~~~~~~~~~~~~~~') checkJ(value,n)
}

//writes up the derivation form inputs (not the form tags). Does this differently for netscape and ie.
function writeIt(m,o) { // m the optional addition to the length of derivation s-elements; o is the added number to be added on the first column; derLength and derWidth need to be defined or they take the defaults of 12 and 2
if (typeof derWidth == 'undefined') derWidth = 2
if (typeof derLength == 'undefined') derLength = 12
for ( var i=1; i<derLength+1; i++ ) {
	var lineNum = (i<10)? '&nbsp;' + i : i
	var sze = 16
	var Jsze = 9
	var Isze
	var sze1 = 0 // the length to be added to the first level sentence inputs
	if (navigator.appName == "Netscape" && navigator.appVersion.indexOf("4")>-1) {
		sze = 8; Jsze = 6
	}
	if (typeof m == 'number') sze+=m
	if (typeof o == 'number') sze1 = o
	document.write('<INPUT TYPE="text" NAME="' + 'j' + i + '" size="' + Jsze + '" onChange="check(this.value, ' + i + ')">');
   	document.write('<tt>' + lineNum +'</tt>');
   	for ( var j=1; j<=derWidth; j++ ) {
		Isze = (j==1)? sze + sze1 : sze
   		document.write('<INPUT TYPE="text" NAME="' + 's' + i + j + '" size="' + Isze + '" onChange="checkL(this.value, ' + i + ',' +  j+ ')">');
   		if ( j==derWidth ) document.write('<br>')
		}
	}
   	if (navigator.appName == "Netscape") document.write('<INPUT type="hidden" name = "j' + (derLength +1) + '"> <p>&nbsp;</p><p>&nbsp;</p>')
   	else {
		var BG
		if (window.location.toString().indexOf('/T')>-1 || window.location.toString().indexOf('\\T')>-1) BG = 'url(pix/grid.gif)'
		else if (window.location.toString().indexOf('tour8')>-1) BG = 'url(../pix/grid.gif)'
		else if (window.location.toString().indexOf('/P')>-1 || window.location.toString().indexOf('\\P')>-1) BG = 'url(pix/grid.gif)'
		else BG = 'url(pix/bg6a.gif)'
     	document.write('<DIV id="Layer1" style="position:absolute; width:25px; height:25px; z-index:1; background: ' + BG + '; border: 1px none #010000"><p>&nbsp;</p><p>&nbsp;</p></DIV>');
     	document.write('<INPUT type="text" name="j' + (derLength +1) + '" size="1">')
  		}
}

// same as above except this works for the password protected problems. 
function writeIt2() {
for ( var i=1; i<derLength+1; i++ ) {
	var lineNum = (i<10)? '&nbsp;' + i : i
	var sze = 15
	var Jsze = 9
	if (navigator.appName.charAt(0) == 'N' && navigator.appVersion.indexOf('4')>-1) {
		sze = 10; Jsze = 8
	}
	document.write('<INPUT TYPE="text" NAME="' + 'j' + i + '" size="' + Jsze + '" onChange="cJ(this.value, ' + i + ')">');
	document.write('<tt>' + lineNum +'</tt>');
	document.write('<INPUT TYPE="text" NAME="' + 's' + i + '1" size="' + sze + '" onChange="checkL(this.value, ' + i + ',1)">');
	document.write('<INPUT TYPE="text" NAME="' + 's' + i + '2" size="' + sze + '" onChange="checkL(this.value, ' + i + ',2)">');
	document.write('<INPUT TYPE="text" NAME="' + 's' + i + '3" size="' + sze + '" onChange="checkL(this.value, ' + i + ',3)">');
	document.write('<INPUT TYPE="text" NAME="' + 's' + i + '4" size="' + sze + '" onChange="checkL(this.value, ' + i + ',4)">');
	document.write('<INPUT TYPE="text" NAME="' + 's' + i + '5" size="' + sze + '" onChange="checkL(this.value, ' + i + ',5)"><br>');
}
   if (navigator.appName == "Netscape") document.write('<INPUT type="hidden" name = "j' + (derLength +1) + '"> <p>&nbsp;</p><p>&nbsp;</p>')
   else {
     document.write('<DIV id="Layer1" style="position:absolute; width:200px; height:115px; z-index:1; background-color: ' + document.bgColor + '; border: 1px none #010000"><p>&nbsp;</p><p>&nbsp;</p></DIV>');
     document.write('<INPUT type="text" name="j' + (derLength +1) + '" size="1">')
  }
}
//FOR writeHints: mac's with ie5.0 fail at write hints focus...test for that:
function focX() {
if (navigator.userAgent.indexOf('MSIE 5.0; Mac')==-1) document.der.elements['j'+f].focus()
}

function writeHints() { // to be used to place the textarea in derivations
var wdth =  ( navigator.appName.indexOf('Netscape')>-1 && navigator.appVersion.indexOf('4.')>-1) ? 35 : 60
document.write('<textarea name="h" cols="' + wdth + '" onFocus="this.value=symbolRewrite(hint);focX()" wrap="VIRTUAL" rows="4">HINTS: Click here to get a suggestion.</textarea>')
}

function symbolRewrite(s) {
if ((typeof rewriteNoLogicFont == 'function') && document.cookie.indexOf('fontSTARTno')>-1) s = rewriteNoLogicFont(s)
return s
}

     // we test to see if a line number is within (what may be) a range:
function between(m,range) {
     if (range == null) return false
     else if ( m == range ) return true
		else {
     	var posi = range.indexOf('-')
     		if ( posi > -1 ) {
          var beg = range.substring(0, posi); var en = range.substring(posi + 1)
          if ( m>=beg && m<=en ) return true
          else return false
     		}
     else return false
	}
}

var goal, goalLn=0, goalLine=1
function goalIs() { // set the goal
	if (typeof goal == 'string' && goal.substring(0,2)== '**' ) { // goal a contradiction -- new version?
		goalLn++
		goalLine=goalLn
		return goal.substring(1)
		}
	else if (typeof goal == 'string' && goal.substring(0,2)== '!!' ) {
		goal = goal.substring(1)
		return goal
		}
	else if (typeof goal == 'string' && goal.charAt(0) == '*') { // for goal explicitly set
		goal = goal.substring(1)
		return goal
		}
	else  {
	for (var i=derLength;i>1;i--) { // gets the goal for the current problem from the sent array
		var s = document.der.elements["s"+ i +"1"].value
		if (s.substring(s.length-3)=='???') {
			goalLine = i
			return ((typeof rewriteToLogic == 'function') && document.cookie.indexOf('fontSTARTno')>-1) ? rewriteToLogic(s.substring(0,s.length-3)) : s.substring(0,s.length-3)
			}
		}
	}
}

function setForDer(s) { // s a string of citation/commentary/sentence sequences separated by ';'. Called by derTable().
	if ( s.charAt(0) == ';' ) s=s.substring(1)
	while ( s.charAt(s.length-1) == ' ' ) s=s.substring(0,s.length-2)
	lineArray = s.split(';')
	var cols = 2, rows = 0
loop:
for ( var i=lineArray.length-1; i>=0; i-- ) {
	var curL=lineArray[i]
	for ( var j=0; j<curL.length; j++ ) {
		if ( curL.charAt(j)!='/' ) {
   		rows=i+1
   		break loop
			}
		}
	}
for ( var i=0; i<rows; i++ ) {
	var c = 1
		for ( var j=0; j<lineArray[i].length; j++ ) {
   		if ( lineArray[i].charAt(j)=='/' && lineArray[i].charAt(j+1)!='/' && lineArray[i].charAt(j+1)!='' && lineArray[i].substring(j+1,j+5)!='~~~~' ) c++
			}
	cols=Math.max(cols,c)
	}
	this.cols=cols
	this.rows=rows
for ( var i=0; i<rows; i++ ) {
		var contentArray = lineArray[i].split('/')
   	for ( var j=0; j<cols; j++ ) {
   		if ( contentArray[j] != null && contentArray[j] != '') {
   			var x = (contentArray[j].indexOf('....')==0) ? contentArray[j].substring(0,11) : contentArray[j]
   			if ( x.indexOf('~~~~')==0 ) x=(x.indexOf('~~~~~~')==0) ? '~~~~' : '~' + x.substring(5,15)
   			this.tableSetValue(i,j,x)
   			}
   		else  this.tableSetValue(i,j,'&nbsp;')
			}
	}
}

function derTable(win,s) { // this provides the various derivations to be drawn in any derivation problem; calls table object once for each derivation
	with (win) { // let win be newWindow in calling function -- or whatever is being written to
	var myName = '(Your name goes here IF you set it in the preferences section.)'
	if (typeof getCookie == 'function') {
		var refBG = getCookie('Prefs') //refBG turns out to be a name for preferences in general...
		if (typeof refBG=='string' && refBG.indexOf('idSTART')>-1) {
			var start = refBG.indexOf('idSTART')
			myName = refBG.substring(start+7,refBG.indexOf('idEND'))
			}
		}
	document.writeln(myName + '<br>')
	var exName = s.substring(0,s.indexOf(';'))
	document.writeln('<u>' + exName + '</u><p>')
	document.writeln('<table cellpadding="3" cellspacing="5" border=0>')
	s=s.substring(s.indexOf(';')+1,s.length-1)
	derArray = s.split('|')
for ( var n=0; n<derArray.length; n++ ) { // n is the problem number
	var nn = (typeof currProbNum == 'string') ? probNums.substring(0,probNums.length-1).split('|')[n] : n+1
   document.writeln('<tr><td valign="top">' + nn + '. &nbsp;</td><td>')
   Tabl = new table
	Tabl.setForDer(derArray[n])
   document.writeln('<table border=1>')
   for ( var i=0; i<Tabl.rows; i++ ) { // i is the line number
   	document.write('<tr>')
   	for ( var j=0; j<Tabl.cols; j++ ) { // j is the column number
   		document.write('<td>' + Tabl.data[i*Tabl.cols + j] + '</td>')
   		if (j==0) document.write('<td></td><td>' + (i+1) + '</td><td></td>') // to set off the justification column: j=0
			}
		document.writeln('</tr>')
		}
   document.write('</table></td></tr>')
	}
	document.write('</table>')
}
}

function printAll(s) {
	newWindow = window.open("", "new", "toolbar,menubar,scrollbars,resizable,height=400,width=600")
	newWindow.document.open();
	newWindow.document.write('<html><head><title>Finished Derivations</title><LINK rel="stylesheet" href="highlightTable.css"></head><body>')
	derTable(newWindow,s)
	newWindow.document.write('</body></html>')
	newWindow.document.close();
	newWindow.focus()
}

	var finishedProbs = '', probNums=''
function saveProblem() { // to be used with keepTrack in cookies.js and ...
	if (typeof currProbNum == 'string') probNums+=currProbNum+'|'
	for ( var i=0; i<document.der.elements.length; i++ ) {
   		if ( document.der.elements[i].name.charAt(0) == 's' ) finishedProbs += '/' + document.der.elements[i].value
   		else if ( document.der.elements[i].name.charAt(0) == 'j' ) finishedProbs += ';' + document.der.elements[i].value
		}
	finishedProbs += '|'
}

//a function to check for equivalence
	var equivProof
function checkEquiv(n,th) {
sents = goal.split('!')
var premNum=0
if (sents[2] == th && equivProof.indexOf('1')<0) {
	for (var i=1;i<=n;i++) {
		if (document.der.elements['j' + i].value == 'Premise' && !term[i]) {
			premNum++
			if (premNum>1) {
				msg="You may only have one premise in each \"half\" of the proof of equivalence."
				alert(msg) //
				return false
				}
			var premised=document.der.elements['s' + i + '1' ].value
			}
		}
		if (premised==sents[1]) equivProof+='1'
	}
else if (sents[1] == th && equivProof.indexOf('2')<0) {
	for (var i=1;i<=n;i++) {
		if (document.der.elements['j' + i].value == 'Premise' && !term[i]) {
			premNum++
			if (premNum>1) {
				msg="You may only have one premise in each \"half\" of the proof of equivalence."
				alert(msg)
				return false
				}
			var premised=document.der.elements['s' + i + '1' ].value
			}
		if (premised==sents[2]) equivProof+='2'
		}
	}
if (equivProof.indexOf('1')>-1 && equivProof.indexOf('2')>-1) keepTrack(n)
}

//a function to check for contradictions. (Goal = '*'. Remember: set goal to '**' so that goalIs drops the first '*'.
function checkContra(l,th,n) { // l = line number!, n = id to keepTrack! misnomers...
var stop = true; var thmE = th // stop is a misnomer, stops and keep's track only if this is set to false
var c = (typeof mainConn == 'function') ? mainConn(thmE) : mainLO(thmE)
var cc = c // unchanging thru loop below
var negEP = ( !out(thmE) && c != null && c != '~' && c!='%' && c!='^') ? '~(' + thmE + ')' : '~' + thmE ; // negated th
var negEB = ( !out(thmE) && c != null && c != '~' && c!='%' && c!='^') ? '~[' + thmE + ']' : '~' + thmE ; // negated th (with brackets)
for ( var i=1; i<l; i++ ) {
						if (level[i]!=1) continue
	 	 if ( thm[i] == negEP || thm[i] == negEB ) {
   	  stop = false; break;}
		 else if ( cc == '~') {
	 	  var t = thm[i]; var c = (typeof mainConn == 'function') ? mainConn(t) : mainLO(t); // check to see if the negation comes first
	 	  var tNP = ( !out(t) && c != null && c != '~'  && c!='%' && c!='^')? '~(' + t + ')' : '~' + t;
	 	  var tNB = ( !out(t) && c != null && c != '~'  && c!='%' && c!='^')? '~[' + t + ']' : '~' + t;
	 	  if ( thmE == tNP || thmE == tNB ) {
	 	   stop = false; break; }
			}
		  }
if ( !stop ) keepTrack(n)
}

// These functions include the table object and allow one to write up derivations as tables.

function table() { // generic table object  old: table(rows,cols,border)
	this.rows = 1 // rows
	this.cols = 1 // cols
	this.border = 1 // border
	this.data = new Array // (rows*cols)
	this.tableSetValue = table_setValue
	this.setForDer = setForDer
}

function table_setValue(row,col,value) { // there needs to be row 0 and col 0
	this.data[row*this.cols+col]=value
}

	var msgWindowX=window.open("","alertXWindow","resizable,width=250,height=260")
	msgWindowX.blur()
function alertX(text) {
if (msgWindowX.closed) {
	msgWindowX=window.open("","alertXWindow","resizable,width=250,height=260")
	msgWindowX.blur()
	}
msgWindowX.document.open()
msgWindowX.document.write("<html><HEAD><TITLE>Message window</TITLE><style type='text/css'><!--a {  text-decoration: none} .variable {  font-style: italic; font-weight: bold; color: #FF6600}--></style>")
msgWindowX.document.writeln("</HEAD><body onLoad=\"opener.navKeypress()\" onkeydown=\"opener.setFocus()\">")
msgWindowX.document.writeln("<font face='Logic'><a href='#' onmouseover=\"opener.setFocus()\">" + text  + "</a>")
msgWindowX.document.writeln("<p><small>(Press any key to continue.)</small></font>")
msgWindowX.document.write("</body></html>")
msgWindowX.document.close()
setTimeout('msgWindowX.focus()',1)
}

function setFocus() {
	self.focus()
	if ( typeof elmtFocus == "object" ) elmtFocus.focus()
	else document.der.elements['j'+f].focus()
}

function unLoader() {
	msgWindowX.close()
	window.status=''
}

function navKeypress() {
if (navigator.appName.indexOf('Nets')>-1) {
	msgWindowX.document.captureEvents(Event.KEYPRESS)
	msgWindowX.document.onkeypress = setFocus
	}
}

function isSame(x,y) { //two strings may differ only wrt parentheses and brackets...returns boolean
if (x==y) return true
if (x.length != y.length) return false
for (var i=0; i<x.length; i++) {
	var charX = x.charAt(i),charY = y.charAt(i)
	if (charX == charY) continue
	if ((charX=='(' || charX=='[')&&(charY=='(' || charY=='[')) continue
	if ((charX==')' || charX==']')&&(charY==')' || charY==']')) continue
	return false
	}
return true
}