Dominoes on Acid Code

/* Copyright (C) 2002 Matthias S. Benkmann <m.s.b@gmx.net>

This program is free software; you can redistribute it and/or
modify it under the terms of the GNU General Public License
as published by the Free Software Foundation; version 2
of the License (ONLY THIS VERSION).

This program is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
GNU General Public License for more details.

You should have received a copy of the GNU General Public License
along with this program; if not, write to the Free Software
Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA  02111-1307, USA.
*/

package domino.ui;

import java.util.Collection;
import java.util.LinkedList;
import java.util.Iterator;
import java.util.Vector;
import java.util.HashMap;

import java.io.File;
import java.io.FileWriter;
import java.io.FileOutputStream;
import java.io.BufferedReader;
import java.io.InputStreamReader;
import java.io.InputStream;
import java.io.IOException;

import java.net.URL;
import java.net.URLConnection;

import javax.swing.*;
import javax.swing.filechooser.FileFilter;
import javax.swing.text.*;
import java.awt.event.*;
import javax.swing.event.MouseInputAdapter;
import javax.swing.event.HyperlinkListener;
import javax.swing.event.HyperlinkEvent;
import java.awt.*;
import java.awt.geom.Point2D;

import domino.core.Debugging;
import domino.core.LevelManager;
import domino.core.Version;

import domino.logic.FormulaDominoTree;
import domino.logic.FormulaDominoSquare;
import domino.logic.DominoTree;
import domino.logic.ProofFormatter;

public class UITest extends JApplet
{
  private final URL DEFAULT_TILES_URL=this.getClass().getClassLoader().getResource("domino/core/tiles.tiles");
  private final URL LEVELS_URL=this.getClass().getClassLoader().getResource("domino/core/levels.txt");
  private final URL COMPLETE_MANUAL_URL=this.getClass().getClassLoader().getResource("domino/doc/manual.html");
  private final URL SHORT_REFERENCE_MANUAL_URL=this.getClass().getClassLoader().getResource("domino/doc/shortref.html");
  private final URL WALKTHROUGH_MANUAL_URL=this.getClass().getClassLoader().getResource("domino/doc/walkthrough.html");
  
  private final static int COMPLETE_MANUAL=0;
  private final static int SHORT_REFERENCE_MANUAL=1;
  private final static int WALKTHROUGH_MANUAL=2;
  private final URL[] MANUAL_URL={COMPLETE_MANUAL_URL, SHORT_REFERENCE_MANUAL_URL, WALKTHROUGH_MANUAL_URL};
  
  private final static int WORLD_XDIM=20;
  private final static int WORLD_YDIM=20;
  private final static int WORLD_SQUARESIZE=32; //24; // 24 for generating documentation pics
  private final static int BORING_ELONGATOR_INDEX=3;
  
  private boolean runningAsApplet=false;
  private boolean firstStart;
  private IsoWorld myIsoWorld;
  
  private MouseEventProcessor myMouseEventProcessor;
  private DominoTile startTile;
  private JFileChooser saveProofChooser;
  private JFileChooser loadSaveTileChooser;
  private Dimension screenSize;
  
  private String currentLevel;
  private LevelManager myLevelManager;
  private TileProducerManager myTileProducerManager;
  
  private Component myRootComponent;
  private RootPaneContainer myRootPaneContainer;
  private JFrame proofFrame=null;
  private JFrame manualFrame=null;
  private JEditorPane manualEditorPane=null;
  
  private JCheckBoxMenuItem autoSimplifyMenuItem=new JCheckBoxMenuItem("Auto-Simplify",true);
  private JMenu tileMenu;
  
  public static void main(String[] args)
  {
    JFrame myFrame=new JFrame("Domino");

    myFrame.addWindowListener
    (   new WindowAdapter() 
        {
          public void windowClosing(WindowEvent e)  { System.exit(0); }
        }
    );
    
    UITest myUI=new UITest();
    myUI.myRootPaneContainer=myFrame;
    myUI.doInit();
    
    myFrame.pack();
    myFrame.setVisible(true);
    
    myUI.start();
  };
  
  public void init()
  {
    runningAsApplet=true;
    myRootPaneContainer=this;
    doInit();
  };

  public void doInit()
  {
/*    Thread foo=new Thread()
    {
      public void run()
      {
        JEditorPane manualEditorPane;
    try{
      manualEditorPane=new JEditorPane(MANUAL_URL);
    }catch(Exception x){System.err.println(x.toString());};  
    manualEditorPane=null;
      }
    };
    foo.setDaemon(true);
    foo.start();*/
    
    myRootComponent=(Component)myRootPaneContainer;
    
    myIsoWorld=new IsoWorld(WORLD_XDIM,WORLD_XDIM,WORLD_YDIM,WORLD_YDIM,WORLD_SQUARESIZE,-0.16,-0.16);
    myRootPaneContainer.setContentPane(myIsoWorld.graphicalRepresentation());
    try{
      screenSize=java.awt.Toolkit.getDefaultToolkit().getScreenSize();
    }catch(Exception x) {screenSize=new Dimension(640,480);};
    
    myIsoWorld.graphicalRepresentation().setPreferredSize(new Dimension(Math.min(900,screenSize.width),Math.min(700,screenSize.height)));
    
    myRootComponent=myRootPaneContainer.getContentPane();
    
    
    myTileProducerManager=new TileProducerManager(BORING_ELONGATOR_INDEX, "Boring Elongator: X0,X0");
    //myTileProducerManager.enableCheating();
    
    myLevelManager=new LevelManager(LEVELS_URL);
    
    
    currentLevel=myLevelManager.getLevel(0);
    if (currentLevel==null) currentLevel="((A->_|_)->_|_)->A";
    createStartTileForLevel(currentLevel);
    
    myIsoWorld.addObject(startTile,new IsoLocation(0,0,0),new IsoShift(0.0,0.0,0.0));
    
    fixWorldSizeForStartTile();
    
    
    
    myMouseEventProcessor=new MouseEventProcessor(myIsoWorld,myTileProducerManager,startTile,new Victory());
    
    Container cont=(Container)myRootComponent;
    while (cont!=null && !(cont instanceof Window)) cont=cont.getParent();
    if (cont!=null) ((Window)cont).addWindowListener(new WindowAdapter()
      { public void windowActivated(WindowEvent e)
        { myIsoWorld.graphicalRepresentation().requestFocus(); }; } );
    

    if (!runningAsApplet)
    {
      saveProofChooser=new JFileChooser();
      saveProofChooser.setDialogTitle("Save Proof");
      FileFilter txtFileFilter=new TxtFileFilter(new String[]{".txt",".proof"});
      saveProofChooser.addChoosableFileFilter(txtFileFilter);
      saveProofChooser.setFileFilter(txtFileFilter);
      
      loadSaveTileChooser=new JFileChooser();
      txtFileFilter=new TxtFileFilter(new String[]{".tiles"});
      loadSaveTileChooser.addChoosableFileFilter(txtFileFilter);
      loadSaveTileChooser.setFileFilter(txtFileFilter);
    };  
    
    

    firstStart=true;
    
    /*
      Create the menu bar and menus
    */
    JMenuBar myMenuBar=new JMenuBar();
    myRootPaneContainer.getRootPane().setJMenuBar(myMenuBar);
    //=====================================
    JMenu myFileMenu=new JMenu("File");
    myFileMenu.setMnemonic(KeyEvent.VK_F);
    myMenuBar.add(myFileMenu);
    
    //------------------
    JMenuItem myMenuItem=new JMenuItem("Show Proof",KeyEvent.VK_S);
    myMenuItem.setAccelerator(KeyStroke.getKeyStroke(
                                            KeyEvent.VK_S, InputEvent.CTRL_MASK));
    myFileMenu.add(myMenuItem);
    myMenuItem.addActionListener
    ( new ActionListener()
      {
        public void actionPerformed(ActionEvent e) { showProof(); };
      }
    );
    //------------------
    if (!runningAsApplet)
    {
      myMenuItem=new JMenuItem("Quit",KeyEvent.VK_Q);
      myMenuItem.setAccelerator(KeyStroke.getKeyStroke(
                                              KeyEvent.VK_Q, InputEvent.CTRL_MASK));
      myFileMenu.add(myMenuItem);
      myMenuItem.addActionListener
      ( new ActionListener()
        {
          public void actionPerformed(ActionEvent e)  { System.exit(0); };
        }
      );
    };  
    
    
    //====================================
    JMenu myLevelMenu=new JMenu("Level");
    myLevelMenu.setMnemonic(KeyEvent.VK_L);
    myMenuBar.add(myLevelMenu);
    //-----------------------
    myMenuItem=new JMenuItem("About",KeyEvent.VK_A);
    myMenuItem.setAccelerator(KeyStroke.getKeyStroke(
                                            KeyEvent.VK_A, InputEvent.CTRL_MASK));
    myLevelMenu.add(myMenuItem);
    myMenuItem.addActionListener
    ( new ActionListener()
      {
        public void actionPerformed(ActionEvent e) { aboutLevel(); };
      }
    );
    //-----------------------
    myMenuItem=new JMenuItem("Restart",KeyEvent.VK_R);
    myMenuItem.setAccelerator(KeyStroke.getKeyStroke(
                                            KeyEvent.VK_R, InputEvent.CTRL_MASK));
    myLevelMenu.add(myMenuItem);
    myMenuItem.addActionListener
    ( new ActionListener()
      {
        public void actionPerformed(ActionEvent e) { restartLevel(); };
      }
    );
    //-----------------------
    myMenuItem=new JMenuItem("Advance",KeyEvent.VK_D);
    myLevelMenu.add(myMenuItem);
    myMenuItem.addActionListener
    ( new ActionListener()
      {
        public void actionPerformed(ActionEvent e) { nextLevel(); };
      }
    );
    //-----------------------
    myMenuItem=new JMenuItem("Select New",KeyEvent.VK_N);
    myMenuItem.setAccelerator(KeyStroke.getKeyStroke(
                                            KeyEvent.VK_N, InputEvent.CTRL_MASK));
    myLevelMenu.add(myMenuItem);
    myMenuItem.addActionListener
    ( new ActionListener()
      {
        public void actionPerformed(ActionEvent e) { newLevel(); };
      }
    );
    //------------------------------------------------
    myLevelMenu.addSeparator();
    autoSimplifyMenuItem.setMnemonic(KeyEvent.VK_U);
    myLevelMenu.add(autoSimplifyMenuItem);
    
    
    //====================================
    tileMenu=new JMenu("Tile");
    tileMenu.setMnemonic(KeyEvent.VK_T);
    myMenuBar.add(tileMenu);
    //-----------------------
    myMenuItem=new JMenuItem("Add Custom Tile",KeyEvent.VK_A);
    tileMenu.add(myMenuItem);
    myMenuItem.addActionListener
    ( new ActionListener()
      {
        public void actionPerformed(ActionEvent e) { addCustomTileToMenu(); };
      }
    );
    //------------------------------------------------
    
    if (!runningAsApplet)
    {
      tileMenu.addSeparator();
      //-----------------------
      myMenuItem=new JMenuItem("Load Tiles",KeyEvent.VK_L);
      tileMenu.add(myMenuItem);
      myMenuItem.addActionListener
      ( new ActionListener()
        {
          public void actionPerformed(ActionEvent e) { loadTiles(); };
        }
      );
      //-----------------------
      myMenuItem=new JMenuItem("Save Tiles",KeyEvent.VK_S);
      tileMenu.add(myMenuItem);
      myMenuItem.addActionListener
      ( new ActionListener()
        {
          public void actionPerformed(ActionEvent e) { saveTiles(); };
        }
      );
    };  
    //------------------------------------------------
    tileMenu.addSeparator();
    //-----------------------
    myMenuItem=new JMenuItem("Remove Unselected");
    tileMenu.add(myMenuItem);
    myMenuItem.addActionListener
    ( new ActionListener()
      {
        public void actionPerformed(ActionEvent e) 
        { 
          myTileProducerManager.removeDisabledProducers(); 
          myTileProducerManager.updateMenu(tileMenu);
        };
      }
    );
    //-----------------------
    myMenuItem=new JMenuItem("Restore Default");
    tileMenu.add(myMenuItem);
    myMenuItem.addActionListener
    ( new ActionListener()
      {
        public void actionPerformed(ActionEvent e) { loadTiles(DEFAULT_TILES_URL); };
      }
    );
    //------------------------------------------------
    tileMenu.addSeparator();
    loadTiles(DEFAULT_TILES_URL);
    
    
    //====================================
    JMenu myHelpMenu=new JMenu("Help");
    myHelpMenu.setMnemonic(KeyEvent.VK_H);
    myMenuBar.add(myHelpMenu);
    //-----------------------
    myMenuItem=new JMenuItem("Short Reference",KeyEvent.VK_S);
    myMenuItem.setAccelerator(KeyStroke.getKeyStroke(
                                            KeyEvent.VK_F1, 0));
    myHelpMenu.add(myMenuItem);
    myMenuItem.addActionListener
    ( new ActionListener()
      {
        public void actionPerformed(ActionEvent e) { showManual(SHORT_REFERENCE_MANUAL); };
      }
    );
    //-----------------------
    myMenuItem=new JMenuItem("Walkthrough",KeyEvent.VK_W);
    myHelpMenu.add(myMenuItem);
    myMenuItem.addActionListener
    ( new ActionListener()
      {
        public void actionPerformed(ActionEvent e) { showManual(WALKTHROUGH_MANUAL); };
      }
    );
    //-----------------------
    myMenuItem=new JMenuItem("Complete Manual",KeyEvent.VK_M);
    myMenuItem.setAccelerator(KeyStroke.getKeyStroke(
                                            KeyEvent.VK_F1, InputEvent.CTRL_MASK));
    myHelpMenu.add(myMenuItem);
    myMenuItem.addActionListener
    ( new ActionListener()
      {
        public void actionPerformed(ActionEvent e) { showManual(COMPLETE_MANUAL); };
      }
    );
    //-----------------------
    myMenuItem=new JMenuItem("About",KeyEvent.VK_A);
    myHelpMenu.add(myMenuItem);
    myMenuItem.addActionListener
    ( new ActionListener()
      {
        public void actionPerformed(ActionEvent e) { aboutGame(); };
      }
    );
    
  };
  
  public void start()
  {
    if (firstStart)
    SwingUtilities.invokeLater(new Runnable()
    {
      public void run() { focusOnStartTile(); }
    });
    firstStart=false;
  };
  
  public void stop(){};  
  public void destroy(){};
  
  
  protected void focusOnStartTile()
  {
    JIsoWorld myJIsoWorld=myIsoWorld.graphicalRepresentation();
    Dimension d=myJIsoWorld.getViewport().getExtentSize();
    Point viewportCenter=new Point(d.width>>1,d.height>>1);
    myIsoWorld.setSquareSize(WORLD_SQUARESIZE,0.5,0.6,viewportCenter.x,viewportCenter.y);
    myIsoWorld.graphicalRepresentation().requestFocus();
  };
  
  protected void newLevel()
  {
    String level;
    do{
      level=JOptionPane.showInputDialog(myRootComponent,
                                        "Enter a level number (1-"+myLevelManager.numberOfLevels()+")\nor an infix formula",
                                        "Start New Level",
                                        JOptionPane.QUESTION_MESSAGE);
      if (level==null) return;

      try{
        int lnum=Integer.parseInt(level.trim())-1; //-1 because LevelManager starts count at 0
        String newLevel=myLevelManager.getLevel(lnum);
        if (newLevel!=null) level=newLevel;
      }catch(Exception x){};  
    }while(!createStartTileForLevel(level));  
    
    currentLevel=level;
    restartLevelWithoutConfirmation();
  };
  
  protected void nextLevel()
  {
    int lnum=myLevelManager.getLevelNumberFor(currentLevel);
    if (lnum<0) lnum=0;
    ++lnum;
    if (lnum>=myLevelManager.numberOfLevels()) lnum=0;
    
    String level=myLevelManager.getLevel(lnum);
    if (level==null) level=currentLevel;
    
    currentLevel=level;
    restartLevelWithoutConfirmation();
  };
  
  protected void restartLevel()
  {
    int retval=JOptionPane.showConfirmDialog(myRootComponent,
                                             "Restart level?",
                                             "Restart level?",
                                             JOptionPane.YES_NO_OPTION,
                                             JOptionPane.QUESTION_MESSAGE);
    if (retval!=JOptionPane.YES_OPTION) return;

    restartLevelWithoutConfirmation();
  };
  
  
  protected void fixWorldSizeForStartTile()
  {
    Iterator i=startTile.blocksIterator();
    IsoLocation minloc=new IsoLocation(-WORLD_XDIM/2,-WORLD_YDIM/2,0);
    IsoLocation maxloc=new IsoLocation(WORLD_XDIM/2,WORLD_YDIM/2,0);
    while (i.hasNext())
    {
      IsoLocation loc=((IsoBlock)i.next()).getAbsoluteLocation();
      if (loc.x<minloc.x) minloc.x=loc.x;
      if (loc.x>maxloc.x) maxloc.x=loc.x;
      if (loc.y<minloc.y) minloc.y=loc.y;
      if (loc.y>maxloc.y) maxloc.y=loc.y;
    };
    minloc.x-=WORLD_XDIM/2;
    minloc.y-=WORLD_YDIM/2;
    maxloc.x+=WORLD_XDIM/2;
    maxloc.y+=WORLD_YDIM/2;
    int worldXdim=-minloc.x;
    if (worldXdim<maxloc.x) worldXdim=maxloc.x;
    int worldYdim=-minloc.y;
    if (worldYdim<maxloc.y) worldYdim=maxloc.y;
    myIsoWorld.addLines(0,worldXdim-myIsoWorld.minusXDim());
    myIsoWorld.addLines(1,worldXdim-myIsoWorld.plusXDim());
    myIsoWorld.addLines(2,worldYdim-myIsoWorld.minusYDim());
    myIsoWorld.addLines(3,worldYdim-myIsoWorld.plusYDim());
  };
  
  protected void restartLevelWithoutConfirmation()
  {  
    createStartTileForLevel(currentLevel);
    myIsoWorld.removeAllIsoObjects();
    DominoTile.removeIdAssignmentsForAllTiles();
    myIsoWorld.addObject(startTile,new IsoLocation(0,0,0),new IsoShift(0.0,0.0,0.0));
    myMouseEventProcessor.reset(startTile);
    fixWorldSizeForStartTile();
    focusOnStartTile();
  };
  
  protected void aboutLevel()
  {
    int lnum=myLevelManager.getLevelNumberFor(currentLevel)+1; //+1 because we want to number from 1
    String level= (lnum==0 ? "Custom Level" : ("Level "+lnum+" of "+myLevelManager.numberOfLevels()));
    level=level+"\n"+currentLevel;
    JOptionPane.showMessageDialog(myRootComponent,level,"About this level",
                                  JOptionPane.INFORMATION_MESSAGE);
  };
  
  protected void aboutGame()
  {
    JOptionPane.showMessageDialog(myRootComponent,
                         "Domino Version "+Version.VERSION+"\n"+
                         "Copyright (c) 2002,2003 Matthias S. Benkmann\n"+
                         "\n"+
                         "Send bug reports and comments to <matthias@winterdrache.de>\n"+
                         "The most recent version can be found at\nhttp://www.winterdrache.de/freeware/domino/index.html",
                         "Game Information",
                         JOptionPane.INFORMATION_MESSAGE);
  };
  
  
  protected void addCustomTileToMenu()
  {
    String name=JOptionPane.showInputDialog(myRootComponent,
                                        "Enter a name for the new tile",
                                        "Custom Tile",
                                        JOptionPane.QUESTION_MESSAGE);
    if (name==null) return;
    myTileProducerManager.extraProducerToRegularProducerIfPossible(name);
    myTileProducerManager.updateMenu(tileMenu);
  };

  protected void loadTiles()
  {
    loadSaveTileChooser.setDialogTitle("Load Tiles");
    int retval=loadSaveTileChooser.showOpenDialog(myRootComponent);
    if (retval==JFileChooser.APPROVE_OPTION)
    {
      try{
        URL fileURL=loadSaveTileChooser.getSelectedFile().toURL();
        loadTiles(fileURL);
      }catch(Exception x) {JOptionPane.showMessageDialog(myRootComponent,"File error: "+x.getMessage(),"File error",JOptionPane.ERROR_MESSAGE);
                           return;};
    };
  };
  
  protected void loadTiles(URL tileFile)
  {
    InputStream instream=null;
    
    try{
      URLConnection ucon=tileFile.openConnection();
      ucon.setDoInput(true);
      ucon.setDoOutput(false);
      //ucon.connect(); should be done implicitly by getInputStream()
      instream=ucon.getInputStream();
      BufferedReader in=new BufferedReader(new InputStreamReader(instream));
    
      TileProducerManager newTileProducerManager=new TileProducerManager(myTileProducerManager);
      newTileProducerManager.removeAllProducers(); //redundant because TileProducerManager(TileProducerManager) is not a true copy constructor, however it might become one in the future
    
      String line;
      while((line=in.readLine())!=null)
      {
        line=line.trim();
        if (line=="") continue;
        newTileProducerManager.addProducerForStringRepresentation(line);
      };  
      instream.close();

      myTileProducerManager=newTileProducerManager; 
      myMouseEventProcessor.setProducerManager(myTileProducerManager);
      myTileProducerManager.updateMenu(tileMenu); 
      myTileProducerManager.activateFirstEnabledProducer();
    }
    catch(Exception x)
    {
      JOptionPane.showMessageDialog(myRootComponent,
                                    "File error: "+x.getMessage(),
                                    "File error",
                                    JOptionPane.ERROR_MESSAGE);
      try{if (instream!=null) instream.close();}catch(Exception y){};
      return;
    };
  };
  
  protected void saveTiles()
  {
    loadSaveTileChooser.setDialogTitle("Save Tiles");
    int retval=loadSaveTileChooser.showSaveDialog(myRootComponent);
    if (retval==JFileChooser.APPROVE_OPTION)
    {
      File file=loadSaveTileChooser.getSelectedFile();
      if (file.exists())
      {
        retval=JOptionPane.showConfirmDialog(myRootComponent,
                                             file+" exists!\nOverwrite?",
                                             "Overwrite?",
                                             JOptionPane.YES_NO_OPTION,
                                             JOptionPane.WARNING_MESSAGE);
        if (retval!=JOptionPane.YES_OPTION) return;
      };
      
      FileWriter out=null;
      try{
        out=new FileWriter(file);
        for (int i=0; i<myTileProducerManager.numberOfProducers()-1; ++i)
          if (i!=BORING_ELONGATOR_INDEX) 
            out.write(myTileProducerManager.getStringRepresentationForProducer(i)+"\n");
            
        if (myTileProducerManager.numberOfProducers()-1>BORING_ELONGATOR_INDEX) 
            out.write(myTileProducerManager.getStringRepresentationForProducer(myTileProducerManager.numberOfProducers()-1)+"\n");    
        out.close();
      }
      catch(Exception x)
      {
        JOptionPane.showMessageDialog(myRootComponent,
                                      "File error: "+x.getMessage(),
                                      "File error",
                                      JOptionPane.ERROR_MESSAGE);
        try{out.close();}catch(Exception y){};
        return;
      };
    };
  };
  
    
  
  protected void prepareManualFrame()
  {
    manualFrame=new JFrame("Domino Documentation");
    manualFrame.setDefaultCloseOperation(JFrame.HIDE_ON_CLOSE);
    
    Container myContentPane=manualFrame.getContentPane();
    
    /*
      Create the menu bar and menus
    */
    JMenuBar myMenuBar=new JMenuBar();
    manualFrame.getRootPane().setJMenuBar(myMenuBar);
    //=====================================
    JMenu myFileMenu=new JMenu("File");
    myFileMenu.setMnemonic(KeyEvent.VK_F);
    myMenuBar.add(myFileMenu);
    
    //------------------
    JMenuItem myMenuItem;
    
    myMenuItem=new JMenuItem("Close Window",KeyEvent.VK_C);
    myMenuItem.setAccelerator(KeyStroke.getKeyStroke(
                                            KeyEvent.VK_W, InputEvent.CTRL_MASK));
    myFileMenu.add(myMenuItem);
    myMenuItem.addActionListener
    ( new ActionListener()
      {
        public void actionPerformed(ActionEvent e)  { manualFrame.setVisible(false);};
      }
    );
    
    manualEditorPane=new JEditorPane();
    
    manualEditorPane.setEditable(false);
    manualEditorPane.addHyperlinkListener
    (
      new HyperlinkListener()
      {
        public void hyperlinkUpdate(HyperlinkEvent e)
        {
          if (e.getEventType()==HyperlinkEvent.EventType.ACTIVATED)
          {
            try{
              manualEditorPane.setPage(e.getURL());
            }
            catch(IOException x){};
          };
        };
      }
    );
    
    JScrollPane manualScrollPane=new JScrollPane(manualEditorPane);
    manualScrollPane.setPreferredSize(new Dimension(Math.min(800,screenSize.width),Math.min(700,screenSize.height)));
    myContentPane.add(manualScrollPane);
    manualFrame.pack();
    manualEditorPane.revalidate();
  };
  
  protected void showManual(int manualId)
  {
    if (manualFrame==null) prepareManualFrame();
    manualFrame.setVisible(true);
    Cursor oldCursor1=manualFrame.getCursor();
    Cursor oldCursor2=myRootComponent.getCursor();
    manualFrame.setCursor(Cursor.getPredefinedCursor(Cursor.WAIT_CURSOR));
    myRootComponent.setCursor(Cursor.getPredefinedCursor(Cursor.WAIT_CURSOR));
    
    try{
      manualEditorPane.setPage(MANUAL_URL[manualId]);
    }catch(Exception x)
    {
      JOptionPane.showMessageDialog(myRootComponent,
                                    "Error: "+x.getMessage(),
                                    "Error",
                                    JOptionPane.ERROR_MESSAGE);
      manualFrame.setVisible(false);
      manualFrame.setCursor(oldCursor1);
      myRootComponent.setCursor(oldCursor2);
      return;
    };  

    manualFrame.setState(Frame.NORMAL);
    manualFrame.toFront();
    manualFrame.requestFocus();
    manualFrame.setCursor(oldCursor1);
    myRootComponent.setCursor(oldCursor2);

/*    JEditorPane manualEditorPane;
    try{
      manualEditorPane=new JEditorPane(MANUAL_URL);
    }catch(IOException x)
    {
      JOptionPane.showMessageDialog(myRootComponent,
                                    "Error: "+x.getMessage(),
                                    "Error",
                                    JOptionPane.ERROR_MESSAGE);
      return;
    };
    manualEditorPane.setEditable(false);
    JScrollPane manualScrollPane=new JScrollPane(manualEditorPane);
  
    myContentPane.remove(loading);
    myContentPane.add(manualScrollPane);*/
//    manualFrame.pack();
    //manualFrame.setVisible(true);
  };  
    

  
  protected class NoWrapEditorKit extends DefaultEditorKit 
  {
    private ViewFactory vf = null;

    public ViewFactory getViewFactory() 
    {
      if (vf == null) vf=new NoWrapFactory();
      return vf;
    };

    protected class NoWrapFactory implements ViewFactory 
    {
      public View create(Element e) 
      {
        return new PlainView(e);
      };
    };
  };
  
  protected void showProof()
  {
    if (proofFrame!=null && proofFrame.isShowing()) { proofFrame.setVisible(false); proofFrame.dispose();};
    proofFrame=new JFrame("Proof");
    proofFrame.setDefaultCloseOperation(JFrame.DISPOSE_ON_CLOSE);
    
    final Container myContentPane=proofFrame.getContentPane();
    
    String[] diag=ProofFormatter.naturalDeductionDiagram(startTile.rootTree());
    for (int i=1; i<diag.length; ++i) {diag[0]=diag[0]+"\n"+diag[i]; diag[i]=null;};
    final JEditorPane proofEditorPane=new JEditorPane("text/plain","");
    proofEditorPane.setEditorKit(new NoWrapEditorKit());
    proofEditorPane.setText(diag[0]);
    proofEditorPane.setFont(new Font("Monospaced",Font.PLAIN,proofEditorPane.getFont().getSize()+2));
    JScrollPane proofScrollPane=new JScrollPane(proofEditorPane);
    
    /*
      Create the menu bar and menus
    */
    JMenuBar myMenuBar=new JMenuBar();
    proofFrame.getRootPane().setJMenuBar(myMenuBar);
    //=====================================
    JMenu myFileMenu=new JMenu("File");
    myFileMenu.setMnemonic(KeyEvent.VK_F);
    myMenuBar.add(myFileMenu);
    
    //------------------
    JMenuItem myMenuItem;
    
    if (!runningAsApplet)
    {
      myMenuItem=new JMenuItem("Save As...",KeyEvent.VK_S);
      myMenuItem.setAccelerator(KeyStroke.getKeyStroke(
                                              KeyEvent.VK_S, InputEvent.CTRL_MASK));
      myFileMenu.add(myMenuItem);
      myMenuItem.addActionListener
      ( new ActionListener()
        {
          public void actionPerformed(ActionEvent e)  { saveJTextComponent(myContentPane,proofEditorPane); };
        }
      );
    };  
    //------------------
    myMenuItem=new JMenuItem("Close Window",KeyEvent.VK_C);
    myMenuItem.setAccelerator(KeyStroke.getKeyStroke(
                                            KeyEvent.VK_W, InputEvent.CTRL_MASK));
    myFileMenu.add(myMenuItem);
    myMenuItem.addActionListener
    ( new ActionListener()
      {
        public void actionPerformed(ActionEvent e)  { proofFrame.setVisible(false); proofFrame.dispose(); };
      }
    );
    
    JMenu myEditMenu=new JMenu("Edit");
    myEditMenu.setMnemonic(KeyEvent.VK_E);
    myMenuBar.add(myEditMenu);
    
    //------------------
    myMenuItem=new JMenuItem("Cut",KeyEvent.VK_T);
    myMenuItem.setAccelerator(KeyStroke.getKeyStroke(
                                              KeyEvent.VK_X, InputEvent.CTRL_MASK));
    myEditMenu.add(myMenuItem);
    myMenuItem.addActionListener
    ( new ActionListener()
      {
        public void actionPerformed(ActionEvent e)  { proofEditorPane.cut(); };
      }
    );
    //------------------
    myMenuItem=new JMenuItem("Copy",KeyEvent.VK_C);
    myMenuItem.setAccelerator(KeyStroke.getKeyStroke(
                                              KeyEvent.VK_C, InputEvent.CTRL_MASK));
    myEditMenu.add(myMenuItem);
    myMenuItem.addActionListener
    ( new ActionListener()
      {
        public void actionPerformed(ActionEvent e)  { proofEditorPane.copy(); };
      }
    );
    //------------------
    myMenuItem=new JMenuItem("Paste",KeyEvent.VK_P);
    myMenuItem.setAccelerator(KeyStroke.getKeyStroke(
                                              KeyEvent.VK_V, InputEvent.CTRL_MASK));
    myEditMenu.add(myMenuItem);
    myMenuItem.addActionListener
    ( new ActionListener()
      {
        public void actionPerformed(ActionEvent e)  { proofEditorPane.paste(); };
      }
    );
    //------------------
    myMenuItem=new JMenuItem("Select All",KeyEvent.VK_A);
    myMenuItem.setAccelerator(KeyStroke.getKeyStroke(
                                              KeyEvent.VK_A, InputEvent.CTRL_MASK));
    myEditMenu.add(myMenuItem);
    myMenuItem.addActionListener
    ( new ActionListener()
      {
        public void actionPerformed(ActionEvent e)  
        { 
          proofEditorPane.selectAll(); 
          proofEditorPane.getCaret().setSelectionVisible(true);
        };
      }
    );
    
    
    myContentPane.add(proofScrollPane);
    proofFrame.pack();
    proofFrame.setVisible(true);
       
    return;
  };
  
  protected void saveJTextComponent(Component myRootComponent,JTextComponent text)
  {
    int retval=saveProofChooser.showSaveDialog(myRootComponent);
    if (retval==JFileChooser.APPROVE_OPTION)
    {
      File file=saveProofChooser.getSelectedFile();
      if (file.exists())
      {
        retval=JOptionPane.showConfirmDialog(myRootComponent,
                                             file+" exists!\nOverwrite?",
                                             "Overwrite?",
                                             JOptionPane.YES_NO_OPTION,
                                             JOptionPane.WARNING_MESSAGE);
        if (retval!=JOptionPane.YES_OPTION) return;
      };
      
      FileWriter out=null;
      try{
        out=new FileWriter(file);
        text.write(out);
        out.close();
      }
      catch(Exception x)
      {
        JOptionPane.showMessageDialog(myRootComponent,
                                      "File error: "+x.getMessage(),
                                      "File error",
                                      JOptionPane.ERROR_MESSAGE);
        try{out.close();}catch(Exception y){};
        return;
      };
    };
  };
  
  
  /**
  * <p>Returns <code>true</code> if <code>formula</code> (!!after converting to
  * uppercase removing all whitespace from it!!) is safe for 
  * further processing. This does not mean
  * it is free of syntax errors, but if the formula is accepted by
  * newFromInfix(), it can be used in this program. This includes a check whether
  * bound variables consist of only ASCII letters. If
  * unboundAllowed==true, unbound variables will not be reported as an error.</p>
  */
  static boolean isFormulaSafe(String formula, boolean unboundAllowed)
  {
    /*
      The following syntax check is only to make sure that all bound variables
      are simple ASCII letter sequences without whitespace in between, because
      we can only generate color values for those. The test also makes sure
      that there is at least one operand.
      There may be other syntax
      errors in level but these are not detected by the following scan.
    */
    formula=formula.toUpperCase();
    StringBuffer operand=new StringBuffer();
    int i=0;
    boolean foundOp=false;
    while (i<formula.length())
    {
      while (i<formula.length() && 
              (Character.isWhitespace(formula.charAt(i)) || formula.charAt(i)=='(')
            ) ++i;
            
      operand.delete(0,Integer.MAX_VALUE);
      while (i<formula.length() && 
             formula.charAt(i)!=')' &&
             !formula.regionMatches(i,"->",0,2)
            ) { operand.append(formula.charAt(i)); ++i; };
      
      String opstr=operand.toString().trim();
      if (opstr.length()==0) return false;
      if (opstr.equals("_|_")) 
        foundOp=true; 
      else
      {
        boolean validOp=false;
        if (unboundAllowed && opstr.charAt(0)=='X' && opstr.length()>1)
        {
          int j=1;
          while (j<opstr.length() && Character.isDigit(opstr.charAt(j))) ++j;
          validOp=(j==opstr.length());
        };
        
        if (!validOp)
        for (int j=0; j<opstr.length(); ++j)
          if (opstr.charAt(j)<'A' || opstr.charAt(j)>'Z') return false;
          
        foundOp=true;
      };       
      
      if (formula.regionMatches(i,"->",0,2)) {i+=2; continue;};
      
      while (i<formula.length() && 
              (Character.isWhitespace(formula.charAt(i)) || formula.charAt(i)==')')
            ) ++i;
            
      if (i<formula.length() && !formula.regionMatches(i,"->",0,2)) return false;
      i+=2;
    };
    return foundOp;
  };
  
  static String upperCaseNoSpace(String s)
  {
    StringBuffer sbuf=new StringBuffer(s.toUpperCase());
    for (int i=sbuf.length()-1; i>=0; --i)
      if (Character.isWhitespace(sbuf.charAt(i))) sbuf.deleteCharAt(i);
      
    return sbuf.toString();
  };
  
  protected boolean createStartTileForLevel(String level)
  {
    if (!isFormulaSafe(level,false)) return false;
    
    //because the check above has made sure that operands are valid,
    //we can now safely remove whitespace without changing the semantics of
    //level. Whitespace removal is necessary because (so far) the
    //newFromInfix*() functions don't chew whitespace.
    level=upperCaseNoSpace(level);
      
    FormulaDominoTree tautologyTree;
    try{
      tautologyTree=FormulaDominoTree.newFromInfix(level,new String[]{level},null);
    }   
    catch(IllegalArgumentException x)
    {
      return false;
    };
    
    //attach as many ->I blocks as possible so that the player doesn't have to do it
    if (autoSimplifyMenuItem.isSelected())
    {
      String[] leaves=new String[]{"X1"};
      String[] bonus={"X0"};
      FormulaDominoTree arrowIntroTree=FormulaDominoTree.newFromInfix("X0->X1",leaves,bonus);
      try{
        while(true)
        {
          arrowIntroTree.cloneDT().attachTo(tautologyTree,0);
        }
      }catch(domino.logic.ConflictingBindException x){};
    };  
    
    startTile=new DominoTile(tautologyTree);
    startTile.deactivateRootBlock();
      
    return true;
  };  
  
  public class Victory implements Runnable
  {
    public void run()
    {
      while(true)
      {
        Object[] options={"Advance","Restart","Show Proof","Continue"};
        int retval=JOptionPane.showOptionDialog(myRootComponent,
                                                "Congratulations!",
                                                "You did it!",
                                                JOptionPane.YES_NO_CANCEL_OPTION,
                                                JOptionPane.INFORMATION_MESSAGE,
                                                null,
                                                options,
                                                options[0]);
        switch(retval)
        {
          case 0: nextLevel(); return;
          case 1: restartLevelWithoutConfirmation(); return;
          case 2: showProof(); return;
          default: return;
        }
      } 
    }
  }
};


class TxtFileFilter extends FileFilter
{
  String[] extensions_;
  
  public TxtFileFilter(String[] extensions)
  {
    extensions_=new String[extensions.length];
    System.arraycopy(extensions,0,extensions_,0,extensions_.length);
  };
  
  public boolean accept(File f)
  {
    if (f.isDirectory()) return true;
    for (int i=0; i<extensions_.length; ++i)
      if (f.getName().endsWith(extensions_[i])) return true;
    return false;
  };
  
  public String getDescription() 
  {
    StringBuffer desc=new StringBuffer("Text Files (");
    for (int i=0; i<extensions_.length-1; ++i) desc.append("*"+extensions_[i]+", ");
    desc.append("*"+extensions_[extensions_.length-1]+")");
    return desc.toString();
  };
};



class TileProducerManager
{
  protected class ProducerMenuItem extends JCheckBoxMenuItem
  {
    private EnhancedDominoTileProducer myProducer;
    private int index;
    private boolean fixed=false;
    public ProducerMenuItem(int sortOrderIdx,EnhancedDominoTileProducer producer,String name, boolean active)
    {
      super(name,active);
      myProducer=producer;
      index=sortOrderIdx;
    };
    
    public EnhancedDominoTileProducer producer() {return myProducer;};
    
    public String name() {return getText();};
    public int sortOrderIndex() {return index;};
    public void setSortOrderIndex(int newIndex) {index=newIndex;};
    public boolean isFixed() {return fixed;};
    public void setFixed() {fixed=true;};
    public boolean isEnabled() {return isSelected();};
  };
  
  private boolean cheating=false;
  /*
  * <p>contains ProducerMenuItems. The 1st entry is always the fixed producer.</p>
  */
  private Vector normalProducers=new Vector(); 
  private ProducerMenuItem extraProducer=null;
  private int fixedProducerIndex=-1;
  private int activeProducer=0;
  private int smallestSortOrderIndex=0;
  
  /**
  * <p>Creates a new <code>TileProducerManager</code> with the same fixed producer
  * as orig. Other producers are NOT copied.</p>
  */
  public TileProducerManager(TileProducerManager orig) //TESTED
  {
    this(orig.fixedProducerIndex,orig.getStringRepresentationForProducer(orig.fixedProducerIndex));
  };
  
  /**
  * <p>Creates a new <code>TileProducerManager</code> with a given fixed producer.</p>
  * <p>The fixed producer can not be disabled or removed and it will always be 
  * activated by <code>activateProducerIfEnabled(fixedProducerNum)</code> (if there
  * are less than <code>fixedProducerNum</code> producers, the fixed producer will
  * be available with other indices, too).</p>
  */
  public TileProducerManager(int fixedProducerNum, String fixedProducerStringRep)
  { //TESTED
    fixedProducerIndex=fixedProducerNum;
    addProducerForStringRepresentation(fixedProducerStringRep);
    getProd(fixedProducerNum).setFixed();    
    activeProducer=fixedProducerNum;
  };
  
  /** <p>Removes all producers except the fixed producer.</p>*/
  public void removeAllProducers() //TESTED
  {
    setExtraProducer(null);
    Iterator iter=normalProducers.iterator();
    while (iter.hasNext()) 
    {
      ProducerMenuItem prod=(ProducerMenuItem)iter.next();
      if (!prod.isFixed()) iter.remove();
    };
  };
  
  public void removeDisabledProducers() //TESTED
  {
    Iterator iter=normalProducers.iterator();
    while (iter.hasNext()) 
    {
      ProducerMenuItem prod=(ProducerMenuItem)iter.next();
      if (!(prod.isFixed()||prod.isEnabled())) iter.remove();
    };
  };
  
  /**
  * <p>Removes all producer entries from <code>tileMenu</code> and then adds
  * entries to the end of the menu for all producers except for the extra
  * producer and the fixed producer.</p>
  */
  public void updateMenu(JMenu tileMenu)
  {
    Component[] items=tileMenu.getMenuComponents();
    for (int i=0; i<items.length; ++i)
    {
      if (items[i] instanceof ProducerMenuItem) 
        tileMenu.remove((ProducerMenuItem)items[i]);
    };
    
    Iterator iter=normalProducers.iterator();
    while (iter.hasNext()) 
    {
      ProducerMenuItem prod=(ProducerMenuItem)iter.next();
      if (!prod.isFixed()) tileMenu.add(prod);
    };  
  };
  
  /**
  * <p>Turns the extra producer into a regular producer. 
  * Unless {@link #enableCheating()} has been called, a
  * {@link BonusEnhancedDominoTileProducer} will not be converted.</p>
  */
  public void extraProducerToRegularProducerIfPossible(String name) //TESTED
  {
    if (extraProducer==null) return;
    String srep=getStringRepresentationForProducer(-1);
    if (srep.equals("")) return;
    addProducerForStringRepresentation(name+": "+srep);
  };
  
  
  /**
  * <p>sreps with syntax errors will be silently ignored.</p>
  */  
  public void addProducerForStringRepresentation(String srep) //TESTED
  {
    /*
      NOTE: This method is called from the constructor to add the fixed producer
      (i.e. the very first producer) to normalProducers, so this method must not
      assume normalProducers is non-empty
    */
    
    String name="";
    int pos=srep.lastIndexOf(':');
    if (pos>=0) 
    {
      name=srep.substring(0,pos).trim();
      srep=srep.substring(pos+1);
    };
    
    FormulaDominoTree tree;
    try{
      tree=recursiveBuildTree(new StringBuffer(srep), new HashMap(),null,-1, FormulaDominoTree.UnboundIdAssigner.newAssigner());
    }catch(Exception x) {return;};  
    
    EnhancedDominoTileProducer newProducer=new NormalEnhancedDominoTileProducer(tree);
    --smallestSortOrderIndex;
    ProducerMenuItem newItem=new ProducerMenuItem(smallestSortOrderIndex,newProducer,name,true);
    normalProducers.add(newItem);
  };
  
  
  class BonusRef
  {
    public FormulaDominoTree tree;
    public int subtree;
    public int bonusForSubtreeIndex;
    public BonusRef(FormulaDominoTree t,int s,int b){tree=t;subtree=s;bonusForSubtreeIndex=b;};
  };
  
  /**
  * Throws IllegalArgumentException if stg is wrong.
  */
  protected FormulaDominoTree recursiveBuildTree(StringBuffer rest,HashMap formulaToBonusRef,FormulaDominoTree parent,int parentIndex, FormulaDominoTree.UnboundIdAssigner assign)
  {
    int pos=rest.toString().indexOf(';');
    if (pos<0) pos=rest.length();
    
    String srep=rest.substring(0,pos).trim();
    rest.delete(0,pos+1);
    
    if (srep.length()==0) return null;
    
    Vector parts=new Vector();
    while (0<=(pos=srep.indexOf(',')))
    {
      parts.add(srep.substring(0,pos));
      srep=srep.substring(pos+1);
    };
    parts.add(srep);
    
    Vector subParts=new Vector();
    Iterator iter=parts.iterator();
    while (iter.hasNext())
    {
      srep=(String)iter.next();
      Vector subPart=new Vector();
      while (0<=(pos=srep.indexOf('[')))
      {
        int pos2=srep.indexOf(']');
        if (pos2<=pos+1) throw new RuntimeException();
        String formula=srep.substring(pos+1,pos2);
        if (!UITest.isFormulaSafe(formula,true)) throw new RuntimeException();
        subPart.add(formula);
        srep=srep.substring(0,pos)+" "+srep.substring(pos2+1);
      };
      if (!UITest.isFormulaSafe(srep,true)) throw new RuntimeException();
      subPart.add(srep);
      subParts.add(subPart);
    };
    
    //now subParts is a Vector of Vectors of Strings that describe infix formulas
    //the last String in each (sub-)Vector is the root or leaf, the other strings are
    //bonuses. The first Vector describes the root, the others are leaves.
    
    FormulaDominoTree tree;
    
    Vector part1=(Vector)subParts.firstElement();
    String root=UITest.upperCaseNoSpace((String)part1.lastElement());

    if (subParts.size()==1) //only a root without leaves
    {
      try{
        BonusRef bRef=(BonusRef)formulaToBonusRef.get(root);
        if (bRef==null)
        {
          String[] lb={root};
          tree=FormulaDominoTree.newFromInfix(root,lb,lb);
          tree.useBonusSquare(0,0);
          if (parent!=null) tree.attachToSubtreeConnection(parent,parentIndex);
        }
        else
        {
          parent.useBonusSquare(parentIndex,bRef.tree,bRef.subtree,bRef.bonusForSubtreeIndex);
          tree=null;
        };
      }catch(Exception x){ throw new RuntimeException(); };
    }
    else //at least one leaf
    {
      String[] globalBonus=new String[part1.size()-1];
      for (int j=0; j<part1.size()-1; ++j) globalBonus[j]=UITest.upperCaseNoSpace((String)part1.get(j));
      String[] leaves=new String[subParts.size()-1];
      String[][] bonus=new String[subParts.size()-1][];
      for (int i=1; i<subParts.size(); ++i)
      {
        Vector subPart=(Vector)subParts.get(i);
        leaves[i-1]=UITest.upperCaseNoSpace((String)subPart.lastElement());
        bonus[i-1]=new String[subPart.size()-1];
        for (int j=0; j<subPart.size()-1; ++j) bonus[i-1][j]=UITest.upperCaseNoSpace((String)subPart.get(j));
      };
      
      try{
        tree=FormulaDominoTree.newFromInfix(root,leaves,globalBonus);
        
        if (parent!=null) tree.attachToSubtreeConnection(parent,parentIndex);
        
        for (int i=0; i<leaves.length; ++i)
          if (bonus[i].length>0) throw new RuntimeException("per-branch bonuses not supported");
          
        for (int i=0; i<tree.numberOfSubtreeConnections(); ++i)
        {
          HashMap newMap=new HashMap(formulaToBonusRef);
          for (int num=0; num<globalBonus.length; ++num)
          {
            newMap.put(globalBonus[num],new BonusRef(tree,i,num));
          };
          
          recursiveBuildTree(rest,newMap,tree,i,assign);
        };  
      }catch(Exception x){ throw new RuntimeException(); };
    };
    
    return tree;
  };  
  
  /**
  * <p>-1 is the extra producer. Unless {@link #enableCheating()} has been called,
  * {@link BonusEnhancedDominoTileProducer}s will be represented by an empty string.</p>
  * <p>Note, that if the producers name is an empty string, the returned string
  * will not contain a ":".</p>
  *
  * @throws IllegalArgumentException if there is no producer with index <code>i</code>.
  */
  public String getStringRepresentationForProducer(int i) //TESTED
  {
    ProducerMenuItem prod=getProd(i);
    String name=prod.name();
    if (!name.equals("")) name=name+": ";
    EnhancedDominoTile edt=prod.producer().produce();
    String ret=name+edt.toStringRepresentation();
    edt.removeIdAssignments();
    return ret;
  };
  
  /** 
  * <p>Returns the number of producers including the fixed producer but 
  * excluding the extra producer.</p>
  */
  public int numberOfProducers() //TESTED
  {
    return normalProducers.size();
  };

  public void enableCheating()
  {
    cheating=true;
  };

  /**
  * <p>Returns the producer with index <code>i</code>. -1 is the extra producer.</p>
  * 
  * @throws @throws IllegalArgumentException if there is no producer with index <code>i</code>.
  */
  protected ProducerMenuItem getProd(int i) //TESTED
  {
    if (i<-1 || (i==-1 && extraProducer==null) || (i>=normalProducers.size() && i>fixedProducerIndex)) 
      throw new IllegalArgumentException("producer not found");
    
    if (i==-1) 
      return extraProducer;
      
    if (i==fixedProducerIndex || i>=normalProducers.size() || (i<fixedProducerIndex &&  i>=normalProducers.size()-1)) 
      i=0;
    else
    {
      if (i<fixedProducerIndex) ++i;
    };
    return (ProducerMenuItem)normalProducers.get(i);
  };

  
  
  /** 
  * <p>Sets <code>prod</code> as the new extra producer.</p>
  * <p>The old extra producer (if any) will be removed. Unless <code>prod</code>
  * is <code>null</code>, it will become the new active producer. If <code>prod</code>
  * is <code>null</code>, another producer will be activated.</p>
  */
  public void setExtraProducer(EnhancedDominoTileProducer prod) //TESTED
  {
    if (prod==null)
    {
      if (activeProducer==-1) activateNextEnabledProducer();
      extraProducer=null;
    }
    else
    {
      --smallestSortOrderIndex;
      extraProducer=new ProducerMenuItem(smallestSortOrderIndex,prod,"",true);  
      activeProducer=-1;
    };
  };
  
  /**
  * <p>Activates the producer i (>=0) if it is enabled.</p>
  * <p>If <code>i</code> is invalid, nothing happens.</p>
  * @return true if producer has been enabled successfully
  */
  public boolean activateProducerIfEnabled(int i)
  {
    try{
      if (getProd(i).isEnabled()) { activeProducer=i; return true; };
    }catch(IllegalArgumentException x){};
    return false;
  };
  
  public void activateNextEnabledProducer() //TESTED
  {
    activateNextPrevProducer(+1,getProd(activeProducer).sortOrderIndex());
  };
  
  public void activatePreviousEnabledProducer()
  { 
    activateNextPrevProducer(-1,getProd(activeProducer).sortOrderIndex());
  };
  
  public void activateFirstEnabledProducer()
  {
    activateNextPrevProducer(+1,smallestSortOrderIndex-1);
  };
  
  /** 
  * <p>If <code>np==+1</code> activates the next, if <code>np==-1</code>
  * activates the previous producer in the sort order, relative to the
  * producer with sort order index <code>idx</code>.</p> 
  */
  public void activateNextPrevProducer(int np, int idx) //TESTED
  {
    int smallestGreater=Integer.MAX_VALUE;
    int smallestGreaterProducer=Integer.MAX_VALUE;
    int smallest=idx;
    int smallestProducer=activeProducer;
    if (extraProducer!=null)
    {
      smallest=getProd(-1).sortOrderIndex();
      smallestProducer=-1; 
      if (np*smallest>np*idx) 
      {
        smallestGreater=smallest;
        smallestGreaterProducer=smallestProducer;
      };
    };
    
    for (int i=0; i<numberOfProducers(); ++i)
    {
      ProducerMenuItem prod=getProd(i);
      if (!prod.isEnabled()) continue;
      
      if (np*prod.sortOrderIndex()<np*smallest)
      {
        smallest=prod.sortOrderIndex();
        smallestProducer=i;
      };
      if ((np*prod.sortOrderIndex()>np*idx) &&  
          (np*prod.sortOrderIndex()<np*smallestGreater))
      {
        smallestGreater=prod.sortOrderIndex();
        smallestGreaterProducer=i;
      };
    };
    if (smallestGreater==Integer.MAX_VALUE) 
      activeProducer=smallestProducer;
    else 
      activeProducer=smallestGreaterProducer;
  };
  
  /**
  * <p>Puts the currently active producer to the front of the sort order.
  * This only affects {@link #activateNextEnabledProducer()} and 
  * {@link #activatePreviousEnabledProducer()}, but not
  * {@link #activateProducerIfEnabled(int)}.</p>
  */
  public void sortActiveToFront() //TESTED
  {
    --smallestSortOrderIndex;
    getProd(activeProducer).setSortOrderIndex(smallestSortOrderIndex);
  };
  
  /**
  * <p>Returns a tile produced by the currently active producer.</p>
  */
  public EnhancedDominoTile produce() //TESTED
  {
    return getProd(activeProducer).producer().produce();
  };
};




class MouseEventProcessor implements MouseListener, MouseMotionListener, KeyListener
{
  /**
  * <p>Number of empty rows/colums to keep at all sides of the board. If the adding
  * of a {@link DominoTile} occurs in this area, it will be increased.</p>
  */
  public static final int FREE_SQUARES_AROUND_BOARD=16;
  
  protected static final int KC_CTRL_R=17;
  protected static final int KC_CTRL_L=17;
  protected static final int KC_SHIFT_R=16;
  protected static final int KC_SHIFT_L=16;
  protected static final int KC_ALT_R=65406;
  protected static final int KC_ALT_L=18;
  protected static final int KC_SPACE=32;
  protected static final int KC_0=48;
  protected static final int KC_9=57;
  
  protected static final int KC_ROTATE_RIGHT1=87;
  protected static final int KC_ROTATE_RIGHT2=69;
  protected static final int KC_ROTATE_RIGHT3=82;
  protected static final int KC_ROTATE_LEFT=81;
  protected static final int KC_DROP_TILE=KC_SPACE;
  protected static final int KC_PICKUP_TILE=KC_SPACE;
  
  protected static final int MOD_LEFT_BUTTON=1;
  protected static final int MOD_RIGHT_BUTTON=2;
  protected static final int MOD_MIDDLE_BUTTON=4;
  protected static final int MOD_CTRL=8;
  protected static final int MOD_SHIFT=16;
  protected static final int MOD_ALT=32;
  protected static final int MOD_SPACE=128;
  
  
  private MouseEventProcessorState state;
  private MouseEventProcessorState noTileHangingAtCursorIdle;

  private MouseEventProcessorState zoom;
  private MouseEventProcessorState moveBoard;

  private MouseEventProcessorState tileHangingAtCursorIdle;
  private MouseEventProcessorState tileHangingAtCursorRotateTile;
  private MouseEventProcessorState rotateTile;
  
  private Point dragStart;
  private Point lastModChangeMousePos;
  private Point mousePos=new Point(0,0);
  private int myModifiers=0;
  private boolean zoomingIn;
  private MouseEventProcessorState lastIdleState;
  private boolean lastIdleStateTracksMovement;
  private boolean dragInhibitor;
  
  private EnhancedDominoTile hangingTile;
  private int hangingTileOrientation=0;
  private TileProducerManager producerManager;

  private IsoWorld myWorld;
  private DominoTile masterTile; //this tile must not be removed
  private UITest.Victory victory;
  
  protected boolean leftButton(MouseEvent e)
  {
    return (e.getModifiers()&InputEvent.BUTTON1_MASK)!=0;
  };
  
  protected boolean rightButton(MouseEvent e)
  {
    return (e.getModifiers()&InputEvent.BUTTON3_MASK)!=0;
  };
  
  protected boolean middleButton(MouseEvent e)
  {
    return (e.getModifiers()&InputEvent.BUTTON2_MASK)!=0;
  };
  
  protected boolean ctrlKey(MouseEvent e)
  {
    return (e.getModifiers()&InputEvent.CTRL_MASK)!=0;
  };
  
  protected boolean shiftKey(MouseEvent e)
  {
    return (e.getModifiers()&InputEvent.SHIFT_MASK)!=0;
  };
  
  protected boolean altKey(MouseEvent e)
  {
    return (e.getModifiers()&InputEvent.ALT_MASK)!=0;
  };
  
  protected static boolean leftButton(int modifiers)
  {
    return (modifiers&MOD_LEFT_BUTTON)!=0;
  };
  
  protected static boolean rightButton(int modifiers)
  {
    return (modifiers&MOD_RIGHT_BUTTON)!=0;
  };
  
  protected static boolean middleButton(int modifiers)
  {
    return (modifiers&MOD_MIDDLE_BUTTON)!=0;
  };
  
  protected static boolean ctrlKey(int modifiers)
  {
    return (modifiers&MOD_CTRL)!=0;
  };
  
  protected static boolean shiftKey(int modifiers)
  {
    return (modifiers&MOD_SHIFT)!=0;
  };
  
  protected static boolean altKey(int modifiers)
  {
    return (modifiers&MOD_ALT)!=0;
  };
  
  public MouseEventProcessor(IsoWorld world, TileProducerManager producerManager_, DominoTile masterTile_, UITest.Victory v)
  {
    victory=v;
    myWorld=world;
    masterTile=masterTile_;
    producerManager=producerManager_;
    
    tileHangingAtCursorIdle=new TileHangingAtCursorIdle();
    noTileHangingAtCursorIdle=new NoTileHangingAtCursorIdle();
    zoom=new Zoom();
    moveBoard=new MoveBoard();
    rotateTile=new RotateTile();
    
    dragInhibitor=false;
        
    setState(noTileHangingAtCursorIdle);
    
    setUpEventProcessing();
  };
  
  protected void setUpEventProcessing()
  {
    myWorld.graphicalRepresentation().addMouseListener(this);
    myWorld.graphicalRepresentation().addMouseMotionListener(this);
    myWorld.graphicalRepresentation().addKeyListener(this);
  };
  
  public void reset(DominoTile newMasterTile)
  {
    producerManager.setExtraProducer(null);

    if (lastIdleState==tileHangingAtCursorIdle)
    {
      hangingTile.deunifyIfNecessary();
      myWorld.removeObject(hangingTile);
      hangingTile.removeIdAssignments();
    };
    
    masterTile=newMasterTile;
    
    dragInhibitor=false;
    myModifiers=0;    
    setState(noTileHangingAtCursorIdle);
  };
  
  public void setProducerManager(TileProducerManager newPMan) 
  {
    producerManager=newPMan;
  };
  
  protected void setState(MouseEventProcessorState s)
  {
    state=s;
    state.init();
  };
  
  
  protected void checkKeyModifiers(MouseEvent e)
  {
    myModifiers&=~(MOD_CTRL|MOD_SHIFT|MOD_ALT);
    if (ctrlKey(e)) myModifiers|=MOD_CTRL;
    if (shiftKey(e)) myModifiers|=MOD_SHIFT;
    if (altKey(e)) myModifiers|=MOD_ALT;
  };
  
  public void mousePressed(MouseEvent e)
  {
    int oldMods=myModifiers;
    int mod=e.getModifiers();

    if (leftButton(e)) 
    {
      myModifiers|=MOD_LEFT_BUTTON;
    };  
    if (rightButton(e)) 
    {
      myModifiers|=MOD_RIGHT_BUTTON;
    };  
    if (middleButton(e))
    {
      myModifiers|=MOD_MIDDLE_BUTTON;
    };
    
    checkKeyModifiers(e);

    if (myModifiers!=oldMods) 
    {
      if (myModifiers==0) dragInhibitor=false;
      lastModChangeMousePos=e.getPoint();
      state.handleModifierChange();
    };  
  };
  
  public void mouseReleased(MouseEvent e)
  {
    int oldMods=myModifiers;
    int mod=e.getModifiers();

    if (leftButton(e)) 
    {
      myModifiers&=~MOD_LEFT_BUTTON;
    };  
    if (rightButton(e)) 
    {
      myModifiers&=~MOD_RIGHT_BUTTON;
    };  
    if (middleButton(e))
    {
      myModifiers&=~MOD_MIDDLE_BUTTON;
    };

    checkKeyModifiers(e);
    
    if (myModifiers!=oldMods) 
    {
      if (myModifiers==0) dragInhibitor=false;
      lastModChangeMousePos=e.getPoint();
      state.handleModifierChange();
    };
  };
    
  public void keyPressed(KeyEvent e)  
  {
    int oldMods=myModifiers;
    switch(e.getKeyCode())
    {
      //case KC_CTRL_R:
      case KC_CTRL_L: myModifiers|=MOD_CTRL; break;
      //case KC_SHIFT_R:
      case KC_SHIFT_L: myModifiers|=MOD_SHIFT; break;
      case KC_ALT_R:
      case KC_ALT_L: myModifiers|=MOD_ALT; break;
      case KC_SPACE: myModifiers|=MOD_SPACE; break;
    };
    if (myModifiers!=oldMods) 
    {
      if (myModifiers==0) dragInhibitor=false;
      lastModChangeMousePos=mousePos;
      state.handleModifierChange();
    };
    state.handleKeyPress(e);
  };
  
  public void keyReleased(KeyEvent e) 
  {
    int oldMods=myModifiers;
    switch(e.getKeyCode())
    {
      //case KC_CTRL_R:
      case KC_CTRL_L: myModifiers&=~MOD_CTRL; break;
      //case KC_SHIFT_R:
      case KC_SHIFT_L: myModifiers&=~MOD_SHIFT; break;
      case KC_ALT_R:
      case KC_ALT_L: myModifiers&=~MOD_ALT; break;
      case KC_SPACE: myModifiers&=~MOD_SPACE; break;
    };
    if (myModifiers!=oldMods) 
    {
      if (myModifiers==0) dragInhibitor=false;
      lastModChangeMousePos=mousePos;
      state.handleModifierChange();
    };
    state.handleKeyRelease(e);
  };
  
  public void keyTyped(KeyEvent e)    {};
    
  public void mouseEntered(MouseEvent e)
  {
    myWorld.graphicalRepresentation().requestFocus();
    myModifiers=0;
  };
  
  public void mouseExited(MouseEvent e) 
  {
    myModifiers=0;
  };
  
  public void mouseClicked(MouseEvent e)
  {
    state.handleMouseClick(e);
  };
  public void mouseDragged(MouseEvent e)
  {
    mousePos=e.getPoint();
    state.handleMouseMotion();
  };
  public void mouseMoved(MouseEvent e)  
  {
    mousePos=e.getPoint();
    state.handleMouseMotion();
  };
    
  
  protected class MouseEventProcessorState
  {
    public void handleMouseClick(MouseEvent e) {};
    public void handleMouseMotion()            {};
    public void handleKeyPress(KeyEvent e)     {};
    public void handleKeyRelease(KeyEvent e)   {};
    public void handleModifierChange()         {};
    
    public void trackMovement() {};
    
    public void init() {};
  };



//####################################################################################  
  protected class       NoTileHangingAtCursorIdle     extends MouseEventProcessorState
//####################################################################################
  {
    private static final int TEAR_OFF_THRESHOLD=16;
    
    public void init()
    {
      lastIdleState=noTileHangingAtCursorIdle;
      lastIdleStateTracksMovement=false;
    };
    
    
    public void handleMouseMotion() 
    {
      if (myModifiers==0||dragInhibitor) return;
  
      int mod=myModifiers;
      
      if (ctrlKey(mod)||shiftKey(mod))
      {
          if (!(leftButton(mod)||rightButton(mod)||middleButton(mod))) return;
          dragStart=lastModChangeMousePos;
          zoomingIn=ctrlKey(mod);
          setState(zoom);
          state.handleMouseMotion();
      }
      else
      if (leftButton(mod)&&(!altKey(mod)))
      {
          dragStart=lastModChangeMousePos;
          setState(moveBoard);
          state.handleMouseMotion();
      }
      else
      if (rightButton(mod)||middleButton(mod)||(leftButton(mod)&&altKey(mod)))
      {
          Point p=new Point(mousePos);
          p.x-=lastModChangeMousePos.x;
          p.y-=lastModChangeMousePos.y;
          int dif=(int)Math.round(Math.sqrt(p.x*(double)p.x+p.y*(double)p.y));
          if (dif>TEAR_OFF_THRESHOLD)          
            attachTileToMouse(true);
      };
    };
    
    public void handleMouseClick(MouseEvent e)
    {
      if (myModifiers!=0 && (!altKey(myModifiers))) return;
      attachTileToMouse(false);
    };
    
    public void handleKeyPress(KeyEvent e)
    {
      int kc=e.getKeyCode();
      if (kc==KC_PICKUP_TILE) attachTileToMouse(false);
      else if (kc>=KC_0 && kc<=KC_9)
      {
        if (producerManager.activateProducerIfEnabled((int)(kc-KC_0)-1)) produceHangingTile();
      };
    };
    
    public void attachTileToMouse(boolean tearOff)
    {
      //NOTE: This function is also called on right-drag if the TEAR_OFF_THRESHOLD
      //has been exceeded (see mouseDragged(MouseEvent) )

      int mod=myModifiers;
      
      if (true) //used to be if (rightButton(mod) but I decided to remove this restriction
      {
          Point clickpos=mousePos;
          if (tearOff) clickpos=lastModChangeMousePos;
          
          JIsoWorld myJIsoWorld=myWorld.graphicalRepresentation();
          //try with z==1 first to give high blocks precedence
          IsoLocation clickLocation=myJIsoWorld.translateToIsoWorld(clickpos,1);
          Collection blocks=myWorld.blocksAtLocation(clickLocation);
          if (blocks==null)
          {
            clickLocation=myJIsoWorld.translateToIsoWorld(clickpos,0);
            blocks=myWorld.blocksAtLocation(clickLocation);
          };
          
          boolean produceHangingTile=false;
          
          if (blocks==null) //user clicked empty space
          {
            if (!tearOff) produceHangingTile=true;
          }
          else //user clicked on an IsoBlock
          {
            EnhancedDominoTileProducer newCurrentExtraProducer=null;
            DominoTile.DominoBlock clickedBlock=
                                     (DominoTile.DominoBlock)blocks.iterator().next();
            DominoTile clickedTile=(DominoTile)clickedBlock.parentObject();

            if (tearOff && clickedTile==masterTile) return;
            
            boolean clickedBonusBlock=(clickedBlock instanceof DominoTile.BonusDominoBlock);
            boolean bonusBlockIsPartOfBiggerTile=clickedTile.numberOfBlocks()>1;
            
            if (clickedBonusBlock && (!tearOff || !bonusBlockIsPartOfBiggerTile))
            { //user clicked on a bonus block and is either not dragging or the
              //bonus block is a tile of its own
              if (clickedBlock.isActive())
              {
                DominoTile.BonusDominoBlock bonusBlock=
                                           (DominoTile.BonusDominoBlock)clickedBlock;
                newCurrentExtraProducer=new BonusEnhancedDominoTileProducer(
                     bonusBlock.formulaDominoTree(),
                     bonusBlock.subtreeConnectionIndex(),
                     bonusBlock.newBonusForSubtreeConnectionIndex());
                     
                if (tearOff) ((EnhancedDominoTile)clickedTile).dieWithChildren();
              };  
            }
            else //user clicked on a non-bonus block or is dragging on a bonus block
            {    //that is part of a bigger tile
              FormulaDominoTree tree=(FormulaDominoTree)clickedTile.rootTree().cloneDT();
              tree.detachFromParent();
              newCurrentExtraProducer=new NormalEnhancedDominoTileProducer(tree);
              
              if (tearOff) ((EnhancedDominoTile)clickedTile).dieWithChildren();
            };
            
            if (newCurrentExtraProducer!=null)
            {
              producerManager.setExtraProducer(newCurrentExtraProducer);
              produceHangingTile=true;
            };  
          };
          
          if (produceHangingTile) 
          {
            if (tearOff) dragInhibitor=true;
            produceHangingTile();
          };  
      };
    };
  };

  protected void produceHangingTile()
  {
    hangingTile=producerManager.produce();
    hangingTile.setOrientation(hangingTileOrientation);
    //clickLocation,new IsoShift(0,0,0) is only approximate location, the call
    //state.handleMouseMotion() later will reposition the tile exactly
    myWorld.addObject(hangingTile,new IsoLocation(0,0,0),new IsoShift(0,0,0));
    myWorld.putInTopLayer(hangingTile);
    
    setState(tileHangingAtCursorIdle);
    state.handleMouseMotion(); //to position the tile properly
  };

  
//####################################################################################  
  protected class                     Zoom            extends MouseEventProcessorState
//####################################################################################
  {
    private static final int DRAG_THRESHOLD=5;
    
    private boolean goingright;
    private boolean goingdown;
    private boolean havedirection;
    private int startSquareSize;
    private Point viewportCenter;
    private Point2D.Double startD;
    
    public void init()
    {
      havedirection=false;
      startSquareSize=myWorld.getSquareSize();
          
      Dimension d=myWorld.graphicalRepresentation().getViewport().getExtentSize();
      viewportCenter=new Point(d.width>>1,d.height>>1);
          
      if (zoomingIn)
        startD=myWorld.graphicalRepresentation().translateToBoardNormalized(dragStart);
      else
        startD=myWorld.graphicalRepresentation().translateToBoardNormalized(viewportCenter);
    };
    
    
    public void handleMouseMotion()
    {
      if (myModifiers==0||dragInhibitor) return;
      
      int curx=mousePos.x;
      int cury=mousePos.y;
      long difx=Math.abs(curx-dragStart.x);
      long dify=Math.abs(cury-dragStart.y);
    
      difx-=DRAG_THRESHOLD;
      if (difx<0) difx=0;
      dify-=DRAG_THRESHOLD;
      if (dify<0) dify=0;

      if (difx+dify!=0)
      {
        if (!havedirection)
        {
          goingright=(curx > dragStart.x);
          goingdown=(cury > dragStart.y);
          havedirection=true;
        }
    
        if ((curx>dragStart.x)!=goingright) difx=0;
        if ((cury>dragStart.y)!=goingdown) dify=0;
    
        double dif=Math.sqrt(difx*difx + dify*dify);
    
        if (zoomingIn) 
          myWorld.setSquareSize(startSquareSize+(int)dif/2,startD.x,startD.y,curx,cury);
        else
          myWorld.setSquareSize(startSquareSize-(int)dif/2,startD.x,startD.y,viewportCenter.x,viewportCenter.y);
      };
      
      if (lastIdleStateTracksMovement) lastIdleState.trackMovement();
    };  
    
    
    public void handleModifierChange()
    {
      setState(lastIdleState);
      if (lastIdleStateTracksMovement) lastIdleState.trackMovement();
    };
  };




//####################################################################################  
  protected class                  MoveBoard          extends MouseEventProcessorState
//####################################################################################
  {
    private Point viewportPosition;
    
    public void init()
    {
      viewportPosition=myWorld.graphicalRepresentation().getViewport().getViewPosition();
    };
    
    public void handleMouseMotion()
    {
      if (myModifiers==0||dragInhibitor) return;
      
      int curx=mousePos.x;
      int cury=mousePos.y;
      int difx=dragStart.x-curx;
      int dify=dragStart.y-cury;
      myWorld.graphicalRepresentation().moveViewportAbsolute(viewportPosition.x+difx,viewportPosition.y+dify);
      if (lastIdleStateTracksMovement) lastIdleState.trackMovement();
    };
  
    public void handleModifierChange()
    {
      setState(lastIdleState);
      if (lastIdleStateTracksMovement) lastIdleState.trackMovement();
    };
  };
  
  
  
  
//####################################################################################  
  protected class       TileHangingAtCursorIdle       extends MouseEventProcessorState
//####################################################################################
  {
    private boolean validDropLocation;
    private IsoLocation dropLocation;
    
    public void init()
    {
      if (lastIdleState!=this)
      {
        validDropLocation=false;
        dropLocation=null;
        lastIdleState=tileHangingAtCursorIdle;
        lastIdleStateTracksMovement=true;
      };  
    };
    
    public void handleMouseMotion() 
    {
      if (myModifiers==0||dragInhibitor) {trackMovement(); return;};
      
      int mod=myModifiers;
      
      if (ctrlKey(mod)||shiftKey(mod))
      {
          if (!(leftButton(mod)||rightButton(mod)||middleButton(mod))) 
            {trackMovement(); return;};
          dragStart=lastModChangeMousePos;
          zoomingIn=ctrlKey(mod);
          setState(zoom);
          state.handleMouseMotion();
      }
      else
      if (leftButton(mod)&&(!altKey(mod)))
      {
          dragStart=lastModChangeMousePos;
          setState(moveBoard);
          state.handleMouseMotion();
      }
      else 
      if (rightButton(mod)||middleButton(mod)||(leftButton(mod)&&altKey(mod)))
      {
          dragStart=lastModChangeMousePos;
          setState(rotateTile);
          state.handleMouseMotion();
      }
      else trackMovement();
    };
    
    
    public void trackMovement()
    {
      Point p=mousePos;
      JIsoWorld myJIsoWorld=myWorld.graphicalRepresentation();
      IsoShift clickShift=new IsoShift();
      IsoLocation clickLocation=myJIsoWorld.translateToIsoWorld(p,0,clickShift);
      
      if (!clickLocation.equals(dropLocation))
      {
        dropLocation=new IsoLocation(clickLocation);
        
        if (validDropLocation)
        {
          hangingTile.deunifyIfNecessary();
          validDropLocation=false;
        };
        
        if (hangingTile.unifyWithNearestTile(clickLocation))
        {
          validDropLocation=true;
        };
      };
      
      
      //adjust to get shift for middle of top side rather than upper left corner
      clickShift.x-=0.5;
      if (clickShift.x<0) {clickShift.x+=1.0; --clickLocation.x;};
      clickShift.y-=0.5;
      if (clickShift.y<0) {clickShift.y+=1.0; --clickLocation.y;};
      myWorld.moveObject(hangingTile,clickLocation,clickShift);
    };
    
    public void handleMouseClick(MouseEvent e)
    {
      int mod=myModifiers;

      if (leftButton(e)&&(!altKey(mod))) 
        dropTile();
      else
      if (rightButton(e)||(leftButton(e)&&altKey(mod)))
      {
        producerManager.activateNextEnabledProducer();
        createNewTile();
      }
      else
      if (middleButton(e)) rotateRight();
    };
    
    
    protected void createNewTile()
    {
      IsoShift sh=hangingTile.getShift();
      IsoLocation loc=hangingTile.getReferenceBlockLocation();
      hangingTile.deunifyIfNecessary();
      myWorld.removeObject(hangingTile);
      hangingTile.removeIdAssignments();
      validDropLocation=false;
      dropLocation=null;
        
      hangingTile=producerManager.produce();
      hangingTile.setOrientation(hangingTileOrientation);
      myWorld.addObject(hangingTile,loc,sh);
      myWorld.putInTopLayer(hangingTile);

      trackMovement(); //to recheck if location is valid drop location and unify
                    //if necessary
    };
    
    protected void dropTile()
    {
      if (!validDropLocation)
      {
        hangingTile.deunifyIfNecessary();

        if ((ctrlKey(myModifiers)||shiftKey(myModifiers)) && hangingTile.hasNoAdjacentBlocks(dropLocation))
          validDropLocation=true;
        else
        {
          myWorld.removeObject(hangingTile);
          hangingTile.removeIdAssignments();
        };  
      };

      if (validDropLocation)
      {
        hangingTile.attachToUnified();
        myWorld.moveObject(hangingTile,dropLocation,new IsoShift(0,0,0));
        myWorld.putInDefaultLayer(hangingTile);

        producerManager.sortActiveToFront();
        
        if (masterTile.rootTree().numberOfOpenLeaves()==0) 
        {
          SwingUtilities.invokeLater(victory);
          myModifiers=0;
        };

        /*
        * check if the newly added tile has an IsoBlock very close to (or even
        * beyond) the edge of the board and increase the board size if necessary
        */
        int left=-myWorld.minusXDim()+FREE_SQUARES_AROUND_BOARD;
        int right=myWorld.plusXDim()-FREE_SQUARES_AROUND_BOARD;
        int top=-myWorld.minusYDim()+FREE_SQUARES_AROUND_BOARD;
        int bottom=myWorld.plusYDim()-FREE_SQUARES_AROUND_BOARD;
        Iterator i=hangingTile.blocksIterator();
        while (i.hasNext())
        {
          IsoLocation loc=((IsoBlock)i.next()).getAbsoluteLocation();
          if (loc.x>right) myWorld.addLines(1,loc.x-right);
          if (loc.x<left) myWorld.addLines(0,left-loc.x);
          if (loc.y>bottom) myWorld.addLines(3,loc.y-bottom);
          if (loc.y<top) myWorld.addLines(2,top-loc.y);
        };
      };

      setState(noTileHangingAtCursorIdle);
    };
    
    public void handleKeyPress(KeyEvent e)
    {
      int kc=e.getKeyCode();
      if (kc==KC_ROTATE_RIGHT1||kc==KC_ROTATE_RIGHT2||kc==KC_ROTATE_RIGHT3) rotateRight();
      else if (kc==KC_ROTATE_LEFT) rotateLeft();
      else if (kc==KC_DROP_TILE) dropTile();
      else if (kc>=KC_0 && kc<=KC_9)
      {
        if (producerManager.activateProducerIfEnabled((int)(kc-KC_0)-1)) createNewTile();
      };
    };
    
    protected void rotateRight()
    {
      hangingTile.deunifyIfNecessary();
      validDropLocation=false;
      dropLocation=null;
      hangingTileOrientation=(hangingTileOrientation+1)&3;
      hangingTile.setOrientation(hangingTileOrientation);
      myWorld.putInTopLayer(hangingTile);
      trackMovement();
    };
    
    protected void rotateLeft()
    {
      hangingTile.deunifyIfNecessary();
      validDropLocation=false;
      dropLocation=null;
      hangingTileOrientation=(hangingTileOrientation+3)&3;
      hangingTile.setOrientation(hangingTileOrientation);
      myWorld.putInTopLayer(hangingTile);
      trackMovement();
    };
    
  };



  
  
//####################################################################################  
  protected class                  RotateTile         extends MouseEventProcessorState
//####################################################################################
  {
    private static final int DRAG_THRESHOLD=32;
    private static final int NUM_ROTATE_STEPS=4;
    
    private boolean haveStartAngle;
    private double startAngle;
    private int startOrientation;
    
    public void init()
    {
      haveStartAngle=false;
      startOrientation=hangingTileOrientation;
    };
    
    
    public void handleMouseMotion()
    {
      if (myModifiers==0||dragInhibitor) return;
      
      int curx=mousePos.x;
      int cury=mousePos.y;
      long difx=curx-dragStart.x;
      long dify=cury-dragStart.y;
    
      double dif=Math.sqrt(difx*difx + dify*dify);
      if (dif>=DRAG_THRESHOLD)
      {
        double angle=Math.atan2(dify,difx);
        if (!haveStartAngle)
        {
          startAngle=angle;
          haveStartAngle=true;
        }
        else //if (haveStartAngle)
        {
          angle-=startAngle;
          if (angle<0) angle+=(2*Math.PI);
          int steps=(int)Math.round(NUM_ROTATE_STEPS*angle/(2*Math.PI));
          hangingTileOrientation=(startOrientation+steps)&3;
          hangingTile.setOrientation(hangingTileOrientation);
          myWorld.putInTopLayer(hangingTile);
        };
      };
    };  
    
    
    public void handleModifierChange()
    {
      setState(tileHangingAtCursorIdle);
      state.handleMouseMotion();
    };
  };


};



abstract class EnhancedDominoTile extends DominoTile
{
  public EnhancedDominoTile(FormulaDominoTree tree)
  {
    super(tree);
  };
  
  public EnhancedDominoTile(FormulaDominoTree tree,int subtreeIdx,int newBonusForSubtreeIdx)
  {
    super(tree,subtreeIdx,newBonusForSubtreeIdx);
  };
  
  public abstract boolean unifyWithNearestTile(IsoLocation location);
  public abstract void deunifyIfNecessary();
  public abstract void attachToUnified();
  
  public class IsoBlockPair
  {
    public IsoBlock block1;
    public IsoBlock block2;
  };
  
  /**
  * <p>Returns an {@link IsoBlock} that would be horizontally or vertically adjacent
  * to a block of <code>this</code> tile if <code>this</code> tile was put at
  * <code>location</code>.</p> 
  * <p>The {@link IsoBlock} is returned as {@link IsoBlockPair#block1} and the
  * adjacent block from <code>this</code> tile is returned as 
  * {@link IsoBlockPair#block2}.</p>
  * <p>Returns <code>null</code> if there is no adjacent block.</p>
  * <p>If <code>onlyone</code> is <code>true</code>, <code>null</code> is
  * returned if there is more than one adjacent block.</p>
  */
  public IsoBlockPair nearestIsoBlock(IsoLocation location, boolean onlyone)
  {
    IsoLocation[] offset={new IsoLocation(-1,0,0),new IsoLocation(1,-1,0),
                          new IsoLocation(1,1,0), new IsoLocation(-1,1,0)};
    IsoBlockPair found=null;
    Iterator iter=blocksIterator();
    while (iter.hasNext())
    {
      IsoBlock block2=(IsoBlock)iter.next();
      IsoLocation blockLoc=block2.getRelativeLocation();
      blockLoc.add(location);
      for (int i=0; i<4; ++i)
      {
        blockLoc.add(offset[i]);
        Collection blocks=getWorld().blocksAtLocation(blockLoc);
        if (blocks!=null)
        {
          Iterator iter2=blocks.iterator();
          while (iter2.hasNext())
          {
            IsoBlock block1=(IsoBlock)iter2.next();
            if (block1.parentObject()!=this)
            {
              if (found!=null) return null;
              found=new IsoBlockPair();
              found.block1=block1;
              found.block2=block2;
              if (!onlyone) return found;
            };
          };
        };
      };
    };
    
    return found;
  };
  
  /**
  * <p>Returns <code>true</code> if there exists no {@link IsoBlock} that would be 
  * horizontally or vertically adjacent
  * to a block of <code>this</code> tile if <code>this</code> tile was put at
  * <code>location</code>.</p> 
  */
  public boolean hasNoAdjacentBlocks(IsoLocation location)
  {
    return nearestIsoBlock(location,false)==null;
  };
  
  public void dieWithChildren()
  {
    DominoTile con=connectedToTile();
    detach();
    if (rootTree()!=null) rootTree().detachFromParent();
    recursiveDeath();
    if (con!=null) con.updateFormulas();
  };
  
  protected void recursiveDeath()
  {  
    for (int i=0; i<numberOfTileConnections(); ++i)
    {
      EnhancedDominoTile subTile=(EnhancedDominoTile)tileConnection(i);
      if (subTile!=null) subTile.recursiveDeath();
    };
    getWorld().removeObject(this);
    removeIdAssignments();
  };  
};


class NormalEnhancedDominoTile extends EnhancedDominoTile
{
  private DominoTile.RootDominoBlock rootBlock;
  private DominoTile.SubtreeConnectionDominoBlock leafBlock;
  
  public NormalEnhancedDominoTile(FormulaDominoTree tree)
  {
    super(tree);
  };
  
  public void deunifyIfNecessary()
  {
    if (rootBlock!=null && rootBlock.formulaDominoTree().detachFromParent())
    {
      ((DominoTile)rootBlock.parentObject()).updateFormulas();
      ((DominoTile)leafBlock.parentObject()).updateFormulas();
    
      //avoid keeping out of date references to prevent errors and gc problems
      rootBlock=null;
      leafBlock=null;
    };  
  };
  
  public boolean unifyWithNearestTile(IsoLocation location)
  {
    DominoTile.RootDominoBlock rBlock;
    DominoTile.SubtreeConnectionDominoBlock lBlock;
    
    location=new IsoLocation(location); //make copy to avoid modifying source

    IsoBlockPair compadres=nearestIsoBlock(location,true);
    if (compadres==null) return false;

    if ((compadres.block1 instanceof DominoTile.SubtreeConnectionDominoBlock) &&
        (compadres.block2 instanceof DominoTile.RootDominoBlock))
    {
      rBlock=(DominoTile.RootDominoBlock)compadres.block2;
      lBlock=(DominoTile.SubtreeConnectionDominoBlock)compadres.block1;   
    }
    else
    if ((compadres.block2 instanceof DominoTile.SubtreeConnectionDominoBlock) &&
        (compadres.block1 instanceof DominoTile.RootDominoBlock))
    {
      rBlock=(DominoTile.RootDominoBlock)compadres.block1;
      lBlock=(DominoTile.SubtreeConnectionDominoBlock)compadres.block2;
    }
    else return false;

    if (!(rBlock.isActive() && lBlock.isActive())) return false;

    FormulaDominoTree tree1=lBlock.formulaDominoTree();
    int tree1idx=lBlock.subtreeConnectionIndex();
    FormulaDominoTree tree2=rBlock.formulaDominoTree();
    try{
      tree2.attachToSubtreeConnection(tree1,tree1idx);
    }
    catch(domino.logic.ConflictingBindException x) { return false; }
    //NOTE: IllegalNodeTypeException is caught because lBlock could already be
    //connected to another tile on the board
    catch(domino.logic.IllegalNodeTypeException x) { return false; }
    
    rootBlock=rBlock;
    leafBlock=lBlock;
    ((DominoTile)rootBlock.parentObject()).updateFormulas();
    ((DominoTile)leafBlock.parentObject()).updateFormulas();
    
    return true;
  };
  

  public void attachToUnified()
  {
    if (rootBlock==null || rootBlock.formulaDominoTree().parent()==null) return;
    DominoTile connectingTile1=(DominoTile)rootBlock.parentObject();
    connectingTile1.attachTo(leafBlock);
    
    DominoTile connectingTile2=(DominoTile)leafBlock.parentObject();
    
    /*
    * The unification makes a lot of color assignments for unbound
    * nodes obsolete because they are superceded by the colors of the unified tree.
    * For that reason, we remove the assignments here. In some cases this may lead to
    * reassignments of visible colors, but this is extremely hard to avoid.
    */
    connectingTile1.removeUnneededIdAssignments();
    connectingTile2.removeUnneededIdAssignments();
    connectingTile1.updateFormulas(); //because some colors might have changed
    connectingTile2.updateFormulas(); //because some colors might have changed
    
    //set references to null because now this tile is attached to another tile and
    //these references are maintained by the DominoTile superclass, so that redundant
    //references should be avoided to prevent inconsistencies.
    rootBlock=null;
    leafBlock=null;
  };
  

  
};


class BonusEnhancedDominoTile extends EnhancedDominoTile
{
  private DominoTile.SubtreeConnectionDominoBlock leafBlock;
  
  public BonusEnhancedDominoTile(FormulaDominoTree tree,int subtreeIdx,int newBonusForSubtreeIdx)
  {
    super(tree,subtreeIdx,newBonusForSubtreeIdx);
  };
  
  
  public boolean unifyWithNearestTile(IsoLocation location)
  {
    DominoTile.BonusDominoBlock bonusBlock;
    DominoTile.SubtreeConnectionDominoBlock lBlock;
    
    location=new IsoLocation(location); //make copy to avoid modifying source

    IsoBlockPair compadres=nearestIsoBlock(location,true);
    if (compadres==null) return false;

    if ((compadres.block1 instanceof DominoTile.SubtreeConnectionDominoBlock) &&
        (compadres.block2 instanceof DominoTile.BonusDominoBlock))
    {
      bonusBlock=(DominoTile.BonusDominoBlock)compadres.block2;
      if (Debugging.enabled)
      {
        if (bonusBlock!=rootBlock()) throw new RuntimeException("weird!");
      };
      lBlock=(DominoTile.SubtreeConnectionDominoBlock)compadres.block1;   
    }
    else return false;

    if (!(lBlock.isActive() && bonusBlock.isActive())) return false;

    DominoTree tree1=lBlock.formulaDominoTree();
    int tree1idx=lBlock.subtreeConnectionIndex();

    if (tree1.subtree(tree1idx)!=null) return false;
    
    try{
      bonusBlock.attachBonusTree(tree1,tree1idx);
    }
    catch(domino.logic.ConflictingBindException x) { return false; }
    //NOTE: IllegalNodeTypeException is caught because lBlock could already be
    //connected to another tile on the board
    catch(domino.logic.IllegalNodeTypeException x) { return false; }
    
    leafBlock=lBlock;

    ((DominoTile)bonusBlock.parentObject()).updateFormulas();
    ((DominoTile)leafBlock.parentObject()).updateFormulas();
    
    return true;
  };
  
  
  public void deunifyIfNecessary()
  {
    DominoTile.BonusDominoBlock bonusBlock=(DominoTile.BonusDominoBlock)rootBlock();
    if (bonusBlock.detachBonusTree())
    {
      ((DominoTile)bonusBlock.parentObject()).updateFormulas();
      ((DominoTile)leafBlock.parentObject()).updateFormulas();
      
      //avoid keeping an out of date reference to avoid errors and gc problems
      leafBlock=null;
    };
  };
  
  public void attachToUnified()
  {
    DominoTile.BonusDominoBlock bonusBlock=(DominoTile.BonusDominoBlock)rootBlock();
    
    if (bonusBlock.getBonusTree()==null) return;
    
    DominoTile connectingTile1=(DominoTile)bonusBlock.parentObject();
    connectingTile1.attachTo(leafBlock);

    DominoTile connectingTile2=(DominoTile)leafBlock.parentObject();
    
    /*
    * The unification makes a lot of color assignments for unbound
    * nodes obsolete because they are superceded by the colors of the unified tree.
    * For that reason, we remove the assignments here. In some cases this may lead to
    * reassignments of visible colors, but this is extremely hard to avoid.
    */
    connectingTile1.removeUnneededIdAssignments();
    connectingTile2.removeUnneededIdAssignments();
    connectingTile1.updateFormulas(); //because some colors might have changed
    connectingTile2.updateFormulas(); //because some colors might have changed
    
    //set reference to null because we are now attached to leafBlock.parentObject()
    //and don't want to risk keeping a reference after a detach()
    leafBlock=null;
  };
};
    



interface EnhancedDominoTileProducer
{
  public EnhancedDominoTile produce();
};


class NormalEnhancedDominoTileProducer implements EnhancedDominoTileProducer
{
  private FormulaDominoTree myTree;
  
  public EnhancedDominoTile produce()
  {
    return new NormalEnhancedDominoTile((FormulaDominoTree)myTree.cloneDT());
  };
  
  NormalEnhancedDominoTileProducer(FormulaDominoTree tree)
  {
    myTree=tree;
  };
};


class BonusEnhancedDominoTileProducer implements EnhancedDominoTileProducer
{
  private FormulaDominoTree myTree;
  private int subtreeIndex;
  private int bonusIndex;
  
  public EnhancedDominoTile produce()
  {
    return new BonusEnhancedDominoTile(myTree,subtreeIndex,bonusIndex);
  };
  
  BonusEnhancedDominoTileProducer(FormulaDominoTree tree,int subtreeIdx,int bonusIdx)
  {
    myTree=tree;
    subtreeIndex=subtreeIdx;
    bonusIndex=bonusIdx;
  };
};