--- /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();
+ }
+
+ }
+
+ }
+
+}
projects / logicplayer.git / blobdiff