import javax.swing.border.*;
import isabelle.*;

font = jEdit.getFontProperty("view.font");

void symbolsDialog()
{
  title = "Modal logic symbols";

  String [] symbolnames = new String []
  { "\<top>", "\<bottom>", "\<not>",
    "^\<not>", "\<and>", "\<or>",
    "\<rightarrow>", "\<leftrightarrow>", "\<forall>",
    "\<exists>", "=", "=^L", 
    "\<box>", "\<diamond>", "\<lfloor> . \<rfloor>"};
  String [] description = new String []
  { "Truth", "Falsehood", "Negation",
    "Pred. Negation", "Conjunction", "Disjunction",
    "Implication", "Equivalence", "Universal Quantification",
    "Existential Quantification", "Equality", "Leibniz Equality",
    "Box operator", "Diamond operator", "Validity"};
  symboltable = new Hashtable();
  symboltable.put(Symbol.decode(symbolnames[0]),"\<^bold>\<top>");
  symboltable.put(Symbol.decode(symbolnames[1]),"\<^bold>\<bottom>");
  symboltable.put(Symbol.decode(symbolnames[2]),"\<^bold>\<not>");
  symboltable.put(Symbol.decode(symbolnames[3]),"\<^sup>\<not>");
  symboltable.put(Symbol.decode(symbolnames[4]),"\<^bold>\<and>");
  symboltable.put(Symbol.decode(symbolnames[5]),"\<^bold>\<or>");
  symboltable.put(Symbol.decode(symbolnames[6]),"\<^bold>\<rightarrow>");
  symboltable.put(Symbol.decode(symbolnames[7]),"\<^bold>\<leftrightarrow>");
  symboltable.put(Symbol.decode(symbolnames[8]),"\<^bold>\<forall>");
  symboltable.put(Symbol.decode(symbolnames[9]),"\<^bold>\<exists>");
  symboltable.put(Symbol.decode(symbolnames[10]),"\<^bold>=");
  symboltable.put(Symbol.decode(symbolnames[11]),"\<^bold>=\<^sup>L");
  symboltable.put(Symbol.decode(symbolnames[12]),"\<^bold>\<box>");
  symboltable.put(Symbol.decode(symbolnames[13]),"\<^bold>\<diamond>");
  symboltable.put(Symbol.decode(symbolnames[14]),"\<lfloor>\<rfloor>");
  abbrevtable = new Hashtable();
  abbrevtable.put(Symbol.decode(symbolnames[0]),"mtrue");
  abbrevtable.put(Symbol.decode(symbolnames[1]),"mfalse");
  abbrevtable.put(Symbol.decode(symbolnames[2]),"mnot");
  abbrevtable.put(Symbol.decode(symbolnames[3]),"mnegpred");
  abbrevtable.put(Symbol.decode(symbolnames[4]),"mand");
  abbrevtable.put(Symbol.decode(symbolnames[5]),"mor");
  abbrevtable.put(Symbol.decode(symbolnames[6]),"mimp");
  abbrevtable.put(Symbol.decode(symbolnames[7]),"mequ");
  abbrevtable.put(Symbol.decode(symbolnames[8]),"mforall");
  abbrevtable.put(Symbol.decode(symbolnames[9]),"mexists");
  abbrevtable.put(Symbol.decode(symbolnames[10]),"meq");
  abbrevtable.put(Symbol.decode(symbolnames[11]),"meqL");
  abbrevtable.put(Symbol.decode(symbolnames[12]),"mbox");
  abbrevtable.put(Symbol.decode(symbolnames[13]),"mdia");
  abbrevtable.put(Symbol.decode(symbolnames[14]),"valid");

  numSymbols = symbolnames.length;
  cols = 2;
  rows = numSymbols;
  size = 50; // width and height available for a single symbol

  dialog = new JDialog(view, title, false);
  
  encoding = new JTextField();
  encoding.setEditable(false);
  encoding.setPreferredSize(new Dimension(size * 4, size));

  abbrev = new JTextField();
  abbrev.setEditable(false);
  abbrev.setPreferredSize(new Dimension(size * 4, size));
  
  symbolPane = new JPanel(new GridLayout(rows, cols));
  symbolPane.setBorder(new EmptyBorder(3, 3, 3, 3));
  symbolPane.setPreferredSize(new Dimension(size * cols, size * rows));


  clickListener = new ActionListener()
  {
    void actionPerformed(e)
    { // insert selected symbol and close dialog
      pos = textArea.getCaretPosition();
      textArea.setSelectedText(symboltable.get(e.getSource().getLabel()));
      if (e.getSource().getLabel().equals(Symbol.decode(symbolnames[14]))) {
        textArea.setCaretPosition(pos+1);
      }
      
      //dialog.dispose();
    }
  };


  hoverListener = new MouseListener() // MouseAdapter does not work
  {
    void mouseEntered(e)
    { // show encoding and abbreviation (if available)
      symbol = Symbol.encode(symboltable.get(e.getSource().getLabel()));
      encoding.setText(symbol);
      abb = abbrevtable.get(e.getSource().getLabel());
      abbrev.setText(abb);
    }
    void mousePressed(e) {}
    void mouseReleased(e) {}
    void mouseExited(e) {}
    void mouseClicked(e) {}
  };

  closeButton = new JButton("Close");
  closeButton.addActionListener(new ActionListener()
  {
    void actionPerformed(e) { dialog.dispose(); }
  });
  
  
  for (int i = 0; i < numSymbols; i++) {
    button = new JButton(Symbol.decode(symbolnames[i])  );
    button.setMaximumSize(new Dimension(size,size));
    button.setFont(font.deriveFont(Font.BOLD));
    button.addActionListener(clickListener);
    button.addMouseListener(hoverListener);
    symbolPane.add(button);
    label = new JLabel(description[i]);
    label.setFont(font);
    symbolPane.add(label);
  }
  // setup GUI components
  scrollPane = new JScrollPane(symbolPane);
  scrollPane.setPreferredSize(new Dimension(size * cols + 3*size, size * rows / 2));
  scrollPane.getVerticalScrollBar().setUnitIncrement(size / 3);

  infoPane = new JPanel();
  infoPane.add(new JLabel("Encoding:"));
  infoPane.add(encoding);
  infoPane.add(new JLabel("Abbreviation:"));
  infoPane.add(abbrev);

  buttonPane = new JPanel();
  buttonPane.setLayout(new BoxLayout(buttonPane, BoxLayout.LINE_AXIS));
  buttonPane.add(Box.createHorizontalGlue());
  buttonPane.add(closeButton);

  contentPane = new JPanel();
  contentPane.setLayout(new BoxLayout(contentPane, BoxLayout.PAGE_AXIS));
  contentPane.add(scrollPane);
  contentPane.add(Box.createRigidArea(new Dimension(0,5)));
  contentPane.add(infoPane);
  contentPane.add(buttonPane);
  dialog.setContentPane(contentPane);

  dialog.pack();
  dialog.setLocationRelativeTo(view);
  dialog.setDefaultCloseOperation(JDialog.DISPOSE_ON_CLOSE);
  dialog.setVisible(true);
}

symbolsDialog();