List<Hypothesis> NodeHP = new ArrayList<Hypothesis>(); //ipotesi associate
Node Father; //puntatore al padre
View.OnClickListener handler; //touchHandler per far comparire il pop-up delle regole
+ View.OnLongClickListener longHandler; //touchHandler per far comparire il menu con tutte le regole
boolean hasFocus; //indica se questo nodo è quello selezionato
int status; //stato del nodo (chiuso, aperto,fake...)
RelativeLayout global; //layout in cui si trova l'albero
BorderedTextView view; //view contenente questo oggetto
TextView ruleView; //view contenente l'intestazione della regola
- float baseLine;
- float leftOffset;
- float rightOffset;
- float maxWidth;
+ float baseLine; //baseLine del Node: corrisponde alla lunghezza dell'overline
+ float leftOffset; //leftOffset: corrisponde alla larghezza della porzione di albero a sinistra del nodo
+ float rightOffset; //rightOffset: porzione di albero a destra del nodo
+ float maxWidth; //larghezza del sottoalbero di questo nodo (comprensiva del nodo stesso)
Node(Formula F) {
this.F = F;
ris+=n.count();
return ris;
}
+ /**************addHP****************+*****/
+ /*****************************************/
+ /*******Metodi per aggiungere ipotesi*****/
+ /*******sotto forma di Hypothesis o di****/
+ /*************Formula*********************/
+ /*****************************************/
public void addHPFormula(List<Formula>List,boolean deleted) {
loop:for (Formula newHp:List) {
for (Hypothesis oldHp: NodeHP) {
- if (oldHp.HP.toString().equals(newHp.toString())) {
+ if (oldHp.HP.toString().equals(newHp.toString())) { //ipotesi già presente: passo alla prossima
continue loop;
}
}
public void addHPList(List<Hypothesis>List) {
loop:for (Hypothesis newHp:List) {
for (Hypothesis oldHp: NodeHP) {
- if (oldHp.HP.toString().equals(newHp.HP.toString())) {
+ if (oldHp.HP.toString().equals(newHp.HP.toString())) { //ipotesi già presente: passo alla prossima
continue loop;
}
}
}
}
+ /*****************************************/
+ /******* Algoritmo di ricerca del ********/
+ /******* focus: restituisce false ********/
+ /******* se la dimostrazione è completa***/
+
public boolean searchFocus(Node caller)
{
if (Children.size()==0) //caso base: controllo se il focus può essere su di me
N.Father = this;
Children.add(N);
Node tmp=Father;
+ //c'è un nuovo nodo nell'albero: tutti i campi dell'algoritmo di disegno sono da ricalcolare per questo ramo
baseLine=FIELD_UNSET;
maxWidth=FIELD_UNSET;
leftOffset=FIELD_UNSET;
return baseLine;
else
{
- float spaceSize = DrawActivity.spaceSize;
- if (Children.size() == 0)
- return (getBaseWidth());
- int res = 0;
- for (Node n:Children)
- res += (n.getMaxWidth()) + spaceSize;
- res -= spaceSize;
- res -= Children.get(0).getLeftOffset();
- res -= Children.get(Children.size() - 1).getRightOffset();
- baseLine=Math.max(res,getBaseWidth());
+ baseLine=Math.max(getUpLine(),getBaseWidth()); //la baseline è il massimo valore tra la upLine e la baseWidth
return baseLine;
}
}
- public float getUpLine()
+ public float getUpLine() //calcola la upLine, ovvero la dimensione prevista del sottoalbero assumendo il nodo attuale di lunghezza unitaria
{
float spaceSize= DrawActivity.spaceSize;
if (Children.size()==0)
for(Node n:Children)
res+=(n.getMaxWidth())+spaceSize;
res-=spaceSize;
- res-=Children.get(0).getLeftOffset();
- res-=Children.get(Children.size()-1).getRightOffset();
+ res-=Children.get(0).getLeftOffset(); //la linea deve fermarsi all'inizio della formula del primo figlio sinistro
+ res-=Children.get(Children.size()-1).getRightOffset(); //la linea deve finire alla fine della formula dell'ultimo figlio destro
return res;
}
+
+ /**Calcolo del leftOffset
+ * esso è uguale al leftOffset del primo figlio, a cui aggiungere la porzione di overline a sinistra della formula del nodo
+ * o rimuovere la mezza differenza tra la baseWidth e la upLine. Se il leftOffset risulterebbe negativo, diventa nullo.
+ */
+
public float getLeftOffset() {
if (leftOffset != FIELD_UNSET) {
return leftOffset;
}
}
- public float getMaxHeight()
- {
- float baseRes=F.height();
- float res=baseRes;
- for (Node n:Children)
- {
- float tempH=n.getMaxHeight()+baseRes;
- if(tempH>res)
- res=tempH;
- }
- return res;
- }
public float getRightOffset()
{
if (rightOffset!=FIELD_UNSET)
return rightOffset;
}
}
- void Refactor()
+
+ public float getMaxHeight() //calcolo dell'altezza massima dell'albero attuale.
+ {
+ float baseRes=F.height();
+ float res=baseRes;
+ for (Node n:Children)
+ {
+ float tempH=n.getMaxHeight()+baseRes;
+ if(tempH>res)
+ res=tempH;
+ }
+ return res;
+ }
+
+ void Refactor() //metodo di supporto: svuota i campi dell'intero sottoalbero che verranno ricalcolati dall'algoritmo alla prossima applicazione
{
baseLine=FIELD_UNSET;
leftOffset=FIELD_UNSET;
n.Refactor();
}
- void Resize()
- {
- int i;
- float interval=0; //intervallo di spazio da sommare nella creazione dei figli
- float spaceSize= DrawActivity.spaceSize;
- int childNo=Children.size();
- if (childNo!=0)
- {
-
- ruleView.setText(ruleName);
- ruleView.setTextSize(TypedValue.COMPLEX_UNIT_PX, DrawActivity.textSize / 2);
- RelativeLayout.LayoutParams intlp=new RelativeLayout.LayoutParams(ViewGroup.LayoutParams.WRAP_CONTENT, ViewGroup.LayoutParams.WRAP_CONTENT);
- intlp.addRule(RelativeLayout.RIGHT_OF,view.getId());
- int sum=0;
- sum+=F.height();
- Node tmp=Father;
- while (tmp!=null)
- {
- sum+=tmp.F.height();
- tmp=tmp.Father;
- }
- intlp.setMargins(0,0,0,sum);
- intlp.addRule(RelativeLayout.ALIGN_PARENT_BOTTOM);
- ruleView.setLayoutParams(intlp);
- }
- for (i=0;i<childNo;i++) {
- Node newChild=Children.get(i);
- RelativeLayout.LayoutParams lp=new RelativeLayout.LayoutParams(ViewGroup.LayoutParams.WRAP_CONTENT, ViewGroup.LayoutParams.WRAP_CONTENT);
- TextView childView=Children.get(i).view;
- lp.addRule(RelativeLayout.ABOVE,view.getId());
- if (i==0) //first child
- {
- float leftPos= view.getLeft()-Math.max((newChild.getLineWidth()-newChild.getBaseWidth())/2,0);
- if (getLineWidth()>getUpLine())
- leftPos+=((getLineWidth()-getUpLine())/2);
- lp.setMargins(Math.round(leftPos), 0, 0, 0);
- childView.setLeft(Math.round(leftPos));
- }
- else {
- lp.setMargins(Math.round(view.getLeft() + interval), 0, 0, 0);
- childView.setLeft(Math.round(view.getLeft() + interval));
- }
- childView.setLayoutParams(lp);
- childView.setTextSize(TypedValue.COMPLEX_UNIT_PX, DrawActivity.textSize);
-
- if(newChild.status==CANCELED || newChild.status==FAKE_CANCELED)
- childView.setWidth((int) ((newChild.F.sizeDeleted())));
- else
- childView.setWidth(Math.round(newChild.getLineWidth()));
-
- newChild.Resize();
- if (i!=childNo-1) //l'ultimo figlio non ha intervalli
- {
- float leftOverflow=(Children.get(i+1).getLineWidth()-Children.get(i+1).getBaseWidth())/2;
- interval += (newChild.getBaseWidth()+newChild.getRightOffset()+Children.get(i+1).getLeftOffset()-(leftOverflow));
- interval+=spaceSize;
- if (i!=0) //devo sommare anche il leftOverflow del nuovo figlio
- interval+=newChild.getLeftOffset();
- }
-
- }
-
- }
-
- public int treeHeight()
+ public void Clean() //metodo di supporto: rimuove dal layout legato al Node tutte le view presenti
{
- int res=0,tmp;
- for (Node n:Children)
- {
- tmp=n.treeHeight();
- if (tmp>res)
- res=tmp;
- }
- return res+1;
+ global.removeAllViews();
}
- public boolean isCorrect()
+
+ public boolean isCorrect() //controlla per l'intero sottoalbero se esso è privo di nodi fake.
{
if (status==FAKE || status==FAKE_CANCELED || status==FAKE_CLOSED)
return false;
return true;
}
- public void Clean()
- {
- global.removeAllViews();
- }
public void Draw()
{
- int i;
float interval=0; //intervallo di spazio da sommare nella creazione dei figli
- float spaceSize= DrawActivity.spaceSize;
- int childNo=Children.size();
+ float spaceSize= DrawActivity.spaceSize; //dimensione della spaziatura tra i sottoalberi
+ int childNo=Children.size(); //numero di figli del nodo attuale
if (childNo==0) //foglia: possibile ramo dimostrato
+
{
view.setBorders(null); //le foglie non hanno overline
if (status!=OPEN && status!=FAKE) { //nodo chiuso
view.setTextColor(Color.GRAY);
if (hasFocus) //avevo il focus: provo a darlo ad uno dei miei fratelli
{
- if (!(Father.searchFocus(this))) {
+ if (!(Father.searchFocus(this))) { //focus inapplicabile nell'albero: dimostrazione completata.
DrawActivity.finishedTree(view.getContext());
return;
}
}
if (status==CANCELED || status==FAKE_CANCELED) { //nodo cancellato
view.setWidth((int) F.sizeDeleted());
- view.setText("[" + view.getText() + "]");
+ view.setText(F.toStringDeleted());
view.setOnClickListener(null); //rimuove eventuali listener per evitare il proseguimento dell'albero
+ /**NOTA: è possibile permettere all'utente di proseguire la dimostrazione
+ * di un ramo chiuso commentando la riga precedente e aggiungendo nel touchnodeHandler
+ * un'controllo che, in caso di nodo chiuso cliccato, lo riapre e gli riaffida il focus.
+ */
}
return;
}
ruleView.setTextSize(TypedValue.COMPLEX_UNIT_PX, DrawActivity.textSize / 2);
RelativeLayout.LayoutParams intlp=new RelativeLayout.LayoutParams(ViewGroup.LayoutParams.WRAP_CONTENT, ViewGroup.LayoutParams.WRAP_CONTENT);
intlp.addRule(RelativeLayout.RIGHT_OF,view.getId());
- int sum=0;
- sum+=F.height();
- Node tmp=Father;
- while (tmp!=null)
- {
- sum+=tmp.F.height();
- tmp=tmp.Father;
- }
- intlp.setMargins(0,0,0,sum);
- intlp.addRule(RelativeLayout.ALIGN_PARENT_BOTTOM);
+ intlp.addRule(RelativeLayout.ABOVE,view.getId());
ruleView.setLayoutParams(intlp);
global.addView(ruleView);
- /////////////////
-
+ hasFocus=false; //se sono arrivato a questo punto il nodo non è una foglia e non può avere il focus di default
- hasFocus=false;
- for (i=0;i<childNo;i++) {
- final Node newChild=Children.get(i);
+ for (int i=0;i<childNo;i++) {
+ final Node newChild=Children.get(i); //recupero l'i-esimo figlio
RelativeLayout.LayoutParams lp=new RelativeLayout.LayoutParams(ViewGroup.LayoutParams.WRAP_CONTENT, ViewGroup.LayoutParams.WRAP_CONTENT);
final BorderedTextView childView=new BorderedTextView(view.getContext());
childView.setBorders(DrawActivity.b);
lp.addRule(RelativeLayout.ABOVE, view.getId());
if (i==0) //first child
{
- float leftPos= view.getLeft()-Math.max((newChild.getLineWidth()-newChild.getBaseWidth())/2,0);
- if (getLineWidth()>getUpLine())
+ float leftPos= view.getLeft()-Math.max((newChild.getLineWidth()-newChild.getBaseWidth())/2,0); //il primo figlio è posizionato a sinistra del padre, con un ulteriore offset
+ // sinistro pari allo scarto della sua overline
+ if (getLineWidth()>getUpLine()) //sono più grande dell'overline prevista: aggiungo un ulteriore offset al figlio
leftPos+=((getLineWidth()-getUpLine())/2);
-
- lp.setMargins(Math.round(leftPos), 0, 0, 0);
+ lp.setMargins(Math.round(leftPos), 0, 0, 0); //leftPos è il margine sinistro del figlio
childView.setLeft(Math.round(leftPos));
}
else {
- lp.setMargins(Math.round(view.getLeft() + interval), 0, 0, 0);
+ lp.setMargins(Math.round(view.getLeft() + interval), 0, 0, 0); //figlio intermedio: basta aggiungere l'interval alla posizione sinistra del padre
childView.setLeft(Math.round(view.getLeft() + interval));
}
childView.setLayoutParams(lp);
newChild.setView(childView,global);
if(newChild.handler==null)
newChild.handler=new touchnodeHandler(newChild);
+ newChild.longHandler=new longnodeHandler(newChild);
newChild.view.setOnClickListener(newChild.handler);
+ newChild.view.setOnLongClickListener(newChild.longHandler);
childView.getViewTreeObserver().removeOnGlobalLayoutListener(this);
newChild.Draw();
}
if (i!=childNo-1) //l'ultimo figlio non ha intervalli
{
float leftOverflow=Math.max((Children.get(i+1).getLineWidth()-Children.get(i+1).getBaseWidth())/2,0);
+ interval += (newChild.getBaseWidth()+newChild.getRightOffset()+Children.get(i+1).getLeftOffset()-(leftOverflow)); //devo aggiungere all'interval la basewidth del figlio attuale, il rightoffset del figlio attuale e il leftOffset del figlio successivo.
+ interval+=spaceSize;
+ if (i!=0) //devo sommare anche il leftOverflow del nuovo figlio
+ interval+=newChild.getLeftOffset();
+ }
+ }
+ }
+ void Resize() //metodo per ridisegnare l'albero dopo un pinch zoom: l'algoritmo applicato è uguale a quello del metodo Draw()
+ {
+ int i;
+ float interval=0; //intervallo di spazio da sommare nella creazione dei figli
+ float spaceSize= DrawActivity.spaceSize;
+ int childNo=Children.size();
+ if (childNo!=0)
+ {
+
+ ruleView.setText(ruleName);
+ ruleView.setTextSize(TypedValue.COMPLEX_UNIT_PX, DrawActivity.textSize / 2);
+ RelativeLayout.LayoutParams intlp=new RelativeLayout.LayoutParams(ViewGroup.LayoutParams.WRAP_CONTENT, ViewGroup.LayoutParams.WRAP_CONTENT);
+ intlp.addRule(RelativeLayout.RIGHT_OF,view.getId());
+ int sum=0;
+ sum+=F.height();
+ Node tmp=Father;
+ while (tmp!=null)
+ {
+ sum+=tmp.F.height();
+ tmp=tmp.Father;
+ }
+ intlp.setMargins(0,0,0,sum);
+ intlp.addRule(RelativeLayout.ALIGN_PARENT_BOTTOM);
+ ruleView.setLayoutParams(intlp);
+ }
+ for (i=0;i<childNo;i++) {
+ Node newChild=Children.get(i);
+ RelativeLayout.LayoutParams lp=new RelativeLayout.LayoutParams(ViewGroup.LayoutParams.WRAP_CONTENT, ViewGroup.LayoutParams.WRAP_CONTENT);
+ TextView childView=Children.get(i).view;
+ lp.addRule(RelativeLayout.ABOVE,view.getId());
+ if (i==0) //first child
+ {
+ float leftPos= view.getLeft()-Math.max((newChild.getLineWidth()-newChild.getBaseWidth())/2,0);
+ if (getLineWidth()>getUpLine())
+ leftPos+=((getLineWidth()-getUpLine())/2);
+ lp.setMargins(Math.round(leftPos), 0, 0, 0);
+ childView.setLeft(Math.round(leftPos));
+ }
+ else {
+ lp.setMargins(Math.round(view.getLeft() + interval), 0, 0, 0);
+ childView.setLeft(Math.round(view.getLeft() + interval));
+ }
+ childView.setLayoutParams(lp);
+ childView.setTextSize(TypedValue.COMPLEX_UNIT_PX, DrawActivity.textSize);
+
+ if(newChild.status==CANCELED || newChild.status==FAKE_CANCELED)
+ childView.setWidth((int) ((newChild.F.sizeDeleted())));
+ else
+ childView.setWidth(Math.round(newChild.getLineWidth()));
+
+ newChild.Resize();
+
+ if (i!=childNo-1) //l'ultimo figlio non ha intervalli
+ {
+ float leftOverflow=(Children.get(i+1).getLineWidth()-Children.get(i+1).getBaseWidth())/2;
interval += (newChild.getBaseWidth()+newChild.getRightOffset()+Children.get(i+1).getLeftOffset()-(leftOverflow));
interval+=spaceSize;
if (i!=0) //devo sommare anche il leftOverflow del nuovo figlio
interval+=newChild.getLeftOffset();
}
+
}
+
}
-}
\ No newline at end of file
+}
projects / logicplayer.git / blobdiff