From 43819143cf823e6767dc944fc4b095cf9a773ba2 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 9 Dec 2014 15:39:48 +0100 Subject: [PATCH] New version (to be tested). --- mainActivity/AndroidManifest.xml | 1 + mainActivity/res/menu/my.xml | 4 - .../furt/myapplication/BorderedTextView.java | 1 - .../furt/myapplication/CopyPasteDialog.java | 10 +- .../myapplication/DialogTouchHandler.java | 36 +- .../furt/myapplication/DrawActivity.java | 97 +- .../furt/myapplication/EliminationRule.java | 7 +- .../example/furt/myapplication/Formula.java | 3 +- .../furt/myapplication/FormulaAnd.java | 3 + .../furt/myapplication/FormulaBOT.java | 1 + .../furt/myapplication/FormulaImpl.java | 6 +- .../furt/myapplication/FormulaNot.java | 4 +- .../example/furt/myapplication/FormulaOr.java | 7 +- .../furt/myapplication/FormulaTOP.java | 8 +- .../furt/myapplication/GenericFormula.java | 10 +- .../furt/myapplication/Hypothesis.java | 5 +- .../furt/myapplication/IntroductionRule.java | 1 - .../example/furt/myapplication/Literal.java | 6 +- .../furt/myapplication/LongHPClick.java | 3 + .../com/example/furt/myapplication/MD5.java | 19 - .../com/example/furt/myapplication/Node.java | 269 ++-- .../myapplication/RuleAndElimination.java | 12 +- .../myapplication/RuleBotElimination.java | 12 +- .../furt/myapplication/RuleDialog.java | 109 +- .../myapplication/RuleImplElimination.java | 4 - .../furt/myapplication/RuleIntroduction.java | 4 - .../myapplication/RuleNotElimination.java | 4 - .../furt/myapplication/RuleOrElimination.java | 4 - .../furt/myapplication/TwoDScrollView.java | 1129 ----------------- .../furt/myapplication/UndefinedFormula.java | 10 +- .../example/furt/myapplication/aggiorna.java | 4 +- .../furt/myapplication/aggiornamento.java | 2 - .../furt/myapplication/askFormula.java | 3 + .../furt/myapplication/download_page.java | 9 +- .../furt/myapplication/longnodeHandler.java | 26 + .../furt/myapplication/mainActivity.java | 2 + .../furt/myapplication/parserDialog.java | 22 +- .../furt/myapplication/recuperaPass.java | 1 + .../myapplication/serverComunication.java | 28 +- .../furt/myapplication/touchHPHandler.java | 26 +- .../myapplication/touchParserHandler.java | 6 + .../furt/myapplication/touchRuleHandler.java | 30 - .../furt/myapplication/touchnodeHandler.java | 99 +- 43 files changed, 459 insertions(+), 1588 deletions(-) delete mode 100755 mainActivity/src/com/example/furt/myapplication/TwoDScrollView.java create mode 100644 mainActivity/src/com/example/furt/myapplication/longnodeHandler.java delete mode 100755 mainActivity/src/com/example/furt/myapplication/touchRuleHandler.java diff --git a/mainActivity/AndroidManifest.xml b/mainActivity/AndroidManifest.xml index 1e93667..4eb25ff 100755 --- a/mainActivity/AndroidManifest.xml +++ b/mainActivity/AndroidManifest.xml @@ -30,6 +30,7 @@ android:exported="false"/> android:label="@string/listEs" > - (); + DrawActivity.selectedNode.Children = new ArrayList(); //eliminazione del sottoalbero DrawActivity.rootNode.Clean(); DrawActivity.startDraw(); } }); builder.setNegativeButton("Annulla", new DialogInterface.OnClickListener() { public void onClick(DialogInterface dialog, int id) { - thisNode=null; } }); // Create the AlertDialog object and return it diff --git a/mainActivity/src/com/example/furt/myapplication/DialogTouchHandler.java b/mainActivity/src/com/example/furt/myapplication/DialogTouchHandler.java index 5e41f79..eba3c67 100755 --- a/mainActivity/src/com/example/furt/myapplication/DialogTouchHandler.java +++ b/mainActivity/src/com/example/furt/myapplication/DialogTouchHandler.java @@ -1,8 +1,9 @@ package com.example.furt.myapplication; -import android.graphics.Color; import android.view.View; -import android.widget.TextView; + +/**DialogTouchHandler: Handler per la gestione delle regole cliccate + * nel Dialog delle regole di introduzione**/ public class DialogTouchHandler implements View.OnClickListener{ Node node; @@ -12,21 +13,22 @@ public class DialogTouchHandler implements View.OnClickListener{ } public void onClick(View view) { - if (RuleDialog.selectedRule!=null) - if (node==RuleDialog.selectedRule) - return; - Node sel=node; - while(sel.Father!=null) - sel=sel.Father; - sel.view.setTextColor(Color.RED); - for (Node n:sel.Children) - n.view.setTextColor(Color.RED); - if (RuleDialog.selectedRule!=null) - { - RuleDialog.selectedRule.view.setTextColor(Color.BLACK); - for (Node n:RuleDialog.selectedRule.Children) - n.view.setTextColor(Color.BLACK); + Node selectedRule=node; + while(selectedRule.Father!=null) //se l'utente ha cliccato su uno dei figli del sottoalbero risalgo alla radice + selectedRule=selectedRule.Father; + for (Node n : selectedRule.Children) { //incollo i figli del nodo sul selectedNode avendo cura di integrare le ipotesi + for (Hypothesis hp : n.NodeHP) + hp.fromNode = DrawActivity.selectedNode; //le ipotesi dei nuovi figli provengono dal nodo in cui stanno per essere inserite + n.addHPList(DrawActivity.selectedNode.NodeHP); + n.handler = null; //rimuovo l'handler per il DialogTouchHandler, che è ora inutile + DrawActivity.selectedNode.addChild(n); } - RuleDialog.selectedRule=sel; + DrawActivity.selectedNode.hasFocus = false; //il vecchio selectedNode non ha più il focus + DrawActivity.selectedNode.ruleName = selectedRule.Children.get(0).ruleName; + DrawActivity.selectedNode.Children.get(0).hasFocus = true; //il primo figlio della regola applicata acquisisce il focus + DrawActivity.nmoves++; + DrawActivity.rootNode.Clean(); + DrawActivity.startDraw(); + touchnodeHandler.ruleDialog.dismiss(); //il ruleDialog del touchnodeHandler non è più necessario } } diff --git a/mainActivity/src/com/example/furt/myapplication/DrawActivity.java b/mainActivity/src/com/example/furt/myapplication/DrawActivity.java index fea3a50..f9a9c84 100644 --- a/mainActivity/src/com/example/furt/myapplication/DrawActivity.java +++ b/mainActivity/src/com/example/furt/myapplication/DrawActivity.java @@ -20,7 +20,8 @@ import android.widget.ScrollView; import android.widget.Toast; import java.sql.Timestamp; -import java.util.ArrayList; + +import static java.lang.Thread.sleep; public class DrawActivity extends FragmentActivity { @@ -34,7 +35,7 @@ public class DrawActivity extends FragmentActivity { static Border[] b; //bordi per le borderedTextView static FragmentManager fragmentManager;//per i dialog static Node rootNode; //radice dell'albero corrente - static ScrollView scroll; + static ScrollView scroll; //Vertical ScrollView contenente l'albero static int nmoves=0;//numero di mosse static int nerrors=0;//nomero di errori static long startTime;//tempo di inizio dell'esercizio @@ -42,6 +43,7 @@ public class DrawActivity extends FragmentActivity { static int globalId =10; //variabile incrementale per l'assegnazione di ID univoci static DisplayMetrics v = new DisplayMetrics();//altezza lunghezza e densità dello schermo + //Informazioni per la comunicazione client-server: username, password, nome dell'esercizio e chiave di sessione. static String user=null; static String pass=null; static String sessionKey=null; @@ -54,17 +56,18 @@ public class DrawActivity extends FragmentActivity { setContentView(R.layout.activity_my); //recupero e setto le variabili globali - getWindowManager().getDefaultDisplay().getMetrics(v); + getWindowManager().getDefaultDisplay().getMetrics(v); //getMetrics() inserisce nella variabile V i dati metrici (altezza,larghezza,densità...) dello schermo del dispositivo globalHP = (RelativeLayout) findViewById(R.id.hpscroll); globalR = (RelativeLayout) findViewById(R.id.global); - spaceSize = 2*(textSize/v.density); + spaceSize = 2*(textSize/v.density); //lo spazio tra due sottoalberi è di due caratteri vuoti fragmentManager=getFragmentManager(); - copiedNode=null; + copiedNode=null; //inizialmente non ci sono ovviamente sottoalberi copiati scroll=(ScrollView)findViewById(R.id.vscroll); startTime=time(); b=new Border[1]; b[0]=new Border(BorderedTextView.BORDER_TOP); b[0].setWidth(2); + //Recupero i dati passati dall'Intent: username, password, nome dell'esercizio da visualizzare e chiave di sessione Bundle dati=getIntent().getExtras(); nomeEs=dati.getString("nomeEs"); user=dati.getString("user"); @@ -72,7 +75,7 @@ public class DrawActivity extends FragmentActivity { sessionKey=dati.getString("sessionKey"); //Creazione dell'albero: setto il rootNode e creo la Formula di partenza (F) - if(!populateTree()) + if(!populateTree()) //populateTree() ha fallito: file dell'esercizio corrotto. return; //Creazione dell'albero: setto i campi della view @@ -81,8 +84,10 @@ public class DrawActivity extends FragmentActivity { globalId++; selectedNode=null; addFakes=false; //di default non vengono aggiunte regole false - rootNode.setView(rootView,globalR); + rootNode.setView(rootView,globalR); //il rootNode viene legato al globalLayout attuale e alla TextView creata rootNode.handler=new touchnodeHandler(rootNode); + rootNode.longHandler=new longnodeHandler(rootNode); + rootNode.hasFocus=true; //di default, la radice ha inizialmente il focus. startDraw(); //imposto il listener per il pinch zoom @@ -120,17 +125,27 @@ public class DrawActivity extends FragmentActivity { globalR.setPadding(0,0,(int)Math.max(rootNode.getRightOffset(),halfScreen),0); globalR.getLayoutParams().height=(int)Math.max((v.heightPixels),(rootNode.getMaxHeight()+rootNode.getMaxHeight()*0.10)); //altezza della view=max(h_screen,h_tree). Aggiungo un 10% all'altezza dell'albero per approssimazione dei calcoli. globalR.requestLayout(); //aggiorna i parametri e le dimensioni del RelativeLayout - if (rootNode.treeHeight()< 3) + if (rootNode.getMaxHeight()(); - for (Node c:tmp.Children) - DrawActivity.selectedNode.addChild(c); //incolla il sottoalbero del nodo copiato nella posizione richiesta - DrawActivity.rootNode.Clean(); - DrawActivity.startDraw(); - } - } - else if(id==R.id.abandon) + if(id==R.id.abandon) { //abbandona esercizio e torna alla view con la lista degli esercizi Intent i = new Intent(globalHP.getContext(), aggiornamento.class); i.putExtra("user", user); @@ -183,35 +182,6 @@ public class DrawActivity extends FragmentActivity { } - public boolean checkHP(Node source,Node target) //controlla se le ipotesi di source sono compatibili per una copia in target - { - boolean found=false; - if (!source.F.toString().equals(target.F.toString())) //se i nodi non hanno la stessa formula la copia è automaticamente impossibile - return false; - for (Hypothesis sourceHp:source.NodeHP) { - for (Hypothesis destHp : target.NodeHP) { - if (destHp.HP.toString().equals(sourceHp.HP.toString())) { //per ogni ipotesi nel nodo sorgente cerco se è disponibile nel nodo destinazione: in caso affermativo, proseguo il ciclo (found=true). - found = true; - break; - } - } - if (!found) - return false; - else found=false; - } - return true; - } - - public Node duplicateNode(Node src) //metodo di supporto che duplica un nodo - { - Node tmp=new Node(src.F); - tmp.addHPList(src.NodeHP); - tmp.ruleName=src.ruleName; - for (Node n:src.Children) { - tmp.addChild(duplicateNode(n)); - } - return tmp; - } public class simpleOnScaleGestureListener extends ScaleGestureDetector.SimpleOnScaleGestureListener { @@ -247,8 +217,23 @@ public class DrawActivity extends FragmentActivity { int second= (int) ((endTime-startTime)/1000); int minute=second/60; Toast.makeText(context, "Esercizio completato in " + Integer.toString(nmoves) + " mosse!", Toast.LENGTH_LONG).show(); + try { + sleep(2); + } catch (InterruptedException e) { + e.printStackTrace(); + } Toast.makeText(context, "Hai commesso " + Integer.toString(nerrors) + " errori!", Toast.LENGTH_LONG).show(); + try { + sleep(2); + } catch (InterruptedException e) { + e.printStackTrace(); + } Toast.makeText(context, "Numero nodi dell'albero: " + Integer.toString(rootNode.count()), Toast.LENGTH_LONG).show(); + try { + sleep(2); + } catch (InterruptedException e) { + e.printStackTrace(); + } Toast.makeText(context, "Tempo impiegato: " + Integer.toString(minute) + " minuti e " + Integer.toString(second-(minute*60)) + " secondi", Toast.LENGTH_LONG).show(); //aggiungo l'esercizio al database int voto=valutazione.voto(nomeEs,nmoves,second,rootNode.count(),nerrors); diff --git a/mainActivity/src/com/example/furt/myapplication/EliminationRule.java b/mainActivity/src/com/example/furt/myapplication/EliminationRule.java index 7285a4a..cc55c45 100755 --- a/mainActivity/src/com/example/furt/myapplication/EliminationRule.java +++ b/mainActivity/src/com/example/furt/myapplication/EliminationRule.java @@ -1,11 +1,8 @@ package com.example.furt.myapplication; -import java.util.ArrayList; -import java.util.List; - +/**EliminationRule: interfaccia per le regole di eliminazione**/ public interface EliminationRule { - public String getName(); - public Node createNodes(Formula F, askFormula ask); + public Node createNodes(Formula F, askFormula ask); //restituisce il sottoalbero successivo all'applicazione della regola sul nodo attualmente selezionato } diff --git a/mainActivity/src/com/example/furt/myapplication/Formula.java b/mainActivity/src/com/example/furt/myapplication/Formula.java index 4209b58..0145444 100755 --- a/mainActivity/src/com/example/furt/myapplication/Formula.java +++ b/mainActivity/src/com/example/furt/myapplication/Formula.java @@ -1,7 +1,8 @@ package com.example.furt.myapplication; import java.util.List; - +/**Formula:interfaccia per l'implementazione di formule logiche. Prevede metodi per + * l'applicazione delle regole e per la gestione dell'editor guidato per l'inserimento.**/ public interface Formula extends FView{ public List introductionRules(); public List EliminationRules(); diff --git a/mainActivity/src/com/example/furt/myapplication/FormulaAnd.java b/mainActivity/src/com/example/furt/myapplication/FormulaAnd.java index 2c81ee9..fe75584 100755 --- a/mainActivity/src/com/example/furt/myapplication/FormulaAnd.java +++ b/mainActivity/src/com/example/furt/myapplication/FormulaAnd.java @@ -31,6 +31,8 @@ public class FormulaAnd extends GenericFormula implements Formula { List rules=new ArrayList(); rules.addAll(super.introductionRules()); + + //Regola di introduzione dell'And RuleIntroduction andIntroduction=new RuleIntroduction("∧i",5); Node Left=new Node(leftF); Node Right=new Node(rightF); @@ -39,6 +41,7 @@ public class FormulaAnd extends GenericFormula implements Formula thisNode.addChild(Right); andIntroduction.tempRule=thisNode; rules.add(andIntroduction); + return rules; } public List EliminationRules() diff --git a/mainActivity/src/com/example/furt/myapplication/FormulaBOT.java b/mainActivity/src/com/example/furt/myapplication/FormulaBOT.java index 6103bd8..f5e905b 100755 --- a/mainActivity/src/com/example/furt/myapplication/FormulaBOT.java +++ b/mainActivity/src/com/example/furt/myapplication/FormulaBOT.java @@ -19,6 +19,7 @@ public class FormulaBOT extends GenericFormula implements Formula{ } public List introductionRules(){ + //Bottom non ha regole di introduzione sensate List nodes=new ArrayList(); return nodes; } diff --git a/mainActivity/src/com/example/furt/myapplication/FormulaImpl.java b/mainActivity/src/com/example/furt/myapplication/FormulaImpl.java index 9761a0e..efe1714 100755 --- a/mainActivity/src/com/example/furt/myapplication/FormulaImpl.java +++ b/mainActivity/src/com/example/furt/myapplication/FormulaImpl.java @@ -28,7 +28,10 @@ public class FormulaImpl extends GenericFormula implements Formula public List introductionRules(){ List nodes=new ArrayList(); - nodes.addAll(super.introductionRules()); + nodes.addAll(super.introductionRules()); //aggiunge la regola di R.A.A. + + //Regola di introduzione dell'implicazione + RuleIntroduction implIntro=new RuleIntroduction("⇒i",10); Node ImplN=new Node(rightF); List implHP=new ArrayList(); @@ -38,6 +41,7 @@ public class FormulaImpl extends GenericFormula implements Formula thisNode.addChild(ImplN); implIntro.tempRule=thisNode; nodes.add(implIntro); + return nodes; } public List EliminationRules() diff --git a/mainActivity/src/com/example/furt/myapplication/FormulaNot.java b/mainActivity/src/com/example/furt/myapplication/FormulaNot.java index f8b0d37..6bd80e5 100755 --- a/mainActivity/src/com/example/furt/myapplication/FormulaNot.java +++ b/mainActivity/src/com/example/furt/myapplication/FormulaNot.java @@ -27,6 +27,8 @@ public class FormulaNot extends GenericFormula implements Formula{ public List introductionRules(){ List nodes=new ArrayList(); + + //Introduzione del not (NOTA: il not non eredita la regola di riduzione ad assurdo) RuleIntroduction notIntro=new RuleIntroduction("¬i",4); Node notN=new Node(new FormulaBOT()); List notHP=new ArrayList(); @@ -63,4 +65,4 @@ public class FormulaNot extends GenericFormula implements Formula{ public Formula duplicate() { return new FormulaNot(Operand.duplicate()); } -} \ No newline at end of file +} diff --git a/mainActivity/src/com/example/furt/myapplication/FormulaOr.java b/mainActivity/src/com/example/furt/myapplication/FormulaOr.java index 4a1794d..83531cc 100755 --- a/mainActivity/src/com/example/furt/myapplication/FormulaOr.java +++ b/mainActivity/src/com/example/furt/myapplication/FormulaOr.java @@ -30,19 +30,24 @@ public class FormulaOr extends GenericFormula implements Formula public List introductionRules(){ List nodes=new ArrayList(); - nodes.addAll(super.introductionRules()); + nodes.addAll(super.introductionRules()); //eredita la R.A.A. + + //Introduzione sinistra dell'or RuleIntroduction orIntroductionLeft=new RuleIntroduction("∨i(L)",6); Node orLeft=new Node(leftF); Node thisNodeL=new Node(this); thisNodeL.addChild(orLeft); orIntroductionLeft.tempRule=thisNodeL; nodes.add(orIntroductionLeft); + + //Introduzione destra dell'or RuleIntroduction orIntroductionRight=new RuleIntroduction("∨i(R)",5); Node orRight=new Node(rightF); Node thisNodeR=new Node(this); thisNodeR.addChild(orRight); orIntroductionRight.tempRule=thisNodeR; nodes.add(orIntroductionRight); + return nodes; } diff --git a/mainActivity/src/com/example/furt/myapplication/FormulaTOP.java b/mainActivity/src/com/example/furt/myapplication/FormulaTOP.java index 05cba71..8d9aa70 100755 --- a/mainActivity/src/com/example/furt/myapplication/FormulaTOP.java +++ b/mainActivity/src/com/example/furt/myapplication/FormulaTOP.java @@ -14,8 +14,9 @@ public class FormulaTOP extends GenericFormula implements Formula{ public String Draw(int p){return "Ț";} public List introductionRules(){ + //le regole di introduzione ed eliminazione per Top non sono implementate in quanto prive + //di un'applicazione effettiva nella dimostrazione List nodes=new ArrayList(); - nodes.addAll(super.introductionRules()); return nodes; } @@ -34,9 +35,4 @@ public class FormulaTOP extends GenericFormula implements Formula{ return new FormulaTOP(); } - public List eliminationRules(){ - List nodes=new ArrayList(); - return nodes; - } - } diff --git a/mainActivity/src/com/example/furt/myapplication/GenericFormula.java b/mainActivity/src/com/example/furt/myapplication/GenericFormula.java index 5e063f5..b2136ab 100755 --- a/mainActivity/src/com/example/furt/myapplication/GenericFormula.java +++ b/mainActivity/src/com/example/furt/myapplication/GenericFormula.java @@ -12,17 +12,17 @@ public class GenericFormula implements Formula int priority; public String Draw(int p) { - return ""; - } + return "?"; + } //la GenericFormula non può essere rappresentata public String toString(){return Draw(0);} public float size(){ p.setTextSize(DrawActivity.textSize); - return p.measureText(toString())+(float)(p.measureText(toString())*0.20); + return p.measureText(toString())+(float)(p.measureText(toString())*0.20);//ritorna la misura effettuata dalla classe Paint con un padding del 20% per migliorare la stima } public float sizeDeleted() { p.setTextSize(DrawActivity.textSize); - return p.measureText(toStringDeleted())+(float)(p.measureText(toStringDeleted())*0.20); + return p.measureText(toStringDeleted())+(float)(p.measureText(toStringDeleted())*0.20); //ritorna la misura effettuata dalla classe Paint con un padding del 20% per migliorare la stima } public String toStringDeleted() { @@ -33,7 +33,7 @@ public class GenericFormula implements Formula p.setTextSize(DrawActivity.textSize); Rect bounds=new Rect(); p.getTextBounds(toString(),0,toString().length(),bounds); - return (float)((bounds.height()+((float)0.20*bounds.height()))*1.5); + return (float)((bounds.height()+((float)0.20*bounds.height()))*1.5); //l'altezza della formula va moltiplicata per l'inverso della densità dello schermo (circa 1.5) } public List introductionRules(){ List rules=new ArrayList(); diff --git a/mainActivity/src/com/example/furt/myapplication/Hypothesis.java b/mainActivity/src/com/example/furt/myapplication/Hypothesis.java index 6a7d638..f951431 100755 --- a/mainActivity/src/com/example/furt/myapplication/Hypothesis.java +++ b/mainActivity/src/com/example/furt/myapplication/Hypothesis.java @@ -1,5 +1,8 @@ package com.example.furt.myapplication; +/**Hypothesis: implementa le ipotesi di un nodo. Contiene una formula, un booleano per verificare se si stratta + * di un'ipotesi scaricata e un puntatore al nodo in cui l'ipotesi è stata introdotta + */ public class Hypothesis { Formula HP; @@ -11,4 +14,4 @@ public class Hypothesis isDeleted=d; fromNode=null; } -} \ No newline at end of file +} diff --git a/mainActivity/src/com/example/furt/myapplication/IntroductionRule.java b/mainActivity/src/com/example/furt/myapplication/IntroductionRule.java index 880ca1a..9799a43 100755 --- a/mainActivity/src/com/example/furt/myapplication/IntroductionRule.java +++ b/mainActivity/src/com/example/furt/myapplication/IntroductionRule.java @@ -3,6 +3,5 @@ package com.example.furt.myapplication; public interface IntroductionRule { int getPriority(); - String getName(); public Node createNodes(askFormula ask); } diff --git a/mainActivity/src/com/example/furt/myapplication/Literal.java b/mainActivity/src/com/example/furt/myapplication/Literal.java index d129975..3da98ce 100755 --- a/mainActivity/src/com/example/furt/myapplication/Literal.java +++ b/mainActivity/src/com/example/furt/myapplication/Literal.java @@ -16,7 +16,7 @@ public class Literal extends GenericFormula implements Formula public List introductionRules(){ List nodes=new ArrayList(); - nodes.addAll(super.introductionRules()); + nodes.addAll(super.introductionRules()); //eredita la R.A.A. return nodes; } @@ -25,10 +25,6 @@ public class Literal extends GenericFormula implements Formula return false; } - public boolean isCompatible(Node n) { - return true; - } - @Override public Formula duplicate() { return new Literal(this.L.charAt(0)); diff --git a/mainActivity/src/com/example/furt/myapplication/LongHPClick.java b/mainActivity/src/com/example/furt/myapplication/LongHPClick.java index fa59a8d..69ed7c3 100755 --- a/mainActivity/src/com/example/furt/myapplication/LongHPClick.java +++ b/mainActivity/src/com/example/furt/myapplication/LongHPClick.java @@ -4,6 +4,9 @@ import android.graphics.Color; import android.os.Handler; import android.view.View; +/**LongHPClick: handler per il longtouch delle ipotesi. Illumina di giallo il nodo + * da cui proviene l'ipotesi in oggetto + */ public class LongHPClick implements View.OnLongClickListener { Node n; diff --git a/mainActivity/src/com/example/furt/myapplication/MD5.java b/mainActivity/src/com/example/furt/myapplication/MD5.java index 8f7bdc0..dc28986 100755 --- a/mainActivity/src/com/example/furt/myapplication/MD5.java +++ b/mainActivity/src/com/example/furt/myapplication/MD5.java @@ -11,25 +11,6 @@ public class MD5 { MD5(){} - /*public static String digest(String fileName) throws NoSuchAlgorithmException, IOException - { - - MessageDigest md = MessageDigest.getInstance("MD5"); - return getDigest(new FileInputStream("/var/www/html/esercizi/"+fileName), md, 2048); - } - - public static String getDigest(InputStream is, MessageDigest md, int byteArraySize) throws NoSuchAlgorithmException, IOException - { - md.reset(); - byte[] bytes = new byte[byteArraySize]; - int numBytes; - while ((numBytes = is.read(bytes)) != -1) { - md.update(bytes, 0, numBytes); - } - byte[] digest = md.digest(); - String result = new String(Hex.encodeHex(digest)); - return result; - }*/ public static String digest(String filePath) { InputStream inputStream = null; try { diff --git a/mainActivity/src/com/example/furt/myapplication/Node.java b/mainActivity/src/com/example/furt/myapplication/Node.java index 9b724ff..0a39fdf 100755 --- a/mainActivity/src/com/example/furt/myapplication/Node.java +++ b/mainActivity/src/com/example/furt/myapplication/Node.java @@ -29,16 +29,17 @@ public class Node implements Tree { List NodeHP = new ArrayList(); //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; @@ -80,11 +81,17 @@ public class Node implements Tree { ris+=n.count(); return ris; } + /**************addHP****************+*****/ + /*****************************************/ + /*******Metodi per aggiungere ipotesi*****/ + /*******sotto forma di Hypothesis o di****/ + /*************Formula*********************/ + /*****************************************/ public void addHPFormula(ListList,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; } } @@ -95,7 +102,7 @@ public class Node implements Tree { public void addHPList(ListList) { 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; } } @@ -105,6 +112,11 @@ public class Node implements Tree { } } + /*****************************************/ + /******* 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 @@ -137,6 +149,7 @@ public class Node implements Tree { 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; @@ -170,20 +183,11 @@ public class Node implements Tree { 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) @@ -192,10 +196,16 @@ public class Node implements Tree { 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; @@ -209,18 +219,6 @@ public class Node implements Tree { } } - 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) @@ -233,7 +231,21 @@ public class Node implements Tree { 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; @@ -243,83 +255,13 @@ public class Node implements Tree { 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;igetUpLine()) - 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; @@ -329,25 +271,21 @@ public class Node implements Tree { 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; } @@ -355,8 +293,12 @@ public class Node implements Tree { } 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; } @@ -371,40 +313,29 @@ public class Node implements Tree { 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;igetUpLine()) + 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); @@ -420,7 +351,9 @@ public class Node implements Tree { 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(); } @@ -428,12 +361,76 @@ public class Node implements Tree { 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;igetUpLine()) + 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 +} diff --git a/mainActivity/src/com/example/furt/myapplication/RuleAndElimination.java b/mainActivity/src/com/example/furt/myapplication/RuleAndElimination.java index 5b2c5d4..5970a86 100755 --- a/mainActivity/src/com/example/furt/myapplication/RuleAndElimination.java +++ b/mainActivity/src/com/example/furt/myapplication/RuleAndElimination.java @@ -2,13 +2,10 @@ package com.example.furt.myapplication; import java.util.ArrayList; import java.util.List; + public class RuleAndElimination implements EliminationRule { String ruleName; - public String getName() - { - return ruleName; - } FormulaAnd Fn; RuleAndElimination(FormulaAnd F){ Fn=F; @@ -17,14 +14,15 @@ public class RuleAndElimination implements EliminationRule public Node createNodes(Formula F,askFormula ask) { Formula C; - if (F==null) + if (F==null) //applicazione Top-Down: chiamo la callback C=ask.Ask(); else - C=F; + C=F; //applicazione bottom-up: il nuovo nodo è la formula F passata Node cNode=new Node(C); - if ((C.toString().equals(Fn.leftF.toString())) || (C.toString().equals(Fn.rightF.toString()))) //I can return leftAnd rule or rightAnd rule + if ((C.toString().equals(Fn.leftF.toString())) || (C.toString().equals(Fn.rightF.toString()))) //Posso utilizzare le regole di eliminazione sinistra o destra { cNode.addChild(new Node(Fn)); + cNode.ruleName=ruleName; return cNode; } Node elNode=new Node(Fn); diff --git a/mainActivity/src/com/example/furt/myapplication/RuleBotElimination.java b/mainActivity/src/com/example/furt/myapplication/RuleBotElimination.java index 83a54fd..501dfe5 100755 --- a/mainActivity/src/com/example/furt/myapplication/RuleBotElimination.java +++ b/mainActivity/src/com/example/furt/myapplication/RuleBotElimination.java @@ -3,10 +3,6 @@ package com.example.furt.myapplication; public class RuleBotElimination implements EliminationRule { String ruleName; - public String getName() - { - return ruleName; - } FormulaBOT Fn; RuleBotElimination(FormulaBOT F) { @@ -15,11 +11,15 @@ public class RuleBotElimination implements EliminationRule } public Node createNodes(Formula F,askFormula ask) { - Formula C=ask.Ask(); + Formula C; + if (F!=null) + C=F; + else + C=ask.Ask(); Node elNode=new Node(Fn); Node rNode=new Node(C); rNode.addChild(elNode); rNode.ruleName=ruleName; return rNode; } -} \ No newline at end of file +} diff --git a/mainActivity/src/com/example/furt/myapplication/RuleDialog.java b/mainActivity/src/com/example/furt/myapplication/RuleDialog.java index 6bcd7bb..1cffd89 100755 --- a/mainActivity/src/com/example/furt/myapplication/RuleDialog.java +++ b/mainActivity/src/com/example/furt/myapplication/RuleDialog.java @@ -12,17 +12,16 @@ import android.view.View; import android.view.ViewGroup; import android.view.ViewTreeObserver; import android.widget.RelativeLayout; +import android.widget.Toast; import java.util.ArrayList; import java.util.List; public class RuleDialog extends DialogFragment { List rules; - static Node selectedRule; boolean showAllRules; public RuleDialog(List r) { - selectedRule=null; rules=new ArrayList(); rules.addAll(r); showAllRules=false; @@ -31,14 +30,23 @@ public class RuleDialog extends DialogFragment { public Dialog onCreateDialog(final Bundle savedInstanceState) { // Use the Builder class for convenient dialog construction AlertDialog.Builder builder = new AlertDialog.Builder(getActivity()); + int prules=0; + for (IntroductionRule r:rules) + if (r.getPriority()>0) + prules++; + if (prules==0 && !showAllRules) + { + showAllRules=true; + reboot(); + dismiss(); + return builder.create(); + } LayoutInflater inflater=getActivity().getLayoutInflater(); View view=inflater.inflate(R.layout.ruledialog,null); RelativeLayout layout=(RelativeLayout)((ViewGroup)((ViewGroup)view).getChildAt(0)).getChildAt(0); int ruleInterval=50; - int i=0; - for (i=0;i(); + for (Node c:tmp.Children) + DrawActivity.selectedNode.addChild(c); //incolla il sottoalbero del nodo copiato nella posizione richiesta + DrawActivity.rootNode.Clean(); + DrawActivity.startDraw(); + } + } + }); if (!showAllRules) { builder.setNeutralButton("Mostra tutte", new DialogInterface.OnClickListener() { public void onClick(DialogInterface dialog, int id) { - showAllRules = true; + showAllRules=true; reboot(); } }); @@ -107,14 +116,13 @@ public class RuleDialog extends DialogFragment { else { builder.setNeutralButton("Nascondi", new DialogInterface.OnClickListener() { public void onClick(DialogInterface dialog, int id) { - showAllRules = false; + showAllRules=false; reboot(); } }); } builder.setNegativeButton("Annulla", new DialogInterface.OnClickListener() { public void onClick(DialogInterface dialog, int id) { - selectedRule=null; } }); // Create the AlertDialog object and return it @@ -122,10 +130,39 @@ public class RuleDialog extends DialogFragment { } void reboot() { - selectedRule=null; - RuleDialog ruleDialog=new RuleDialog(rules); - ruleDialog.showAllRules=showAllRules; - ruleDialog.show(DrawActivity.fragmentManager, "CIAO"); + touchnodeHandler.ruleDialog=new RuleDialog(rules); + touchnodeHandler.ruleDialog.showAllRules=showAllRules; + touchnodeHandler.ruleDialog.show(DrawActivity.fragmentManager, "CIAO"); + } + + public boolean checkHP(Node source,Node target) //controlla se le ipotesi di source sono compatibili per una copia in target + { + boolean found=false; + if (!source.F.toString().equals(target.F.toString())) //se i nodi non hanno la stessa formula la copia è automaticamente impossibile + return false; + for (Hypothesis sourceHp:source.NodeHP) { + for (Hypothesis destHp : target.NodeHP) { + if (destHp.HP.toString().equals(sourceHp.HP.toString())) { //per ogni ipotesi nel nodo sorgente cerco se è disponibile nel nodo destinazione: in caso affermativo, proseguo il ciclo (found=true). + found = true; + break; + } + } + if (!found) + return false; + else found=false; + } + return true; + } + + public Node duplicateNode(Node src) //metodo di supporto che duplica un nodo + { + Node tmp=new Node(src.F); + tmp.addHPList(src.NodeHP); + tmp.ruleName=src.ruleName; + for (Node n:src.Children) { + tmp.addChild(duplicateNode(n)); + } + return tmp; } } diff --git a/mainActivity/src/com/example/furt/myapplication/RuleImplElimination.java b/mainActivity/src/com/example/furt/myapplication/RuleImplElimination.java index 0c266dd..f2fd1ff 100755 --- a/mainActivity/src/com/example/furt/myapplication/RuleImplElimination.java +++ b/mainActivity/src/com/example/furt/myapplication/RuleImplElimination.java @@ -3,10 +3,6 @@ package com.example.furt.myapplication; public class RuleImplElimination implements EliminationRule { String ruleName; - public String getName() - { - return ruleName; - } FormulaImpl Fn; RuleImplElimination(FormulaImpl F) { diff --git a/mainActivity/src/com/example/furt/myapplication/RuleIntroduction.java b/mainActivity/src/com/example/furt/myapplication/RuleIntroduction.java index 67301e0..ed0b6a1 100755 --- a/mainActivity/src/com/example/furt/myapplication/RuleIntroduction.java +++ b/mainActivity/src/com/example/furt/myapplication/RuleIntroduction.java @@ -11,10 +11,6 @@ public class RuleIntroduction implements IntroductionRule { ruleName=name; priority=p; } - public String getName() - { - return ruleName; - } public Node createNodes(askFormula ask) { Formula C=ask.Ask(); diff --git a/mainActivity/src/com/example/furt/myapplication/RuleNotElimination.java b/mainActivity/src/com/example/furt/myapplication/RuleNotElimination.java index ec5034b..7c7aaca 100755 --- a/mainActivity/src/com/example/furt/myapplication/RuleNotElimination.java +++ b/mainActivity/src/com/example/furt/myapplication/RuleNotElimination.java @@ -3,10 +3,6 @@ package com.example.furt.myapplication; public class RuleNotElimination implements EliminationRule { String ruleName; - public String getName() - { - return ruleName; - } FormulaNot Fn; RuleNotElimination(FormulaNot F) { diff --git a/mainActivity/src/com/example/furt/myapplication/RuleOrElimination.java b/mainActivity/src/com/example/furt/myapplication/RuleOrElimination.java index 3d678b7..75d1a77 100755 --- a/mainActivity/src/com/example/furt/myapplication/RuleOrElimination.java +++ b/mainActivity/src/com/example/furt/myapplication/RuleOrElimination.java @@ -6,10 +6,6 @@ import java.util.List; public class RuleOrElimination implements EliminationRule { String ruleName; - public String getName() - { - return ruleName; - } FormulaOr Fn; RuleOrElimination(FormulaOr F) { diff --git a/mainActivity/src/com/example/furt/myapplication/TwoDScrollView.java b/mainActivity/src/com/example/furt/myapplication/TwoDScrollView.java deleted file mode 100755 index 8108428..0000000 --- a/mainActivity/src/com/example/furt/myapplication/TwoDScrollView.java +++ /dev/null @@ -1,1129 +0,0 @@ -package com.example.furt.myapplication; - -import android.content.Context; -import android.graphics.Rect; -import android.util.AttributeSet; -import android.view.FocusFinder; -import android.view.KeyEvent; -import android.view.MotionEvent; -import android.view.VelocityTracker; -import android.view.View; -import android.view.ViewConfiguration; -import android.view.ViewGroup; -import android.view.ViewParent; -import android.view.animation.AnimationUtils; -import android.widget.FrameLayout; -import android.widget.Scroller; - -import java.util.List; - - -/** - * Copyright (C) 2006 The Android Open Source Project - * - * Licensed under the Apache License, Version 2.0 (the "License"); - * you may not use this file except in compliance with the License. - * You may obtain a copy of the License at - * - * http://www.apache.org/licenses/LICENSE-2.0 - * - * Unless required by applicable law or agreed to in writing, software - * distributed under the License is distributed on an "AS IS" BASIS, - * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. - * See the License for the specific language governing permissions and - * limitations under the License. - * -* - * Revised 5/19/2010 by GORGES - * Now supports two-dimensional view scrolling - * http://GORGES.us - */ - -/** - * Layout container for a view hierarchy that can be scrolled by the user, - * allowing it to be larger than the physical display. A TwoDScrollView - * is a {@link android.widget.FrameLayout}, meaning you should place one child in it - * containing the entire contents to scroll; this child may itself be a layout - * manager with a complex hierarchy of objects. A child that is often used - * is a {@link android.widget.LinearLayout} in a vertical orientation, presenting a vertical - * array of top-level items that the user can scroll through. - * - *

The {@link android.widget.TextView} class also - * takes care of its own scrolling, so does not require a TwoDScrollView, but - * using the two together is possible to achieve the effect of a text view - * within a larger container. - */ - -public class TwoDScrollView extends FrameLayout { - static final int ANIMATED_SCROLL_GAP = 250; - static final float MAX_SCROLL_FACTOR = 0.5f; - - private long mLastScroll; - - private final Rect mTempRect = new Rect(); - private Scroller mScroller; - - /* - * Flag to indicate that we are moving focus ourselves. This is so the - * code that watches for focus changes initiated outside this TwoDScrollView - * knows that it does not have to do anything. - */ - private boolean mTwoDScrollViewMovedFocus; - - /* - * Position of the last motion event. - */ - private float mLastMotionY; - private float mLastMotionX; - - /* - * True when the layout has changed but the traversal has not come through yet. - * Ideally the view hierarchy would keep track of this for us. - */ - private boolean mIsLayoutDirty = true; - - /* - * The child to give focus to in the event that a child has requested focus while the - * layout is dirty. This prevents the scroll from being wrong if the child has not been - * laid out before requesting focus. - */ - private View mChildToScrollTo = null; - - /* - * True if the user is currently dragging this TwoDScrollView around. This is - * not the same as 'is being flinged', which can be checked by - * mScroller.isFinished() (flinging begins when the user lifts his finger). - */ - private boolean mIsBeingDragged = false; - - /* - * Determines speed during touch scrolling - */ - private VelocityTracker mVelocityTracker; - - /* - * Whether arrow scrolling is animated. - */ - private int mTouchSlop; - private int mMinimumVelocity; - private int mMaximumVelocity; - - public TwoDScrollView(Context context) { - super(context); - initTwoDScrollView(); - } - - public TwoDScrollView(Context context, AttributeSet attrs) { - super(context, attrs); - initTwoDScrollView(); - } - - public TwoDScrollView(Context context, AttributeSet attrs, int defStyle) { - super(context, attrs, defStyle); - initTwoDScrollView(); - } - - @Override - protected float getTopFadingEdgeStrength() { - if (getChildCount() == 0) { - return 0.0f; - } - final int length = getVerticalFadingEdgeLength(); - if (getScrollY() < length) { - return getScrollY() / (float) length; - } - return 1.0f; - } - - @Override - protected float getBottomFadingEdgeStrength() { - if (getChildCount() == 0) { - return 0.0f; - } - final int length = getVerticalFadingEdgeLength(); - final int bottomEdge = getHeight() - getPaddingBottom(); - final int span = getChildAt(0).getBottom() - getScrollY() - bottomEdge; - if (span < length) { - return span / (float) length; - } - return 1.0f; - } - - @Override - protected float getLeftFadingEdgeStrength() { - if (getChildCount() == 0) { - return 0.0f; - } - final int length = getHorizontalFadingEdgeLength(); - if (getScrollX() < length) { - return getScrollX() / (float) length; - } - return 1.0f; - } - - @Override - protected float getRightFadingEdgeStrength() { - if (getChildCount() == 0) { - return 0.0f; - } - final int length = getHorizontalFadingEdgeLength(); - final int rightEdge = getWidth() - getPaddingRight(); - final int span = getChildAt(0).getRight() - getScrollX() - rightEdge; - if (span < length) { - return span / (float) length; - } - return 1.0f; - } - - /** - * @return The maximum amount this scroll view will scroll in response to - * an arrow event. - */ - public int getMaxScrollAmountVertical() { - return (int) (MAX_SCROLL_FACTOR * getHeight()); - } - public int getMaxScrollAmountHorizontal() { - return (int) (MAX_SCROLL_FACTOR * getWidth()); - } - - private void initTwoDScrollView() { - mScroller = new Scroller(getContext()); - setFocusable(true); - setDescendantFocusability(FOCUS_AFTER_DESCENDANTS); - setWillNotDraw(false); - final ViewConfiguration configuration = ViewConfiguration.get(getContext()); - mTouchSlop = configuration.getScaledTouchSlop(); - mMinimumVelocity = configuration.getScaledMinimumFlingVelocity(); - mMaximumVelocity = configuration.getScaledMaximumFlingVelocity(); - } - - @Override - public void addView(View child) { - if (getChildCount() > 0) { - throw new IllegalStateException("TwoDScrollView can host only one direct child"); - } - super.addView(child); - } - - @Override - public void addView(View child, int index) { - if (getChildCount() > 0) { - throw new IllegalStateException("TwoDScrollView can host only one direct child"); - } - super.addView(child, index); - } - - @Override - public void addView(View child, ViewGroup.LayoutParams params) { - if (getChildCount() > 0) { - throw new IllegalStateException("TwoDScrollView can host only one direct child"); - } - super.addView(child, params); - } - - @Override - public void addView(View child, int index, ViewGroup.LayoutParams params) { - if (getChildCount() > 0) { - throw new IllegalStateException("TwoDScrollView can host only one direct child"); - } - super.addView(child, index, params); - } - - /** - * @return Returns true this TwoDScrollView can be scrolled - */ - private boolean canScroll() { - View child = getChildAt(0); - if (child != null) { - int childHeight = child.getHeight(); - int childWidth = child.getWidth(); - return (getHeight() < childHeight + getPaddingTop() + getPaddingBottom()) || - (getWidth() < childWidth + getPaddingLeft() + getPaddingRight()); - } - return false; - } - - @Override - public boolean dispatchKeyEvent(KeyEvent event) { - // Let the focused view and/or our descendants get the key first - boolean handled = super.dispatchKeyEvent(event); - if (handled) { - return true; - } - return executeKeyEvent(event); - } - - /** - * You can call this function yourself to have the scroll view perform - * scrolling from a key event, just as if the event had been dispatched to - * it by the view hierarchy. - * - * @param event The key event to execute. - * @return Return true if the event was handled, else false. - */ - public boolean executeKeyEvent(KeyEvent event) { - mTempRect.setEmpty(); - if (!canScroll()) { - if (isFocused()) { - View currentFocused = findFocus(); - if (currentFocused == this) currentFocused = null; - View nextFocused = FocusFinder.getInstance().findNextFocus(this, currentFocused, View.FOCUS_DOWN); - return nextFocused != null && nextFocused != this && nextFocused.requestFocus(View.FOCUS_DOWN); - } - return false; - } - boolean handled = false; - if (event.getAction() == KeyEvent.ACTION_DOWN) { - switch (event.getKeyCode()) { - case KeyEvent.KEYCODE_DPAD_UP: - if (!event.isAltPressed()) { - handled = arrowScroll(View.FOCUS_UP, false); - } else { - handled = fullScroll(View.FOCUS_UP, false); - } - break; - case KeyEvent.KEYCODE_DPAD_DOWN: - if (!event.isAltPressed()) { - handled = arrowScroll(View.FOCUS_DOWN, false); - } else { - handled = fullScroll(View.FOCUS_DOWN, false); - } - break; - case KeyEvent.KEYCODE_DPAD_LEFT: - if (!event.isAltPressed()) { - handled = arrowScroll(View.FOCUS_LEFT, true); - } else { - handled = fullScroll(View.FOCUS_LEFT, true); - } - break; - case KeyEvent.KEYCODE_DPAD_RIGHT: - if (!event.isAltPressed()) { - handled = arrowScroll(View.FOCUS_RIGHT, true); - } else { - handled = fullScroll(View.FOCUS_RIGHT, true); - } - break; - } - } - return handled; - } - - @Override - public boolean onInterceptTouchEvent(MotionEvent ev) { - /* - * This method JUST determines whether we want to intercept the motion. - * If we return true, onMotionEvent will be called and we do the actual - * scrolling there. - * - * Shortcut the most recurring case: the user is in the dragging - * state and he is moving his finger. We want to intercept this - * motion. - */ - final int action = ev.getAction(); - if ((action == MotionEvent.ACTION_MOVE) && (mIsBeingDragged)) { - return true; - } - if (!canScroll()) { - mIsBeingDragged = false; - return false; - } - final float y = ev.getY(); - final float x = ev.getX(); - switch (action) { - case MotionEvent.ACTION_MOVE: - /* - * mIsBeingDragged == false, otherwise the shortcut would have caught it. Check - * whether the user has moved far enough from his original down touch. - */ - /* - * Locally do absolute value. mLastMotionY is set to the y value - * of the down event. - */ - final int yDiff = (int) Math.abs(y - mLastMotionY); - final int xDiff = (int) Math.abs(x - mLastMotionX); - if (yDiff > mTouchSlop || xDiff > mTouchSlop) { - mIsBeingDragged = true; - } - break; - - case MotionEvent.ACTION_DOWN: - /* Remember location of down touch */ - mLastMotionY = y; - mLastMotionX = x; - - /* - * If being flinged and user touches the screen, initiate drag; - * otherwise don't. mScroller.isFinished should be false when - * being flinged. - */ - mIsBeingDragged = !mScroller.isFinished(); - break; - - case MotionEvent.ACTION_CANCEL: - case MotionEvent.ACTION_UP: - /* Release the drag */ - mIsBeingDragged = false; - break; - } - - /* - * The only time we want to intercept motion events is if we are in the - * drag mode. - */ - return mIsBeingDragged; - } - - @Override - public boolean onTouchEvent(MotionEvent ev) { - - if (ev.getAction() == MotionEvent.ACTION_DOWN && ev.getEdgeFlags() != 0) { - // Don't handle edge touches immediately -- they may actually belong to one of our - // descendants. - return false; - } - - if (!canScroll()) { - return false; - } - - if (mVelocityTracker == null) { - mVelocityTracker = VelocityTracker.obtain(); - } - mVelocityTracker.addMovement(ev); - - final int action = ev.getAction(); - final float y = ev.getY(); - final float x = ev.getX(); - - switch (action) { - case MotionEvent.ACTION_DOWN: - /* - * If being flinged and user touches, stop the fling. isFinished - * will be false if being flinged. - */ - if (!mScroller.isFinished()) { - mScroller.abortAnimation(); - } - - // Remember where the motion event started - mLastMotionY = y; - mLastMotionX = x; - break; - case MotionEvent.ACTION_MOVE: - // Scroll to follow the motion event - int deltaX = (int) (mLastMotionX - x); - int deltaY = (int) (mLastMotionY - y); - mLastMotionX = x; - mLastMotionY = y; - - if (deltaX < 0) { - if (getScrollX() < 0) { - deltaX = 0; - } - } else if (deltaX > 0) { - final int rightEdge = getWidth() - getPaddingRight(); - final int availableToScroll = getChildAt(0).getRight() - getScrollX() - rightEdge; - if (availableToScroll > 0) { - deltaX = Math.min(availableToScroll, deltaX); - } else { - deltaX = 0; - } - } - if (deltaY < 0) { - if (getScrollY() < 0) { - deltaY = 0; - } - } else if (deltaY > 0) { - final int bottomEdge = getHeight() - getPaddingBottom(); - final int availableToScroll = getChildAt(0).getBottom() - getScrollY() - bottomEdge; - if (availableToScroll > 0) { - deltaY = Math.min(availableToScroll, deltaY); - } else { - deltaY = 0; - } - } - if (deltaY != 0 || deltaX != 0) - scrollBy(deltaX, deltaY); - break; - case MotionEvent.ACTION_UP: - final VelocityTracker velocityTracker = mVelocityTracker; - velocityTracker.computeCurrentVelocity(1000, mMaximumVelocity); - int initialXVelocity = (int) velocityTracker.getXVelocity(); - int initialYVelocity = (int) velocityTracker.getYVelocity(); - if ((Math.abs(initialXVelocity) + Math.abs(initialYVelocity) > mMinimumVelocity) && getChildCount() > 0) { - fling(-initialXVelocity, -initialYVelocity); - } - if (mVelocityTracker != null) { - mVelocityTracker.recycle(); - mVelocityTracker = null; - } - } - return true; - } - - /** - * Finds the next focusable component that fits in this View's bounds - * (excluding fading edges) pretending that this View's top is located at - * the parameter top. - * - * @param topFocus look for a candidate is the one at the top of the bounds - * if topFocus is true, or at the bottom of the bounds if topFocus is - * false - * @param top the top offset of the bounds in which a focusable must be - * found (the fading edge is assumed to start at this position) - * @param preferredFocusable the View that has highest priority and will be - * returned if it is within my bounds (null is valid) - * @return the next focusable component in the bounds or null if none can be - * found - */ - private View findFocusableViewInMyBounds(final boolean topFocus, final int top, final boolean leftFocus, final int left, View preferredFocusable) { - /* - * The fading edge's transparent side should be considered for focus - * since it's mostly visible, so we divide the actual fading edge length - * by 2. - */ - final int verticalFadingEdgeLength = getVerticalFadingEdgeLength() / 2; - final int topWithoutFadingEdge = top + verticalFadingEdgeLength; - final int bottomWithoutFadingEdge = top + getHeight() - verticalFadingEdgeLength; - final int horizontalFadingEdgeLength = getHorizontalFadingEdgeLength() / 2; - final int leftWithoutFadingEdge = left + horizontalFadingEdgeLength; - final int rightWithoutFadingEdge = left + getWidth() - horizontalFadingEdgeLength; - - if ((preferredFocusable != null) - && (preferredFocusable.getTop() < bottomWithoutFadingEdge) - && (preferredFocusable.getBottom() > topWithoutFadingEdge) - && (preferredFocusable.getLeft() < rightWithoutFadingEdge) - && (preferredFocusable.getRight() > leftWithoutFadingEdge)) { - return preferredFocusable; - } - return findFocusableViewInBounds(topFocus, topWithoutFadingEdge, bottomWithoutFadingEdge, leftFocus, leftWithoutFadingEdge, rightWithoutFadingEdge); - } - - /** - * Finds the next focusable component that fits in the specified bounds. - *

- * - * @param topFocus look for a candidate is the one at the top of the bounds - * if topFocus is true, or at the bottom of the bounds if topFocus is - * false - * @param top the top offset of the bounds in which a focusable must be - * found - * @param bottom the bottom offset of the bounds in which a focusable must - * be found - * @return the next focusable component in the bounds or null if none can - * be found - */ - private View findFocusableViewInBounds(boolean topFocus, int top, int bottom, boolean leftFocus, int left, int right) { - List focusables = getFocusables(View.FOCUS_FORWARD); - View focusCandidate = null; - - /* - * A fully contained focusable is one where its top is below the bound's - * top, and its bottom is above the bound's bottom. A partially - * contained focusable is one where some part of it is within the - * bounds, but it also has some part that is not within bounds. A fully contained - * focusable is preferred to a partially contained focusable. - */ - boolean foundFullyContainedFocusable = false; - - int count = focusables.size(); - for (int i = 0; i < count; i++) { - View view = focusables.get(i); - int viewTop = view.getTop(); - int viewBottom = view.getBottom(); - int viewLeft = view.getLeft(); - int viewRight = view.getRight(); - - if (top < viewBottom && viewTop < bottom && left < viewRight && viewLeft < right) { - /* - * the focusable is in the target area, it is a candidate for - * focusing - */ - final boolean viewIsFullyContained = (top < viewTop) && (viewBottom < bottom) && (left < viewLeft) && (viewRight < right); - if (focusCandidate == null) { - /* No candidate, take this one */ - focusCandidate = view; - foundFullyContainedFocusable = viewIsFullyContained; - } else { - final boolean viewIsCloserToVerticalBoundary = - (topFocus && viewTop < focusCandidate.getTop()) || - (!topFocus && viewBottom > focusCandidate.getBottom()); - final boolean viewIsCloserToHorizontalBoundary = - (leftFocus && viewLeft < focusCandidate.getLeft()) || - (!leftFocus && viewRight > focusCandidate.getRight()); - if (foundFullyContainedFocusable) { - if (viewIsFullyContained && viewIsCloserToVerticalBoundary && viewIsCloserToHorizontalBoundary) { - /* - * We're dealing with only fully contained views, so - * it has to be closer to the boundary to beat our - * candidate - */ - focusCandidate = view; - } - } else { - if (viewIsFullyContained) { - /* Any fully contained view beats a partially contained view */ - focusCandidate = view; - foundFullyContainedFocusable = true; - } else if (viewIsCloserToVerticalBoundary && viewIsCloserToHorizontalBoundary) { - /* - * Partially contained view beats another partially - * contained view if it's closer - */ - focusCandidate = view; - } - } - } - } - } - return focusCandidate; - } - - /** - *

Handles scrolling in response to a "home/end" shortcut press. This - * method will scroll the view to the top or bottom and give the focus - * to the topmost/bottommost component in the new visible area. If no - * component is a good candidate for focus, this scrollview reclaims the - * focus.

- * - * @param direction the scroll direction: {@link android.view.View#FOCUS_UP} - * to go the top of the view or - * {@link android.view.View#FOCUS_DOWN} to go the bottom - * @return true if the key event is consumed by this method, false otherwise - */ - public boolean fullScroll(int direction, boolean horizontal) { - if (!horizontal) { - boolean down = direction == View.FOCUS_DOWN; - int height = getHeight(); - mTempRect.top = 0; - mTempRect.bottom = height; - if (down) { - int count = getChildCount(); - if (count > 0) { - View view = getChildAt(count - 1); - mTempRect.bottom = view.getBottom(); - mTempRect.top = mTempRect.bottom - height; - } - } - return scrollAndFocus(direction, mTempRect.top, mTempRect.bottom, 0, 0, 0); - } else { - boolean right = direction == View.FOCUS_DOWN; - int width = getWidth(); - mTempRect.left = 0; - mTempRect.right = width; - if (right) { - int count = getChildCount(); - if (count > 0) { - View view = getChildAt(count - 1); - mTempRect.right = view.getBottom(); - mTempRect.left = mTempRect.right - width; - } - } - return scrollAndFocus(0, 0, 0, direction, mTempRect.top, mTempRect.bottom); - } - } - - /** - *

Scrolls the view to make the area defined by top and - * bottom visible. This method attempts to give the focus - * to a component visible in this area. If no component can be focused in - * the new visible area, the focus is reclaimed by this scrollview.

- * - * @param direction the scroll direction: {@link android.view.View#FOCUS_UP} - * to go upward - * {@link android.view.View#FOCUS_DOWN} to downward - * @param top the top offset of the new area to be made visible - * @param bottom the bottom offset of the new area to be made visible - * @return true if the key event is consumed by this method, false otherwise - */ - private boolean scrollAndFocus(int directionY, int top, int bottom, int directionX, int left, int right) { - boolean handled = true; - int height = getHeight(); - int containerTop = getScrollY(); - int containerBottom = containerTop + height; - boolean up = directionY == View.FOCUS_UP; - int width = getWidth(); - int containerLeft = getScrollX(); - int containerRight = containerLeft + width; - boolean leftwards = directionX == View.FOCUS_UP; - View newFocused = findFocusableViewInBounds(up, top, bottom, leftwards, left, right); - if (newFocused == null) { - newFocused = this; - } - if ((top >= containerTop && bottom <= containerBottom) || (left >= containerLeft && right <= containerRight)) { - handled = false; - } else { - int deltaY = up ? (top - containerTop) : (bottom - containerBottom); - int deltaX = leftwards ? (left - containerLeft) : (right - containerRight); - doScroll(deltaX, deltaY); - } - if (newFocused != findFocus() && newFocused.requestFocus(directionY)) { - mTwoDScrollViewMovedFocus = true; - mTwoDScrollViewMovedFocus = false; - } - return handled; - } - - /** - * Handle scrolling in response to an up or down arrow click. - * - * @param direction The direction corresponding to the arrow key that was - * pressed - * @return True if we consumed the event, false otherwise - */ - public boolean arrowScroll(int direction, boolean horizontal) { - View currentFocused = findFocus(); - if (currentFocused == this) currentFocused = null; - View nextFocused = FocusFinder.getInstance().findNextFocus(this, currentFocused, direction); - final int maxJump = horizontal ? getMaxScrollAmountHorizontal() : getMaxScrollAmountVertical(); - - if (!horizontal) { - if (nextFocused != null) { - nextFocused.getDrawingRect(mTempRect); - offsetDescendantRectToMyCoords(nextFocused, mTempRect); - int scrollDelta = computeScrollDeltaToGetChildRectOnScreen(mTempRect); - doScroll(0, scrollDelta); - nextFocused.requestFocus(direction); - } else { - // no new focus - int scrollDelta = maxJump; - if (direction == View.FOCUS_UP && getScrollY() < scrollDelta) { - scrollDelta = getScrollY(); - } else if (direction == View.FOCUS_DOWN) { - if (getChildCount() > 0) { - int daBottom = getChildAt(0).getBottom(); - int screenBottom = getScrollY() + getHeight(); - if (daBottom - screenBottom < maxJump) { - scrollDelta = daBottom - screenBottom; - } - } - } - if (scrollDelta == 0) { - return false; - } - doScroll(0, direction == View.FOCUS_DOWN ? scrollDelta : -scrollDelta); - } - } else { - if (nextFocused != null) { - nextFocused.getDrawingRect(mTempRect); - offsetDescendantRectToMyCoords(nextFocused, mTempRect); - int scrollDelta = computeScrollDeltaToGetChildRectOnScreen(mTempRect); - doScroll(scrollDelta, 0); - nextFocused.requestFocus(direction); - } else { - // no new focus - int scrollDelta = maxJump; - if (direction == View.FOCUS_UP && getScrollY() < scrollDelta) { - scrollDelta = getScrollY(); - } else if (direction == View.FOCUS_DOWN) { - if (getChildCount() > 0) { - int daBottom = getChildAt(0).getBottom(); - int screenBottom = getScrollY() + getHeight(); - if (daBottom - screenBottom < maxJump) { - scrollDelta = daBottom - screenBottom; - } - } - } - if (scrollDelta == 0) { - return false; - } - doScroll(direction == View.FOCUS_DOWN ? scrollDelta : -scrollDelta, 0); - } - } - return true; - } - - /** - * Smooth scroll by a Y delta - * - * @param delta the number of pixels to scroll by on the Y axis - */ - private void doScroll(int deltaX, int deltaY) { - if (deltaX != 0 || deltaY != 0) { - smoothScrollBy(deltaX, deltaY); - } - } - - /** - * Like {@link android.view.View#scrollBy}, but scroll smoothly instead of immediately. - * - * @param dx the number of pixels to scroll by on the X axis - * @param dy the number of pixels to scroll by on the Y axis - */ - public final void smoothScrollBy(int dx, int dy) { - long duration = AnimationUtils.currentAnimationTimeMillis() - mLastScroll; - if (duration > ANIMATED_SCROLL_GAP) { - mScroller.startScroll(getScrollX(), getScrollY(), dx, dy); - awakenScrollBars(mScroller.getDuration()); - invalidate(); - } else { - if (!mScroller.isFinished()) { - mScroller.abortAnimation(); - } - scrollBy(dx, dy); - } - mLastScroll = AnimationUtils.currentAnimationTimeMillis(); - } - - /** - * Like {@link #scrollTo}, but scroll smoothly instead of immediately. - * - * @param x the position where to scroll on the X axis - * @param y the position where to scroll on the Y axis - */ - public final void smoothScrollTo(int x, int y) { - smoothScrollBy(x - getScrollX(), y - getScrollY()); - } - - /** - *

The scroll range of a scroll view is the overall height of all of its - * children.

- */ - @Override - protected int computeVerticalScrollRange() { - int count = getChildCount(); - return count == 0 ? getHeight() : (getChildAt(0)).getBottom(); - } - @Override - protected int computeHorizontalScrollRange() { - int count = getChildCount(); - return count == 0 ? getWidth() : (getChildAt(0)).getRight(); - } - - @Override - protected void measureChild(View child, int parentWidthMeasureSpec, int parentHeightMeasureSpec) { - ViewGroup.LayoutParams lp = child.getLayoutParams(); - int childWidthMeasureSpec; - int childHeightMeasureSpec; - - childWidthMeasureSpec = getChildMeasureSpec(parentWidthMeasureSpec, getPaddingLeft() + getPaddingRight(), lp.width); - childHeightMeasureSpec = MeasureSpec.makeMeasureSpec(0, MeasureSpec.UNSPECIFIED); - - child.measure(childWidthMeasureSpec, childHeightMeasureSpec); - } - - @Override - protected void measureChildWithMargins(View child, int parentWidthMeasureSpec, int widthUsed, int parentHeightMeasureSpec, int heightUsed) { - final MarginLayoutParams lp = (MarginLayoutParams) child.getLayoutParams(); - final int childWidthMeasureSpec = getChildMeasureSpec(parentWidthMeasureSpec, - getPaddingLeft() + getPaddingRight() + lp.leftMargin + lp.rightMargin + widthUsed, lp.width); - final int childHeightMeasureSpec = MeasureSpec.makeMeasureSpec(lp.topMargin + lp.bottomMargin, MeasureSpec.UNSPECIFIED); - - child.measure(childWidthMeasureSpec, childHeightMeasureSpec); - } - - @Override - public void computeScroll() { - if (mScroller.computeScrollOffset()) { - // This is called at drawing time by ViewGroup. We don't want to - // re-show the scrollbars at this point, which scrollTo will do, - // so we replicate most of scrollTo here. - // - // It's a little odd to call onScrollChanged from inside the drawing. - // - // It is, except when you remember that computeScroll() is used to - // animate scrolling. So unless we want to defer the onScrollChanged() - // until the end of the animated scrolling, we don't really have a - // choice here. - // - // I agree. The alternative, which I think would be worse, is to post - // something and tell the subclasses later. This is bad because there - // will be a window where mScrollX/Y is different from what the app - // thinks it is. - // - int oldX = getScrollX(); - int oldY = getScrollY(); - int x = mScroller.getCurrX(); - int y = mScroller.getCurrY(); - if (getChildCount() > 0) { - View child = getChildAt(0); - scrollTo(clamp(x, getWidth() - getPaddingRight() - getPaddingLeft(), child.getWidth()), - clamp(y, getHeight() - getPaddingBottom() - getPaddingTop(), child.getHeight())); - } else { - scrollTo(x, y); - } - if (oldX != getScrollX() || oldY != getScrollY()) { - onScrollChanged(getScrollX(), getScrollY(), oldX, oldY); - } - - // Keep on drawing until the animation has finished. - postInvalidate(); - } - } - - /** - * Scrolls the view to the given child. - * - * @param child the View to scroll to - */ - private void scrollToChild(View child) { - child.getDrawingRect(mTempRect); - /* Offset from child's local coordinates to TwoDScrollView coordinates */ - offsetDescendantRectToMyCoords(child, mTempRect); - int scrollDelta = computeScrollDeltaToGetChildRectOnScreen(mTempRect); - if (scrollDelta != 0) { - scrollBy(0, scrollDelta); - } - } - - /** - * If rect is off screen, scroll just enough to get it (or at least the - * first screen size chunk of it) on screen. - * - * @param rect The rectangle. - * @param immediate True to scroll immediately without animation - * @return true if scrolling was performed - */ - private boolean scrollToChildRect(Rect rect, boolean immediate) { - final int delta = computeScrollDeltaToGetChildRectOnScreen(rect); - final boolean scroll = delta != 0; - if (scroll) { - if (immediate) { - scrollBy(0, delta); - } else { - smoothScrollBy(0, delta); - } - } - return scroll; - } - - /** - * Compute the amount to scroll in the Y direction in order to get - * a rectangle completely on the screen (or, if taller than the screen, - * at least the first screen size chunk of it). - * - * @param rect The rect. - * @return The scroll delta. - */ - protected int computeScrollDeltaToGetChildRectOnScreen(Rect rect) { - if (getChildCount() == 0) return 0; - int height = getHeight(); - int screenTop = getScrollY(); - int screenBottom = screenTop + height; - int fadingEdge = getVerticalFadingEdgeLength(); - // leave room for top fading edge as long as rect isn't at very top - if (rect.top > 0) { - screenTop += fadingEdge; - } - - // leave room for bottom fading edge as long as rect isn't at very bottom - if (rect.bottom < getChildAt(0).getHeight()) { - screenBottom -= fadingEdge; - } - int scrollYDelta = 0; - if (rect.bottom > screenBottom && rect.top > screenTop) { - // need to move down to get it in view: move down just enough so - // that the entire rectangle is in view (or at least the first - // screen size chunk). - if (rect.height() > height) { - // just enough to get screen size chunk on - scrollYDelta += (rect.top - screenTop); - } else { - // get entire rect at bottom of screen - scrollYDelta += (rect.bottom - screenBottom); - } - - // make sure we aren't scrolling beyond the end of our content - int bottom = getChildAt(0).getBottom(); - int distanceToBottom = bottom - screenBottom; - scrollYDelta = Math.min(scrollYDelta, distanceToBottom); - - } else if (rect.top < screenTop && rect.bottom < screenBottom) { - // need to move up to get it in view: move up just enough so that - // entire rectangle is in view (or at least the first screen - // size chunk of it). - - if (rect.height() > height) { - // screen size chunk - scrollYDelta -= (screenBottom - rect.bottom); - } else { - // entire rect at top - scrollYDelta -= (screenTop - rect.top); - } - - // make sure we aren't scrolling any further than the top our content - scrollYDelta = Math.max(scrollYDelta, -getScrollY()); - } - return scrollYDelta; - } - - @Override - public void requestChildFocus(View child, View focused) { - if (!mTwoDScrollViewMovedFocus) { - if (!mIsLayoutDirty) { - scrollToChild(focused); - } else { - // The child may not be laid out yet, we can't compute the scroll yet - mChildToScrollTo = focused; - } - } - super.requestChildFocus(child, focused); - } - - /** - * When looking for focus in children of a scroll view, need to be a little - * more careful not to give focus to something that is scrolled off screen. - * - * This is more expensive than the default {@link android.view.ViewGroup} - * implementation, otherwise this behavior might have been made the default. - */ - @Override - protected boolean onRequestFocusInDescendants(int direction, Rect previouslyFocusedRect) { - // convert from forward / backward notation to up / down / left / right - // (ugh). - if (direction == View.FOCUS_FORWARD) { - direction = View.FOCUS_DOWN; - } else if (direction == View.FOCUS_BACKWARD) { - direction = View.FOCUS_UP; - } - - final View nextFocus = previouslyFocusedRect == null ? - FocusFinder.getInstance().findNextFocus(this, null, direction) : - FocusFinder.getInstance().findNextFocusFromRect(this, - previouslyFocusedRect, direction); - - if (nextFocus == null) { - return false; - } - - return nextFocus.requestFocus(direction, previouslyFocusedRect); - } - - @Override - public boolean requestChildRectangleOnScreen(View child, Rect rectangle, boolean immediate) { - // offset into coordinate space of this scroll view - rectangle.offset(child.getLeft() - child.getScrollX(), child.getTop() - child.getScrollY()); - return scrollToChildRect(rectangle, immediate); - } - - @Override - public void requestLayout() { - mIsLayoutDirty = true; - super.requestLayout(); - } - - @Override - protected void onLayout(boolean changed, int l, int t, int r, int b) { - super.onLayout(changed, l, t, r, b); - mIsLayoutDirty = false; - // Give a child focus if it needs it - if (mChildToScrollTo != null && isViewDescendantOf(mChildToScrollTo, this)) { - scrollToChild(mChildToScrollTo); - } - mChildToScrollTo = null; - - // Calling this with the present values causes it to re-clam them - scrollTo(getScrollX(), getScrollY()); - } - - @Override - protected void onSizeChanged(int w, int h, int oldw, int oldh) { - super.onSizeChanged(w, h, oldw, oldh); - - View currentFocused = findFocus(); - if (null == currentFocused || this == currentFocused) - return; - - // If the currently-focused view was visible on the screen when the - // screen was at the old height, then scroll the screen to make that - // view visible with the new screen height. - currentFocused.getDrawingRect(mTempRect); - offsetDescendantRectToMyCoords(currentFocused, mTempRect); - int scrollDeltaX = computeScrollDeltaToGetChildRectOnScreen(mTempRect); - int scrollDeltaY = computeScrollDeltaToGetChildRectOnScreen(mTempRect); - doScroll(scrollDeltaX, scrollDeltaY); - } - - /** - * Return true if child is an descendant of parent, (or equal to the parent). - */ - private boolean isViewDescendantOf(View child, View parent) { - if (child == parent) { - return true; - } - - final ViewParent theParent = child.getParent(); - return (theParent instanceof ViewGroup) && isViewDescendantOf((View) theParent, parent); - } - - /** - * Fling the scroll view - * - * @param velocityY The initial velocity in the Y direction. Positive - * numbers mean that the finger/curor is moving down the screen, - * which means we want to scroll towards the top. - */ - public void fling(int velocityX, int velocityY) { - if (getChildCount() > 0) { - int height = getHeight() - getPaddingBottom() - getPaddingTop(); - int bottom = getChildAt(0).getHeight(); - int width = getWidth() - getPaddingRight() - getPaddingLeft(); - int right = getChildAt(0).getWidth(); - - mScroller.fling(getScrollX(), getScrollY(), velocityX, velocityY, 0, right - width, 0, bottom - height); - - final boolean movingDown = velocityY > 0; - final boolean movingRight = velocityX > 0; - - View newFocused = findFocusableViewInMyBounds(movingRight, mScroller.getFinalX(), movingDown, mScroller.getFinalY(), findFocus()); - if (newFocused == null) { - newFocused = this; - } - - if (newFocused != findFocus() && newFocused.requestFocus(movingDown ? View.FOCUS_DOWN : View.FOCUS_UP)) { - mTwoDScrollViewMovedFocus = true; - mTwoDScrollViewMovedFocus = false; - } - - awakenScrollBars(mScroller.getDuration()); - invalidate(); - } - } - - /** - * {@inheritDoc} - * - *

This version also clamps the scrolling to the bounds of our child. - */ - public void scrollTo(int x, int y) { - // we rely on the fact the View.scrollBy calls scrollTo. - if (getChildCount() > 0) { - View child = getChildAt(0); - x = clamp(x, getWidth() - getPaddingRight() - getPaddingLeft(), child.getWidth()); - y = clamp(y, getHeight() - getPaddingBottom() - getPaddingTop(), child.getHeight()); - if (x != getScrollX() || y != getScrollY()) { - super.scrollTo(x, y); - } - } - } - - private int clamp(int n, int my, int child) { - if (my >= child || n < 0) { - /* my >= child is this case: - * |--------------- me ---------------| - * |------ child ------| - * or - * |--------------- me ---------------| - * |------ child ------| - * or - * |--------------- me ---------------| - * |------ child ------| - * - * n < 0 is this case: - * |------ me ------| - * |-------- child --------| - * |-- mScrollX --| - */ - return 0; - } - if ((my+n) > child) { - /* this case: - * |------ me ------| - * |------ child ------| - * |-- mScrollX --| - */ - return child-my; - } - return n; - } -} diff --git a/mainActivity/src/com/example/furt/myapplication/UndefinedFormula.java b/mainActivity/src/com/example/furt/myapplication/UndefinedFormula.java index 309cb4c..c5885a0 100755 --- a/mainActivity/src/com/example/furt/myapplication/UndefinedFormula.java +++ b/mainActivity/src/com/example/furt/myapplication/UndefinedFormula.java @@ -8,7 +8,7 @@ public class UndefinedFormula implements Formula{ Paint p=new Paint(); int priority; - boolean currentF; + boolean currentF; //indica se la formula è quella su cui sta lavorando il parser per l'inserimento di ipotesi UndefinedFormula() { priority=100; @@ -16,13 +16,13 @@ public class UndefinedFormula implements Formula{ } public String Draw(int x) { - if(currentF) + if(currentF) //la formula corrente visualizza un _ return "_"; else return " "; } public String toString(){return Draw(0);} - public String toStringDeleted(){return null;} //UndefinedFormula should never be deleted + public String toStringDeleted(){return null;} //UndefinedFormula non può essere scaricata public float size(){ p.setTextSize(DrawActivity.textSize); return p.measureText(toString()); @@ -30,11 +30,11 @@ public class UndefinedFormula implements Formula{ public float height() { return 0; - } + } //UndefinedFormula non ha dimensioni e non accetta regole public float sizeDeleted(){return(0);} public List introductionRules(){ return null; - } //UndefinedFormula accepts no rules + } public List EliminationRules(){ return null; } diff --git a/mainActivity/src/com/example/furt/myapplication/aggiorna.java b/mainActivity/src/com/example/furt/myapplication/aggiorna.java index a97220e..7ea276d 100755 --- a/mainActivity/src/com/example/furt/myapplication/aggiorna.java +++ b/mainActivity/src/com/example/furt/myapplication/aggiorna.java @@ -4,7 +4,6 @@ package com.example.furt.myapplication; import android.content.Context; import android.os.AsyncTask; import android.os.Environment; -import android.util.Log; import android.widget.Toast; import java.io.File; @@ -64,8 +63,7 @@ public class aggiorna { personalDBHelper connessione = new personalDBHelper(aggiornamento.t.getContext()); List esercizi=connessione.getElem(user); if(esercizi!=null && !esercizi.isEmpty()) { - for (listElem esercizio : esercizi) { - Log.e("",esercizio.getEsercizio());} + for (listElem esercizio : esercizi) { String richiesta = "8/" + sessionKey + "/" + esercizio.getEsercizio() + "/" + esercizio.getMd5() + "/" + esercizio.getTime() + "/" + esercizio.getClick(); String ritorno = serverComunication.connessione(richiesta); diff --git a/mainActivity/src/com/example/furt/myapplication/aggiornamento.java b/mainActivity/src/com/example/furt/myapplication/aggiornamento.java index c3893fe..ee114a9 100755 --- a/mainActivity/src/com/example/furt/myapplication/aggiornamento.java +++ b/mainActivity/src/com/example/furt/myapplication/aggiornamento.java @@ -3,7 +3,6 @@ package com.example.furt.myapplication; import android.app.Activity; import android.content.Intent; import android.os.Bundle; -import android.util.Log; import android.widget.RelativeLayout; @@ -24,7 +23,6 @@ public class aggiornamento extends Activity sessionKey = serverComunication.connessione("1/" + user + "/" + pass); if(sessionKey.contentEquals("request-login") || sessionKey.contains("err")) { - Log.e("", "ciao"); Intent i = new Intent(getApplicationContext(), mainActivity.class); i.putExtra("logout", "si"); i.addFlags(Intent.FLAG_ACTIVITY_NEW_TASK); diff --git a/mainActivity/src/com/example/furt/myapplication/askFormula.java b/mainActivity/src/com/example/furt/myapplication/askFormula.java index a6fb161..ca15a35 100755 --- a/mainActivity/src/com/example/furt/myapplication/askFormula.java +++ b/mainActivity/src/com/example/furt/myapplication/askFormula.java @@ -1,5 +1,8 @@ package com.example.furt.myapplication; +/** + * askFormula(): callback per ottenere informazioni aggiuntive sulla regola da applicare + */ public class askFormula{ public Formula Ask(){return DrawActivity.selectedNode.F;}; } diff --git a/mainActivity/src/com/example/furt/myapplication/download_page.java b/mainActivity/src/com/example/furt/myapplication/download_page.java index 1193815..4541b31 100755 --- a/mainActivity/src/com/example/furt/myapplication/download_page.java +++ b/mainActivity/src/com/example/furt/myapplication/download_page.java @@ -96,7 +96,13 @@ public class download_page extends Activity getMenuInflater().inflate(R.menu.menu_dow, menu); return true; } - + @Override + public void onBackPressed() { + Intent i = new Intent(getApplicationContext(), mainActivity.class); + i.putExtra("logout","si"); + i.addFlags(Intent.FLAG_ACTIVITY_NEW_TASK); + getApplicationContext().startActivity(i); + } @Override public boolean onOptionsItemSelected(MenuItem item) { @@ -104,6 +110,7 @@ public class download_page extends Activity // automatically handle clicks on the Home/Up button, so long // as you specify a parent activity in AndroidManifest.xml. int id = item.getItemId(); + if(id==R.id.aggiorna) { Intent i = new Intent(getApplicationContext(), aggiornamento.class); diff --git a/mainActivity/src/com/example/furt/myapplication/longnodeHandler.java b/mainActivity/src/com/example/furt/myapplication/longnodeHandler.java new file mode 100644 index 0000000..b17796d --- /dev/null +++ b/mainActivity/src/com/example/furt/myapplication/longnodeHandler.java @@ -0,0 +1,26 @@ +package com.example.furt.myapplication; + +import android.view.View; + +/**LongNodeHandler: handler per la pressione prolungata di un nodo**/ + +public class longnodeHandler implements View.OnLongClickListener { + Node n; //nodo a cui è legato questo handler + + longnodeHandler(Node node) { + n = node; + } + + @Override + public boolean onLongClick(View view) { + if (DrawActivity.selectedNode != null) + if (DrawActivity.selectedNode.view == view) { + if (DrawActivity.selectedNode.Children.size() == 0) { //se l'hold click è stato fatto sul selectedNode ed esso è un nodo foglia + touchnodeHandler.ruleDialog = new RuleDialog(DrawActivity.selectedNode.F.introductionRules()); + touchnodeHandler.ruleDialog.showAllRules=true; //nuovo ruleDialog con l'opzione showAllRules già settata + touchnodeHandler.ruleDialog.show(DrawActivity.fragmentManager, "CIAO"); + } + } + return true; + } +} diff --git a/mainActivity/src/com/example/furt/myapplication/mainActivity.java b/mainActivity/src/com/example/furt/myapplication/mainActivity.java index 1c68148..3f456a5 100755 --- a/mainActivity/src/com/example/furt/myapplication/mainActivity.java +++ b/mainActivity/src/com/example/furt/myapplication/mainActivity.java @@ -72,6 +72,8 @@ public class mainActivity extends Activity { i.addFlags(Intent.FLAG_ACTIVITY_NEW_TASK); getApplicationContext().startActivity(i);//avvio la "aggiornamento.class" } + else + Toast.makeText(getApplicationContext(),"credenziali errate", Toast.LENGTH_SHORT).show(); } } catch (Exception e) { e.printStackTrace(); diff --git a/mainActivity/src/com/example/furt/myapplication/parserDialog.java b/mainActivity/src/com/example/furt/myapplication/parserDialog.java index e871b7f..ccc18cc 100755 --- a/mainActivity/src/com/example/furt/myapplication/parserDialog.java +++ b/mainActivity/src/com/example/furt/myapplication/parserDialog.java @@ -5,13 +5,13 @@ import android.app.Dialog; import android.app.DialogFragment; import android.content.DialogInterface; import android.os.Bundle; -import android.util.Log; import android.view.LayoutInflater; import android.view.View; import android.view.ViewGroup; import android.widget.Button; import android.widget.RelativeLayout; import android.widget.TextView; +import android.widget.Toast; import java.util.ArrayList; import java.util.List; @@ -20,7 +20,6 @@ public class parserDialog extends DialogFragment { static Formula F=null; //formula che sto costruendo static RelativeLayout formulaLayout; static TextView FView; //View contenente la formula che sto visualizzando - static Button dismissButton; static boolean reload=false; static ArrayList esliter=new ArrayList(); static ArrayList undo=new ArrayList(); @@ -35,7 +34,6 @@ public class parserDialog extends DialogFragment { F.setCursor(); } esliter.addAll(parser.getLiteral(DrawActivity.nomeEs)); - Log.e("","⊤"); } @Override public Dialog onCreateDialog(final Bundle savedInstanceState) { @@ -110,24 +108,32 @@ public class parserDialog extends DialogFragment { public void onClick(DialogInterface dialog, int id) { if(!F.toString().contains("_")) { List L = F.EliminationRules(); - if (L.size()==0) + if (L.size()==0){ + F=null; + Toast.makeText(DrawActivity.rootNode.view.getContext(),"Impossibile scaricare questa ipotesi ora",Toast.LENGTH_LONG).show(); return; + } + if (F.toString().equals(DrawActivity.selectedNode.F.toString())) //sto provando a scaricare il nodo selezionato + { + Toast.makeText(DrawActivity.rootNode.view.getContext(),"Impossibile scaricare un nodo aperto senza dimostrarlo",Toast.LENGTH_LONG).show(); + F=null; + return; + } touchHPHandler t = new touchHPHandler(L.get(0).createNodes(null, new askFormula()),new Hypothesis(F,true)); F = null; t.discard=false; t.onClick(null); } - else + else{ + Toast.makeText(DrawActivity.rootNode.view.getContext(),"Completa l'inserimento!",Toast.LENGTH_SHORT).show(); reboot(); + } } }); builder.setNeutralButton("Undo", new DialogInterface.OnClickListener() { public void onClick(DialogInterface dialog, int id) { if(undo.size()>1) { F = undo.remove(undo.size() - 1); - /*for(int i=0;i { @Override @@ -105,21 +115,7 @@ public class serverComunication } } - public static String connessioneMain(String parametri) - { - try { - return new richiestaServerMain().execute(parametri).get(); - } catch (InterruptedException e) { - e.printStackTrace(); - } catch (ExecutionException e) { - e.printStackTrace(); - } - return null; - } - - - - static class richiestaServerMain extends AsyncTask { + public static class richiestaServerMain extends AsyncTask { @Override protected String doInBackground(String... params) { diff --git a/mainActivity/src/com/example/furt/myapplication/touchHPHandler.java b/mainActivity/src/com/example/furt/myapplication/touchHPHandler.java index 44691ce..0e62a53 100755 --- a/mainActivity/src/com/example/furt/myapplication/touchHPHandler.java +++ b/mainActivity/src/com/example/furt/myapplication/touchHPHandler.java @@ -1,10 +1,11 @@ package com.example.furt.myapplication; import android.view.View; +import android.widget.Toast; public class touchHPHandler implements View.OnClickListener { - Node L; + Node L; //nodo contenente il sottoalbero successivo all'eliminazione dell'ipotesi boolean discard; Hypothesis thisHP; //ipotesi che sto eliminando touchHPHandler(Node n,Hypothesis hp) @@ -15,13 +16,14 @@ public class touchHPHandler implements View.OnClickListener } public void onClick(View view) { - if (DrawActivity.selectedNode==null) //non-existent selectedNode (should never happen) + if (DrawActivity.selectedNode==null) //selectedNode non esiste (non dovrebbe mai succedere) return; - if (DrawActivity.selectedNode.Children.size()!=0) //not a leaf: can't add children + if (DrawActivity.selectedNode.Children.size()!=0) //non è una foglia: non si possono applicare regole. { + Toast.makeText(DrawActivity.rootNode.view.getContext(),"Impossibile scaricare ipotesi su nodi intermedi",Toast.LENGTH_LONG).show(); return; } - if (thisHP.HP.toString().equals(DrawActivity.selectedNode.F.toString())) //close current Node + if (thisHP.HP.toString().equals(DrawActivity.selectedNode.F.toString())) //sto scaricando una formula uguale al nodo corrente: lo chiudo aggiornando lo stato del nodo { if (thisHP.isDeleted) { if (DrawActivity.selectedNode.status == Node.OPEN) @@ -39,17 +41,21 @@ public class touchHPHandler implements View.OnClickListener DrawActivity.startDraw(); return; } - if (L==null) //incompatible elimination + if (L==null) //eliminazione incompatibile con il nodo attuale + { + Toast.makeText(DrawActivity.rootNode.view.getContext(),"Impossibile scaricare questa ipotesi ora",Toast.LENGTH_LONG).show(); return; - for (Node n:L.Children) { + } + for (Node n:L.Children) { //aggiungo al sottoalbero della regola da applicare tutte le ipotesi del selectedNode. In più aggiungo alle ipotesi introdotte da questa regola il fromNode corretto. for (Hypothesis hp:n.NodeHP) hp.fromNode= DrawActivity.selectedNode; //le ipotesi dei nuovi figli provengono dal nodo in cui stanno per essere inserite n.addHPList(DrawActivity.selectedNode.NodeHP); DrawActivity.selectedNode.addChild(n); } - DrawActivity.selectedNode.hasFocus=false; - DrawActivity.selectedNode.Children.get(0).hasFocus=true; - if(discard) { + DrawActivity.selectedNode.hasFocus=false; //il nodo su cui ho applicato la regola non è più una foglia e non ha più focus + DrawActivity.selectedNode.ruleName = L.ruleName; + DrawActivity.selectedNode.Children.get(0).hasFocus=true; //il primo figlio dell'applicazione della regola ha di default il focus + if(discard) { //sto scaricando un'ipotesi: il primo figlio è automaticamente chiuso if (thisHP.isDeleted) DrawActivity.selectedNode.Children.get(0).status = Node.CANCELED; else @@ -57,8 +63,6 @@ public class touchHPHandler implements View.OnClickListener } else DrawActivity.selectedNode.Children.get(0).status= Node.OPEN; - DrawActivity.selectedNode.hasFocus = false; - DrawActivity.selectedNode.ruleName = L.ruleName; DrawActivity.nmoves++; DrawActivity.rootNode.Clean(); DrawActivity.startDraw(); diff --git a/mainActivity/src/com/example/furt/myapplication/touchParserHandler.java b/mainActivity/src/com/example/furt/myapplication/touchParserHandler.java index 464cc09..655901f 100755 --- a/mainActivity/src/com/example/furt/myapplication/touchParserHandler.java +++ b/mainActivity/src/com/example/furt/myapplication/touchParserHandler.java @@ -2,6 +2,7 @@ package com.example.furt.myapplication; import android.view.View; import android.widget.TextView; +import android.widget.Toast; public class touchParserHandler implements View.OnClickListener { @@ -14,6 +15,11 @@ public class touchParserHandler implements View.OnClickListener } public void onClick(View view) { + if(!parserDialog.F.toString().contains("_")) + { + Toast.makeText(DrawActivity.rootNode.view.getContext(),"Formula completa! Premere \"Undo\" per modificare", Toast.LENGTH_SHORT).show(); + return; + } parserDialog.undo.add(parserDialog.F.duplicate()); parserDialog.formulaLayout.removeAllViews(); if(type==0) diff --git a/mainActivity/src/com/example/furt/myapplication/touchRuleHandler.java b/mainActivity/src/com/example/furt/myapplication/touchRuleHandler.java deleted file mode 100755 index 7443ebc..0000000 --- a/mainActivity/src/com/example/furt/myapplication/touchRuleHandler.java +++ /dev/null @@ -1,30 +0,0 @@ -package com.example.furt.myapplication; -import android.view.View; - -import java.util.List; - -public class touchRuleHandler implements View.OnClickListener -{ - List L; - touchRuleHandler(List list) - { - L=list; - } - public void onClick(View view) - { - if (DrawActivity.selectedNode.Children.size()!=0) //not a leaf: can't add children - return; - for (Node n:L) { - for (Hypothesis hp:n.NodeHP) - hp.fromNode= DrawActivity.selectedNode; //le ipotesi dei nuovi figli provengono dal nodo in cui stanno per essere inserite - n.addHPList(DrawActivity.selectedNode.NodeHP); - DrawActivity.selectedNode.addChild(n); - } - DrawActivity.selectedNode.hasFocus=false; - DrawActivity.selectedNode.ruleName=L.get(0).ruleName; - DrawActivity.selectedNode.Children.get(0).hasFocus=true; - DrawActivity.nmoves++; - DrawActivity.rootNode.Clean(); - DrawActivity.startDraw(); - } -} diff --git a/mainActivity/src/com/example/furt/myapplication/touchnodeHandler.java b/mainActivity/src/com/example/furt/myapplication/touchnodeHandler.java index 4fcb64d..002fb00 100755 --- a/mainActivity/src/com/example/furt/myapplication/touchnodeHandler.java +++ b/mainActivity/src/com/example/furt/myapplication/touchnodeHandler.java @@ -1,39 +1,39 @@ package com.example.furt.myapplication; import android.graphics.Color; +import android.graphics.Paint; import android.util.TypedValue; import android.view.View; import android.view.ViewGroup; import android.widget.Button; import android.widget.RelativeLayout; import android.widget.TextView; -import android.util.Log; -import android.graphics.Paint; import java.util.ArrayList; import java.util.List; public class touchnodeHandler implements View.OnClickListener { - - Node n; + static RuleDialog ruleDialog; //il ruleDialog da far comparire nel caso in cui l'utente voglia visualizzare le regole di introduzione disponibili + Node n; //nodo a cui è legato questo handler touchnodeHandler(Node node) { - n=node; + n=node; ruleDialog=null; } @Override public void onClick(View view) { + Paint p=new Paint(); + n.hasFocus=true; //il nodo cliccato ha il focus TextView v=(TextView)view; - v.setTextColor(Color.RED); + v.setTextColor(Color.RED); //colorazione rossa per il nodo if (DrawActivity.selectedNode!=null) - if (DrawActivity.selectedNode.view==view) { + if (DrawActivity.selectedNode.view==view) { //doppio clic sul nodo: parte il Dialog per le regole di introduzione if (DrawActivity.selectedNode.Children.size()==0){ List L=new ArrayList(); - for (IntroductionRule r: DrawActivity.selectedNode.F.introductionRules()) { - if (r.getPriority()!=0) + if (r.getPriority()!=0) //short click: aggiungo solo le regole a priorità alta L.add(r); } - if (L.size()==1) + if (L.size()==1) //c'è una sola regola: la applico immediatamente. { Node selectedRule=L.get(0).createNodes(new askFormula()); for (Node n : selectedRule.Children) { @@ -49,13 +49,15 @@ public class touchnodeHandler implements View.OnClickListener { DrawActivity.nmoves++; DrawActivity.rootNode.Clean(); DrawActivity.startDraw(); + return; } else { - RuleDialog ruleDialog = new RuleDialog(DrawActivity.selectedNode.F.introductionRules()); + //parte il ruleDialog + ruleDialog = new RuleDialog(DrawActivity.selectedNode.F.introductionRules()); ruleDialog.show(DrawActivity.fragmentManager, "CIAO"); } } - else + else //nodo intermedio: parte il Dialog per le operazioni di copia/cancella { CopyPasteDialog copyPasteDialog=new CopyPasteDialog(DrawActivity.selectedNode); copyPasteDialog.show(DrawActivity.fragmentManager,""); @@ -63,38 +65,18 @@ public class touchnodeHandler implements View.OnClickListener { return; } int i,size; - if (DrawActivity.selectedNode!=null) { + if (DrawActivity.selectedNode!=null) { //c'era già un selectedNode: lo ricoloro adeguatamente. if(DrawActivity.selectedNode.status==Node.OPEN || DrawActivity.selectedNode.status==Node.FAKE) DrawActivity.selectedNode.view.setTextColor(Color.BLACK); else DrawActivity.selectedNode.view.setTextColor(Color.GRAY); } DrawActivity.selectedNode = n; - DrawActivity.globalHP.removeAllViews(); - size = n.NodeHP.size(); - int leftID=0; - int headID=0; - float sum=0; - final Button elim=new Button(view.getContext()); - String newText = "Nuova"; - elim.setText(newText); - elim.setTextSize(TypedValue.COMPLEX_UNIT_SP,16); - elim.setId(DrawActivity.globalId++); - RelativeLayout.LayoutParams myP2=new RelativeLayout.LayoutParams(ViewGroup.LayoutParams.WRAP_CONTENT, ViewGroup.LayoutParams.WRAP_CONTENT); - elim.setLayoutParams(myP2); - elim.setOnClickListener(new View.OnClickListener() { - @Override - public void onClick(View v) { - parserDialog p=new parserDialog(); - p.show(DrawActivity.fragmentManager, ""); //parte l'editor per inserire nuove formule - } - }); - DrawActivity.globalHP.addView(elim); - Paint p = new Paint(); - p.setTextSize(DrawActivity.textSize); - float newSize=p.measureText(newText)+(float)(p.measureText(newText)*0.20) + 200; - sum+=newSize; - leftID=elim.getId(); + DrawActivity.globalHP.removeAllViews(); //rimuovo le eventuali vecchie ipotesi per mostrare quelle del nuovo selectedNode + size = n.NodeHP.size(); //numero di ipotesi + int leftID=0; //ID dell'eventuale ipotesi a destra della quale dev'essere posizionata l'ipotesi (0=assente) + int headID=0; //ID dell'eventuale ipotesi sotto la quale deve comparire l'ipotesi (0=assente) + float sum=0; //lunghezza raggiunta finora: se supera la larghezza dello schermo devo andare a capo for (i = 0; i(DrawActivity.v.widthPixels/1.5)) //ho superato la larghezza dello schermo: devo andare a capo + float thisSize; + p.setTextSize(30); + thisSize=p.measureText(newT.getText().toString()); //misuro la larghezza dell'ipotesi inserita + thisSize+=thisSize*0.2; //con un'approssimazione per eccesso del 20% + sum+=thisSize; //aggiungo alla somma totale la larghezza di questa ipotesi e della spaziatura + sum+=50; + if (sum>(DrawActivity.v.widthPixels+20)) //ho superato la larghezza dello schermo: devo andare a capo { - sum=n.NodeHP.get(i).HP.size(); - headID=leftID; + sum=thisSize; //il nuovo nodo è il primo della nuova riga + headID=leftID; //tutti gli altri devono stare sotto un nodo della riga precedente } else - myP.addRule(RelativeLayout.RIGHT_OF,leftID); + myP.addRule(RelativeLayout.RIGHT_OF,leftID); //non vado a capo: mi limito a posizionarmi a destra del leftID if (headID!=0) - myP.addRule(RelativeLayout.BELOW,headID); + myP.addRule(RelativeLayout.BELOW,headID); //mi posiziono sotto l'headID se esiste newT.setLayoutParams(myP); List R=n.NodeHP.get(i).HP.EliminationRules(); - if (R.size()!=0) { + if (R.size()!=0) { //ci sono regole di eliminazione per questa formula Node L= R.get(0).createNodes(null,new askFormula()); newT.setOnClickListener(new touchHPHandler(L,n.NodeHP.get(i))); } - else + else //setto comunuqe il listener nel caso in cui la formula venga scaricata newT.setOnClickListener(new touchHPHandler(null,n.NodeHP.get(i))); - newT.setOnLongClickListener(new LongHPClick(n.NodeHP.get(i).fromNode)); - leftID=newT.getId(); + newT.setOnLongClickListener(new LongHPClick(n.NodeHP.get(i).fromNode)); //setto un longclick listener che mostra il nodo da cui viene l'ipotesi + leftID=newT.getId(); //aggiorno il leftID DrawActivity.globalHP.addView(newT); } -/* + //disegno il bottone utilizzando lo stesso algoritmo utilizzato per le ipotesi + final Button elim=new Button(view.getContext()); RelativeLayout.LayoutParams myP=new RelativeLayout.LayoutParams(ViewGroup.LayoutParams.WRAP_CONTENT, ViewGroup.LayoutParams.WRAP_CONTENT); - elim.setText("Nuova"); + elim.setText("Nuova..."); elim.setTextSize(TypedValue.COMPLEX_UNIT_SP,16); elim.setId(DrawActivity.globalId++); myP.setMargins(50,0,0,0); - sum+=elim.getWidth(); + p.setTextSize(16); + float buttonSize=p.measureText("Nuova..."); + sum+=buttonSize; if (sum>(DrawActivity.v.widthPixels/1.5)) //ho superato la larghezza dello schermo: devo andare a capo { - sum=n.NodeHP.get(i).HP.size(); headID=leftID; } else @@ -151,7 +142,7 @@ public class touchnodeHandler implements View.OnClickListener { } }); DrawActivity.globalHP.addView(elim); -*/ - } } + + -- 2.39.2