mainActivity/src/com/example/furt/myapplication/Node.java

   1 package com.example.furt.myapplication;
   2
   3 import android.graphics.Color;
   4 import android.util.TypedValue;
   5 import android.view.Gravity;
   6 import android.view.View;
   7 import android.view.ViewGroup;
   8 import android.view.ViewTreeObserver;
   9 import android.widget.RelativeLayout;
  10 import android.widget.TextView;
  11
  12 import java.util.ArrayList;
  13 import java.util.List;
  14
  15
  16 public class Node implements Tree {
  17
  18     static int FIELD_UNSET = -1;
  19     static int OPEN=0;
  20     static int FAKE=1;
  21     static int CLOSED=2;
  22     static int FAKE_CLOSED=3;
  23     static int CANCELED=4;
  24     static int FAKE_CANCELED=5;
  25
  26     Formula F; //formula legata al nodo
  27     String ruleName; //nome della regola associata a questo nodo
  28     List<Node> Children = new ArrayList<Node>(); //Nodi figli
  29     List<Hypothesis> NodeHP = new ArrayList<Hypothesis>(); //ipotesi associate
  30     Node Father; //puntatore al padre
  31     View.OnClickListener handler; //touchHandler per far comparire il pop-up delle regole
  32     boolean hasFocus; //indica se questo nodo è quello selezionato
  33     int status; //stato del nodo (chiuso, aperto,fake...)
  34     RelativeLayout global; //layout in cui si trova l'albero
  35     BorderedTextView view; //view contenente questo oggetto
  36     TextView ruleView; //view contenente l'intestazione della regola
  37
  38     float baseLine;
  39     float leftOffset;
  40     float rightOffset;
  41     float maxWidth;
  42
  43     Node(Formula F) {
  44         this.F = F;
  45         view = null;
  46         handler = null;
  47         ruleName="";
  48         Father = null;
  49         status=OPEN;
  50         hasFocus = false;
  51         leftOffset = 0;
  52         rightOffset = 0;
  53         baseLine = getBaseWidth();
  54         maxWidth = baseLine;
  55     }
  56
  57     /**************SetView**************+*****/
  58     /*****************************************/
  59     /*******Setta la TextView del node  ******/
  60     /** e il layout in cui deve comparire  ***/
  61     /*****************************************/
  62
  63     public void setView(BorderedTextView t,RelativeLayout r) {
  64         view = t;
  65         ruleView =new TextView(t.getContext());
  66         global=r;
  67     }
  68
  69
  70     /**************Count****************+*****/
  71     /*****************************************/
  72     /*******Restituisce il numero di    ******/
  73     /*************nodi dell'albero ***********/
  74     /*****************************************/
  75
  76     int count()
  77     {
  78         int ris=1;
  79         for (Node n:Children)
  80             ris+=n.count();
  81         return ris;
  82     }
  83
  84     public void addHPFormula(List<Formula>List,boolean deleted) {
  85         loop:for (Formula newHp:List) {
  86             for (Hypothesis oldHp: NodeHP) {
  87                 if (oldHp.HP.toString().equals(newHp.toString())) {
  88                     continue loop;
  89                 }
  90             }
  91             NodeHP.add(new Hypothesis(newHp, deleted));
  92         }
  93     }
  94
  95     public void addHPList(List<Hypothesis>List) {
  96         loop:for (Hypothesis newHp:List) {
  97             for (Hypothesis oldHp: NodeHP) {
  98                 if (oldHp.HP.toString().equals(newHp.HP.toString())) {
  99                     continue loop;
 100                 }
 101             }
 102             Hypothesis copyHP=new Hypothesis(newHp.HP, newHp.isDeleted);
 103             copyHP.fromNode=newHp.fromNode;
 104             NodeHP.add(copyHP);
 105         }
 106     }
 107
 108     public boolean searchFocus(Node caller)
 109     {
 110         if (Children.size()==0) //caso base: controllo se il focus può essere su di me
 111         {
 112             if (status!=OPEN && status!=FAKE) //nodo chiuso: il focus non può essere su di me
 113                 return false;
 114             hasFocus=true;                             //posso assumere il focus
 115             if (handler!=null)
 116                 handler.onClick(view);
 117             return true;
 118         }
 119         //passo induttivo: vado su tutti i miei figli, poi su mio padre. Termino se il padre è null.
 120         for (Node n:Children) {
 121             if (caller != null)
 122                 if (n == caller) //per ogni figlio diverso dal chiamante
 123                 {
 124                     continue;
 125                 }
 126             if(n.searchFocus(null))
 127                 return true;
 128         }
 129         if (caller==null) //ero stato chiamato da mio padre: è inutile richiamarlo
 130             return false;
 131         else if (Father==null)
 132             return false; //padre null: l'albero è dimostrato e non ci sono nodi a cui dare il focus.
 133         else
 134             return Father.searchFocus(this); //propaga il searchFocus sul padre
 135     }
 136     public void addChild(Node N) {
 137         N.Father = this;
 138         Children.add(N);
 139         Node tmp=Father;
 140         baseLine=FIELD_UNSET;
 141         maxWidth=FIELD_UNSET;
 142         leftOffset=FIELD_UNSET;
 143         rightOffset=FIELD_UNSET;
 144         while (tmp!=null)
 145         {
 146             tmp.baseLine=FIELD_UNSET;
 147             tmp.leftOffset=FIELD_UNSET;
 148             tmp.rightOffset=FIELD_UNSET;
 149             tmp.maxWidth=FIELD_UNSET;
 150             tmp=tmp.Father;
 151         }
 152     }
 153
 154     public float getBaseWidth() {
 155         return F.size();
 156     }
 157
 158     public float getMaxWidth() //ritorna la larghezza massima del sottoalbero
 159     {
 160         if (maxWidth!=FIELD_UNSET)
 161             return maxWidth;
 162         else
 163             maxWidth=getLeftOffset()+getBaseWidth()+getRightOffset();
 164         return (maxWidth);
 165     }
 166
 167     public float getLineWidth()
 168     {
 169         if (baseLine!=FIELD_UNSET)
 170             return baseLine;
 171         else
 172         {
 173             float spaceSize = DrawActivity.spaceSize;
 174             if (Children.size() == 0)
 175                 return (getBaseWidth());
 176             int res = 0;
 177             for (Node n:Children)
 178                 res += (n.getMaxWidth()) + spaceSize;
 179             res -= spaceSize;
 180             res -= Children.get(0).getLeftOffset();
 181             res -= Children.get(Children.size() - 1).getRightOffset();
 182             baseLine=Math.max(res,getBaseWidth());
 183             return baseLine;
 184         }
 185     }
 186     public float getUpLine()
 187     {
 188         float spaceSize= DrawActivity.spaceSize;
 189         if (Children.size()==0)
 190             return(getBaseWidth());
 191         int res=0;
 192         for(Node n:Children)
 193             res+=(n.getMaxWidth())+spaceSize;
 194         res-=spaceSize;
 195         res-=Children.get(0).getLeftOffset();
 196         res-=Children.get(Children.size()-1).getRightOffset();
 197         return res;
 198     }
 199     public float getLeftOffset() {
 200         if (leftOffset != FIELD_UNSET) {
 201             return leftOffset;
 202         }
 203         else {
 204             if (Children.size() == 0) //foglia
 205                 leftOffset=0;
 206             else
 207                 leftOffset=Math.max(Children.get(0).getLeftOffset() + ((getUpLine() - getBaseWidth()) / 2),0);
 208             return leftOffset;
 209         }
 210     }
 211
 212     public float getMaxHeight()
 213     {
 214         float baseRes=F.height();
 215         float res=baseRes;
 216         for (Node n:Children)
 217         {
 218             float tempH=n.getMaxHeight()+baseRes;
 219             if(tempH>res)
 220                 res=tempH;
 221         }
 222         return res;
 223     }
 224     public float getRightOffset()
 225     {
 226         if (rightOffset!=FIELD_UNSET)
 227             return rightOffset;
 228         else {
 229             if (Children.size() == 0) //foglia
 230                 rightOffset=0;
 231             else
 232                 rightOffset=Math.max(Children.get(Children.size() - 1).getRightOffset() + ((getUpLine() - getBaseWidth()) / 2),0);
 233             return rightOffset;
 234         }
 235     }
 236     void Refactor()
 237     {
 238         baseLine=FIELD_UNSET;
 239         leftOffset=FIELD_UNSET;
 240         rightOffset=FIELD_UNSET;
 241         maxWidth=FIELD_UNSET;
 242         for(Node n:Children)
 243             n.Refactor();
 244     }
 245
 246     void Resize()
 247     {
 248         int i;
 249         float interval=0; //intervallo di spazio da sommare nella creazione dei figli
 250         float spaceSize= DrawActivity.spaceSize;
 251         int childNo=Children.size();
 252         if (childNo!=0)
 253         {
 254
 255             ruleView.setText(ruleName);
 256             ruleView.setTextSize(TypedValue.COMPLEX_UNIT_PX, DrawActivity.textSize / 2);
 257             RelativeLayout.LayoutParams intlp=new RelativeLayout.LayoutParams(ViewGroup.LayoutParams.WRAP_CONTENT, ViewGroup.LayoutParams.WRAP_CONTENT);
 258             intlp.addRule(RelativeLayout.RIGHT_OF,view.getId());
 259             int sum=0;
 260             sum+=F.height();
 261             Node tmp=Father;
 262             while (tmp!=null)
 263             {
 264                 sum+=tmp.F.height();
 265                 tmp=tmp.Father;
 266             }
 267             intlp.setMargins(0,0,0,sum);
 268             intlp.addRule(RelativeLayout.ALIGN_PARENT_BOTTOM);
 269             ruleView.setLayoutParams(intlp);
 270         }
 271         for (i=0;i<childNo;i++) {
 272             Node newChild=Children.get(i);
 273             RelativeLayout.LayoutParams lp=new RelativeLayout.LayoutParams(ViewGroup.LayoutParams.WRAP_CONTENT, ViewGroup.LayoutParams.WRAP_CONTENT);
 274             TextView childView=Children.get(i).view;
 275             lp.addRule(RelativeLayout.ABOVE,view.getId());
 276             if (i==0) //first child
 277             {
 278                 float leftPos= view.getLeft()-Math.max((newChild.getLineWidth()-newChild.getBaseWidth())/2,0);
 279                 if (getLineWidth()>getUpLine())
 280                     leftPos+=((getLineWidth()-getUpLine())/2);
 281                 lp.setMargins(Math.round(leftPos), 0, 0, 0);
 282                 childView.setLeft(Math.round(leftPos));
 283             }
 284             else {
 285                 lp.setMargins(Math.round(view.getLeft() + interval), 0, 0, 0);
 286                 childView.setLeft(Math.round(view.getLeft() + interval));
 287             }
 288             childView.setLayoutParams(lp);
 289             childView.setTextSize(TypedValue.COMPLEX_UNIT_PX, DrawActivity.textSize);
 290
 291             if(newChild.status==CANCELED || newChild.status==FAKE_CANCELED)
 292                 childView.setWidth((int) ((newChild.F.sizeDeleted())));
 293             else
 294                 childView.setWidth(Math.round(newChild.getLineWidth()));
 295
 296             newChild.Resize();
 297
 298             if (i!=childNo-1) //l'ultimo figlio non ha intervalli
 299             {
 300                 float leftOverflow=(Children.get(i+1).getLineWidth()-Children.get(i+1).getBaseWidth())/2;
 301                 interval += (newChild.getBaseWidth()+newChild.getRightOffset()+Children.get(i+1).getLeftOffset()-(leftOverflow));
 302                 interval+=spaceSize;
 303                 if (i!=0) //devo sommare anche il leftOverflow del nuovo figlio
 304                     interval+=newChild.getLeftOffset();
 305             }
 306
 307         }
 308
 309     }
 310
 311     public int treeHeight()
 312     {
 313         int res=0,tmp;
 314         for (Node n:Children)
 315         {
 316             tmp=n.treeHeight();
 317             if (tmp>res)
 318                 res=tmp;
 319         }
 320         return res+1;
 321     }
 322     public boolean isCorrect()
 323     {
 324         if (status==FAKE || status==FAKE_CANCELED || status==FAKE_CLOSED)
 325             return false;
 326         else for (Node n:Children)
 327             if (!n.isCorrect())
 328                 return false;
 329         return true;
 330
 331     }
 332     public void Clean()
 333     {
 334         global.removeAllViews();
 335     }
 336
 337     public void Draw()
 338     {
 339         int i;
 340         float interval=0; //intervallo di spazio da sommare nella creazione dei figli
 341         float spaceSize= DrawActivity.spaceSize;
 342         int childNo=Children.size();
 343         if (childNo==0) //foglia: possibile ramo dimostrato
 344         {
 345             view.setBorders(null); //le foglie non hanno overline
 346             if (status!=OPEN && status!=FAKE) { //nodo chiuso
 347                 view.setTextColor(Color.GRAY);
 348                 if (hasFocus) //avevo il focus: provo a darlo ad uno dei miei fratelli
 349                 {
 350                     if (!(Father.searchFocus(this))) {
 351                         DrawActivity.finishedTree(view.getContext());
 352                         return;
 353                     }
 354                     hasFocus = false;
 355                 }
 356                 if (status==CANCELED || status==FAKE_CANCELED) { //nodo cancellato
 357                     view.setWidth((int) F.sizeDeleted());
 358                     view.setText("[" + view.getText() + "]");
 359                     view.setOnClickListener(null); //rimuove eventuali listener per evitare il proseguimento dell'albero
 360                 }
 361                 return;
 362             }
 363             if (hasFocus && DrawActivity.selectedNode!=this)
 364                 handler.onClick(view);
 365             else if (hasFocus) //hasFocus: must be colored red anyway
 366                 view.setTextColor(Color.RED);
 367             return;
 368         }
 369
 370         ruleView.setText(ruleName);
 371         ruleView.setTextSize(TypedValue.COMPLEX_UNIT_PX, DrawActivity.textSize / 2);
 372         RelativeLayout.LayoutParams intlp=new RelativeLayout.LayoutParams(ViewGroup.LayoutParams.WRAP_CONTENT, ViewGroup.LayoutParams.WRAP_CONTENT);
 373         intlp.addRule(RelativeLayout.RIGHT_OF,view.getId());
 374         int sum=0;
 375         sum+=F.height();
 376         Node tmp=Father;
 377         while (tmp!=null)
 378         {
 379             sum+=tmp.F.height();
 380             tmp=tmp.Father;
 381         }
 382         intlp.setMargins(0,0,0,sum);
 383         intlp.addRule(RelativeLayout.ALIGN_PARENT_BOTTOM);
 384         ruleView.setLayoutParams(intlp);
 385         global.addView(ruleView);
 386
 387         /////////////////
 388
 389
 390         hasFocus=false;
 391         for (i=0;i<childNo;i++) {
 392             final Node newChild=Children.get(i);
 393             RelativeLayout.LayoutParams lp=new RelativeLayout.LayoutParams(ViewGroup.LayoutParams.WRAP_CONTENT, ViewGroup.LayoutParams.WRAP_CONTENT);
 394             final BorderedTextView childView=new BorderedTextView(view.getContext());
 395             childView.setBorders(DrawActivity.b);
 396             lp.addRule(RelativeLayout.ABOVE, view.getId());
 397             if (i==0) //first child
 398             {
 399                 float leftPos= view.getLeft()-Math.max((newChild.getLineWidth()-newChild.getBaseWidth())/2,0);
 400                 if (getLineWidth()>getUpLine())
 401                     leftPos+=((getLineWidth()-getUpLine())/2);
 402
 403                 lp.setMargins(Math.round(leftPos), 0, 0, 0);
 404                 childView.setLeft(Math.round(leftPos));
 405             }
 406             else {
 407                 lp.setMargins(Math.round(view.getLeft() + interval), 0, 0, 0);
 408                 childView.setLeft(Math.round(view.getLeft() + interval));
 409             }
 410             childView.setLayoutParams(lp);
 411             childView.setId(DrawActivity.globalId++);
 412             childView.setText(newChild.F.toString());
 413             childView.setTextSize(TypedValue.COMPLEX_UNIT_PX, DrawActivity.textSize);
 414             childView.setGravity(Gravity.CENTER); //formula al centro della sua overline
 415             childView.setWidth(Math.round(newChild.getLineWidth()));
 416             global.addView(childView);
 417             childView.getViewTreeObserver().addOnGlobalLayoutListener(new ViewTreeObserver.OnGlobalLayoutListener() {
 418                 @Override
 419                 public void onGlobalLayout() {
 420                     newChild.setView(childView,global);
 421                     if(newChild.handler==null)
 422                         newChild.handler=new touchnodeHandler(newChild);
 423                     newChild.view.setOnClickListener(newChild.handler);
 424                     childView.getViewTreeObserver().removeOnGlobalLayoutListener(this);
 425                     newChild.Draw();
 426                 }
 427             });
 428             if (i!=childNo-1) //l'ultimo figlio non ha intervalli
 429             {
 430                 float leftOverflow=Math.max((Children.get(i+1).getLineWidth()-Children.get(i+1).getBaseWidth())/2,0);
 431                 interval += (newChild.getBaseWidth()+newChild.getRightOffset()+Children.get(i+1).getLeftOffset()-(leftOverflow));
 432                 interval+=spaceSize;
 433                 if (i!=0) //devo sommare anche il leftOverflow del nuovo figlio
 434                     interval+=newChild.getLeftOffset();
 435             }
 436         }
 437     }
 438
 439 }