+++ /dev/null
-package com.example.furt.myapplication;
-
-import android.graphics.Color;
-import android.util.TypedValue;
-import android.view.Gravity;
-import android.view.View;
-import android.view.ViewGroup;
-import android.view.ViewTreeObserver;
-import android.widget.RelativeLayout;
-import android.widget.TextView;
-
-import java.util.ArrayList;
-import java.util.List;
-
-
-public class Node implements Tree {
-
- static int FIELD_UNSET = -1;
- static int OPEN=0;
- static int FAKE=1;
- static int CLOSED=2;
- static int FAKE_CLOSED=3;
- static int CANCELED=4;
- static int FAKE_CANCELED=5;
-
- Formula F; //formula legata al nodo
- String ruleName; //nome della regola associata a questo nodo
- List<Node> Children = new ArrayList<Node>(); //Nodi figli
- 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; //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;
- view = null;
- handler = null;
- ruleName="";
- Father = null;
- status=OPEN;
- hasFocus = false;
- leftOffset = 0;
- rightOffset = 0;
- baseLine = getBaseWidth();
- maxWidth = baseLine;
- }
-
- /**************SetView**************+*****/
- /*****************************************/
- /*******Setta la TextView del node ******/
- /** e il layout in cui deve comparire ***/
- /*****************************************/
-
- public void setView(BorderedTextView t,RelativeLayout r) {
- view = t;
- ruleView =new TextView(t.getContext());
- global=r;
- }
-
-
- /**************Count****************+*****/
- /*****************************************/
- /*******Restituisce il numero di ******/
- /*************nodi dell'albero ***********/
- /*****************************************/
-
- int count()
- {
- int ris=1;
- for (Node n:Children)
- 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())) { //ipotesi già presente: passo alla prossima
- continue loop;
- }
- }
- NodeHP.add(new Hypothesis(newHp, deleted));
- }
- }
-
- public void addHPList(List<Hypothesis>List) {
- loop:for (Hypothesis newHp:List) {
- for (Hypothesis oldHp: NodeHP) {
- if (oldHp.HP.toString().equals(newHp.HP.toString())) { //ipotesi già presente: passo alla prossima
- continue loop;
- }
- }
- Hypothesis copyHP=new Hypothesis(newHp.HP, newHp.isDeleted);
- copyHP.fromNode=newHp.fromNode;
- NodeHP.add(copyHP);
- }
- }
-
- /*****************************************/
- /******* 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
- {
- if (status!=OPEN && status!=FAKE) //nodo chiuso: il focus non può essere su di me
- return false;
- hasFocus=true; //posso assumere il focus
- if (handler!=null)
- handler.onClick(view);
- return true;
- }
- //passo induttivo: vado su tutti i miei figli, poi su mio padre. Termino se il padre è null.
- for (Node n:Children) {
- if (caller != null)
- if (n == caller) //per ogni figlio diverso dal chiamante
- {
- continue;
- }
- if(n.searchFocus(null))
- return true;
- }
- if (caller==null) //ero stato chiamato da mio padre: è inutile richiamarlo
- return false;
- else if (Father==null)
- return false; //padre null: l'albero è dimostrato e non ci sono nodi a cui dare il focus.
- else
- return Father.searchFocus(this); //propaga il searchFocus sul padre
- }
- public void addChild(Node N) {
- 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;
- rightOffset=FIELD_UNSET;
- while (tmp!=null)
- {
- tmp.baseLine=FIELD_UNSET;
- tmp.leftOffset=FIELD_UNSET;
- tmp.rightOffset=FIELD_UNSET;
- tmp.maxWidth=FIELD_UNSET;
- tmp=tmp.Father;
- }
- }
-
- public float getBaseWidth() {
- return F.size();
- }
-
- public float getMaxWidth() //ritorna la larghezza massima del sottoalbero
- {
- if (maxWidth!=FIELD_UNSET)
- return maxWidth;
- else
- maxWidth=getLeftOffset()+getBaseWidth()+getRightOffset();
- return (maxWidth);
- }
-
- public float getLineWidth()
- {
- if (baseLine!=FIELD_UNSET)
- return baseLine;
- else
- {
- baseLine=Math.max(getUpLine(),getBaseWidth()); //la baseline è il massimo valore tra la upLine e la baseWidth
- return baseLine;
- }
- }
- 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)
- return(getBaseWidth());
- int res=0;
- for(Node n:Children)
- res+=(n.getMaxWidth())+spaceSize;
- res-=spaceSize;
- 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;
- }
- else {
- if (Children.size() == 0) //foglia
- leftOffset=0;
- else
- leftOffset=Math.max(Children.get(0).getLeftOffset() + ((getUpLine() - getBaseWidth()) / 2),0);
- return leftOffset;
- }
- }
-
- public float getRightOffset()
- {
- if (rightOffset!=FIELD_UNSET)
- return rightOffset;
- else {
- if (Children.size() == 0) //foglia
- rightOffset=0;
- else
- rightOffset=Math.max(Children.get(Children.size() - 1).getRightOffset() + ((getUpLine() - getBaseWidth()) / 2),0);
- return rightOffset;
- }
- }
-
- 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;
- rightOffset=FIELD_UNSET;
- maxWidth=FIELD_UNSET;
- for(Node n:Children)
- n.Refactor();
- }
-
-
- public void Clean() //metodo di supporto: rimuove dal layout legato al Node tutte le view presenti
- {
- global.removeAllViews();
- }
-
- 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;
- else for (Node n:Children)
- if (!n.isCorrect())
- return false;
- return true;
-
- }
-
- public void Draw()
- {
- float interval=0; //intervallo di spazio da sommare nella creazione dei figli
- 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))) { //focus inapplicabile nell'albero: dimostrazione completata.
- DrawActivity.finishedTree(view.getContext());
- return;
- }
- hasFocus = false;
- }
- if (status==CANCELED || status==FAKE_CANCELED) { //nodo cancellato
- view.setWidth((int) F.sizeDeleted());
- 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;
- }
- if (hasFocus && DrawActivity.selectedNode!=this)
- handler.onClick(view);
- else if (hasFocus) //hasFocus: must be colored red anyway
- view.setTextColor(Color.RED);
- return;
- }
-
- 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());
- 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
-
- 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); //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); //leftPos è il margine sinistro del figlio
- childView.setLeft(Math.round(leftPos));
- }
- else {
- 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);
- childView.setId(DrawActivity.globalId++);
- childView.setText(newChild.F.toString());
- childView.setTextSize(TypedValue.COMPLEX_UNIT_PX, DrawActivity.textSize);
- childView.setGravity(Gravity.CENTER); //formula al centro della sua overline
- childView.setWidth(Math.round(newChild.getLineWidth()));
- global.addView(childView);
- childView.getViewTreeObserver().addOnGlobalLayoutListener(new ViewTreeObserver.OnGlobalLayoutListener() {
- @Override
- public void onGlobalLayout() {
- 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();
- }
-
- }
-
- }
-
-}