/* Copyright (C) 2008 Hugh McGuire http://www.cis.gvsu.edu/~mcguire/ * Grand Valley State University, MI 49401-9403 */ /* 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; either version 3 of the License, or (at your option) any later 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. For a copy of the GNU General Public License, write to the Free Software Foundation, Inc., 51 Franklin Street, Fifth floor, Boston, MA 02110-1301, USA. Another option as of January 1, 2008 is to browse the following URL: http://www.gnu.org/copyleft/gpl.html */ import java.awt.*; import java.awt.event.*; import java.util.*; import javax.swing.*; import javax.swing.text.DefaultEditorKit; import java.io.*; /** * Manages user entry of theorem, presuppositions. * @author Hugh McGuire */ class User_Entry_Dialog extends JDialog { private JTextArea message_ta, entry_ta; private JTable table; private JPanel buttons_panel; private JButton cancel_newproof_button; private boolean accepting_multiple_exprs, allowing_free_variables, // Free variables would be misleading, appearing like constants; // and such wouldn't be permitted in a theorem say // if the user entered the theorem before // the presupposition using the variables seeking_constant_term; private Vector results; private String original_text; private Expression original, result; private Symbol comment_symbol; User_Entry_Dialog(JTable table_given) { //Create and set up the window. // Java doesn't allow |super((table = table_given)....| // because |super()| is supposed to occur first // and |super((table = table_given)....| would be // doing |table = table_given| first. super((JFrame) table_given.getTopLevelAncestor(), "User Entry", true); //dialog.setDefaultCloseOperation(JFrame.EXIT_ON_CLOSE); table = table_given; // NEED |"Edit"| MENU /* //Create and set up the menu bar: JMenuBar menu_bar = new JMenuBar(); //Create an Edit menu to support cut/copy/paste: JMenu menu = new JMenu("Edit"); // menu.setMnemonic(KeyEvent.VK_E); JMenuItem menu_item; menu_item = new JMenuItem(new DefaultEditorKit.CutAction()); menu_item.setText("Cut"); menu_item.setMnemonic(KeyEvent.VK_T); //menu_item.setAccelerator( //KeyStroke.getKeyStroke(KeyEvent.VK_X, ActionEvent.CTRL_MASK) //); menu.add(menu_item); menu_item = new JMenuItem(new DefaultEditorKit.CopyAction()); menu_item.setText("Copy"); menu_item.setMnemonic(KeyEvent.VK_C); //menu_item.setAccelerator( //KeyStroke.getKeyStroke(KeyEvent.VK_C, ActionEvent.CTRL_MASK) //); menu.add(menu_item); menu_item = new JMenuItem(new DefaultEditorKit.PasteAction()); menu_item.setText("Paste"); menu_item.setMnemonic(KeyEvent.VK_P); //menu_item.setAccelerator( //KeyStroke.getKeyStroke(KeyEvent.VK_V, ActionEvent.CTRL_MASK) //); menu.add(menu_item); menu_bar.add(menu); dialog.setJMenuBar(menu_bar); */ //JPanel content_pane = new JPanel(new BorderLayout()); Container content_pane = getContentPane(); // avoiding |GridBagLayout| message_ta = new JTextArea(); message_ta.setEditable(false); message_ta.setRows(4); final JScrollPane message_scroll_pane = new JScrollPane(message_ta); content_pane.add(message_scroll_pane, BorderLayout.PAGE_START); JPanel entry_panel = new JPanel(new BorderLayout()); content_pane.add(entry_panel, BorderLayout.CENTER); entry_ta = new JTextArea(); entry_ta.setFont( new Font("Monospaced", Font.PLAIN, entry_ta.getFont().getSize()) ); entry_ta.setRows(5); entry_ta.setColumns(55); entry_panel.add(new JScrollPane(entry_ta), BorderLayout.CENTER); this.addWindowListener( new WindowAdapter() { public void windowActivated(WindowEvent e) { entry_ta.requestFocusInWindow(); } } ); JPanel entry_help_panel = new JPanel(new BorderLayout()); entry_panel.add(entry_help_panel, BorderLayout.PAGE_END); entry_help_panel.add( new JLabel( /* " Pressing the Alt key" + " while typing one of the following characters" + " yields the corresponding symbol below: " */ " While entering text (above)," + " you can press the Alt key" + " while typing one of the following characters" + " to insert the corresponding symbol below: " ), BorderLayout.PAGE_START ); /* Though supposed to be "Monospaced", characters have different widths * so not aligned JTextField entry_alt_chars_tf = new JTextField( " A E s p = B b I i o a : # < > [ {" + " u t 0 1 2 3 - + W w n @ y C R Q Z N / " ); entry_alt_chars_tf.setEditable(false); entry_alt_chars_tf.setFont( new Font( "Monospaced", Font.PLAIN, entry_alt_chars_tf.getFont().getSize() ) ); entry_help_panel.add(entry_alt_chars_tf); JTextField entry_symbols_tf = new JTextField( " " + Symbol.FORALL_UNICODE + ' ' + Symbol.EXISTS_UNICODE + ' ' + Symbol.SUM_UNICODE + ' ' + Symbol.PROD_UNICODE + ' ' + Symbol.THREE_BAR_UNICODE + ' ' + Symbol.ARROW_LEFT_RIGHT_TWO_BARS_UNICODE + ' ' + Symbol.ARROW_LEFT_RIGHT_ONE_BAR_UNICODE + ' ' + Symbol.ARROW_RIGHT_TWO_BARS_UNICODE + ' ' + Symbol.ARROW_RIGHT_ONE_BAR_UNICODE + ' ' + Symbol.OR_UNICODE + ' ' + Symbol.AND_UNICODE + ' ' + Symbol.ARROW_LEFT_ONE_BAR_UNICODE + ' ' + Symbol.NEQ_UNICODE + ' ' + Symbol.LEQ_UNICODE + ' ' + Symbol.GEQ_UNICODE + ' ' + Symbol.SUBSET_UNICODE + ' ' + Symbol.SUBSETEQ_UNICODE + ' ' + Symbol.UNION_UNICODE + ' ' + Symbol.INTERSECT_UNICODE + ' ' + Symbol.SUPERSCRIPT_0_UNICODE + ' ' + Symbol.SUPERSCRIPT_1_UNICODE + ' ' + Symbol.SUPERSCRIPT_2_UNICODE + ' ' + Symbol.SUPERSCRIPT_3_UNICODE + ' ' + Symbol.SUPERSCRIPT_MINUS_UNICODE + ' ' + Symbol.THETA_UPPERCASE_UNICODE + ' ' + Symbol.OMEGA_UPPERCASE_UNICODE + ' ' + Symbol.OMEGA_LOWERCASE_UNICODE + ' ' + Symbol.NOT_UNICODE + ' ' + Symbol.TRIANGLE_FILLED_LEFT_POINTING_UNICODE + ' ' + Symbol.INFINITY_UNICODE + ' ' + Symbol.C_UNICODE + ' ' + Symbol.R_NUMBERS_UNICODE + ' ' + Symbol.Q_UNICODE + ' ' + Symbol.Z_UNICODE + ' ' + Symbol.N_UNICODE + ' ' + Symbol.EMPTY_UNICODE + ' ' ); entry_symbols_tf.setEditable(false); entry_symbols_tf.setFont( new Font( "Monospaced", Font.PLAIN, entry_alt_chars_tf.getFont().getSize() ) ); entry_help_panel.add(entry_symbols_tf); */ // REALLY SHOULD USE A MARGIN OR AN INSET OR SUCH INSTEAD OF: entry_help_panel.add(new JLabel(" "), BorderLayout.WEST); ArrayList alt_chars = new ArrayList(), symbol_chars = new ArrayList(); alt_chars.add('A'); symbol_chars.add(Symbol.FORALL_UNICODE); alt_chars.add('E'); symbol_chars.add(Symbol.EXISTS_UNICODE); /* NOT PUBLICIZING UNTIL ARRANGE FOR THIS TO APPEAR MORE CLEARLY THIN alt_chars.add(' '); symbol_chars.add(Symbol.THIN_SPACE_UNICODE); */ alt_chars.add('a'); symbol_chars.add(Symbol.AND_UNICODE); alt_chars.add('o'); symbol_chars.add(Symbol.OR_UNICODE); alt_chars.add('n'); symbol_chars.add(Symbol.NOT_UNICODE); alt_chars.add('i'); symbol_chars.add(Symbol.ARROW_RIGHT_ONE_BAR_UNICODE); alt_chars.add('I'); symbol_chars.add(Symbol.ARROW_RIGHT_TWO_BARS_UNICODE); /* alt_chars.add('j'); symbol_chars.add(Symbol.IMPLIES_U_COUNTERCLOCKWISE_UNICODE); */ alt_chars.add('b'); symbol_chars.add(Symbol.ARROW_LEFT_RIGHT_ONE_BAR_UNICODE); alt_chars.add('B'); symbol_chars.add(Symbol.ARROW_LEFT_RIGHT_TWO_BARS_UNICODE); alt_chars.add('='); symbol_chars.add(Symbol.THREE_BAR_UNICODE); alt_chars.add('~'); symbol_chars.add(Symbol.CONGRUENT_UNICODE); /* // BECOMES: alt_chars.add(':'); symbol_chars.add(Symbol.ARROW_LEFT_ONE_BAR_UNICODE); */ alt_chars.add('<'); symbol_chars.add(Symbol.LEQ_UNICODE); alt_chars.add('>'); symbol_chars.add(Symbol.GEQ_UNICODE); alt_chars.add('#'); symbol_chars.add(Symbol.NEQ_UNICODE); alt_chars.add('.'); symbol_chars.add(Symbol.MIDDLE_DOT_UNICODE); alt_chars.add('/'); symbol_chars.add(Symbol.EMPTYSET_UNICODE); alt_chars.add('e'); symbol_chars.add(Symbol.IS_IN_UNICODE); alt_chars.add('r'); symbol_chars.add(Symbol.NOT_IN_UNICODE); alt_chars.add('c'); symbol_chars.add(Symbol.SUBSET_UNICODE); // One might want to switch these two. alt_chars.add('C'); symbol_chars.add(Symbol.SUBSETEQ_UNICODE); alt_chars.add('u'); symbol_chars.add(Symbol.UNION_UNICODE); alt_chars.add('t'); symbol_chars.add(Symbol.INTERSECT_UNICODE); alt_chars.add('-'); symbol_chars.add(Symbol.SUPERSCRIPT_MINUS_UNICODE); alt_chars.add('p'); symbol_chars.add(Symbol.SCRIPT_CAPITAL_P_UNICODE); alt_chars.add('x'); symbol_chars.add(Symbol.TIMES_X_UNICODE); alt_chars.add('['); // |LFLOOR_UNICODE| appears poorly here symbol_chars.add(Symbol.LEFT_LOWER_CORNER_UNICODE); alt_chars.add(']'); // |RFLOOR_UNICODE| appears poorly here symbol_chars.add(Symbol.RIGHT_LOWER_CORNER_UNICODE); alt_chars.add('{'); // |LCEIL_UNICODE| appears poorly here symbol_chars.add(Symbol.LEFT_UPPER_CORNER_UNICODE); alt_chars.add('}'); // |RCEIL_UNICODE| appears poorly here symbol_chars.add(Symbol.RIGHT_UPPER_CORNER_UNICODE); alt_chars.add('O'); symbol_chars.add(Symbol.THETA_UPPERCASE_UNICODE); alt_chars.add('W'); symbol_chars.add(Symbol.OMEGA_UPPERCASE_UNICODE); alt_chars.add('w'); symbol_chars.add(Symbol.OMEGA_LOWERCASE_UNICODE); alt_chars.add('S'); symbol_chars.add(Symbol.SUM_UNICODE); alt_chars.add('P'); symbol_chars.add(Symbol.PROD_UNICODE); alt_chars.add('@'); symbol_chars.add(Symbol.TRIANGLE_FILLED_LEFT_POINTING_UNICODE); alt_chars.add('y'); symbol_chars.add(Symbol.INFINITY_UNICODE); alt_chars.add('N'); symbol_chars.add(Symbol.N_NUMBERS_UNICODE); alt_chars.add('Z'); symbol_chars.add(Symbol.Z_NUMBERS_UNICODE); alt_chars.add('Q'); symbol_chars.add(Symbol.Q_NUMBERS_UNICODE); alt_chars.add('R'); symbol_chars.add(Symbol.R_NUMBERS_UNICODE); //alt_chars.add('X'); symbol_chars.add(Symbol.C_NUMBERS_UNICODE); alt_chars.add('1'); symbol_chars.add(Symbol.SUPERSCRIPT_1_UNICODE); alt_chars.add('2'); symbol_chars.add(Symbol.SUPERSCRIPT_2_UNICODE); alt_chars.add('3'); symbol_chars.add(Symbol.SUPERSCRIPT_3_UNICODE); JPanel chars_symbols_panel = new JPanel(new GridLayout(2, 0)); int char_sym_component_preferred_width = 0; for ( char alt_char : alt_chars ) { JLabel alt_char_label = new JLabel(Character.toString(alt_char)); alt_char_label.setHorizontalAlignment(JLabel.CENTER); char_sym_component_preferred_width = Math.max( char_sym_component_preferred_width, alt_char_label.getPreferredSize().width ); chars_symbols_panel.add(alt_char_label); } chars_symbols_panel.add( new JLabel( "" + Symbol.MIDDLE_DOT_UNICODE + Symbol.MIDDLE_DOT_UNICODE + Symbol.MIDDLE_DOT_UNICODE ) ); // newline for ( final char symbol_char : symbol_chars ) { // On my Mac, buttons had rounded ends which consumed space. JTextField symbol_char_tf = new JTextField(Character.toString(symbol_char)); symbol_char_tf.setEditable(false); symbol_char_tf.addMouseListener( new MouseAdapter() { private String symbol_string = Character.toString(symbol_char); public void mouseReleased(MouseEvent me) { entry_ta.replaceSelection(symbol_string); entry_ta.requestFocusInWindow(); } } ); chars_symbols_panel.add(symbol_char_tf); } chars_symbols_panel.add( new JLabel( "" + Symbol.MIDDLE_DOT_UNICODE + Symbol.MIDDLE_DOT_UNICODE + Symbol.MIDDLE_DOT_UNICODE ) ); entry_help_panel.add(chars_symbols_panel, BorderLayout.CENTER); entry_help_panel.add(new JLabel(" "), BorderLayout.EAST); entry_help_panel.add( new JLabel( " You can also click on any of these symbols" + " to insert it." ), BorderLayout.PAGE_END ); buttons_panel = new JPanel(); content_pane.add(buttons_panel, BorderLayout.PAGE_END); AbstractAction submit_action = new AbstractAction("Submit entry") { public void actionPerformed(ActionEvent ae) { if ( seeking_constant_term ) // I no longer know why I have this code. entry_ta.setText(entry_ta.getText().replace("\n", " ")); // 'outdent' text, i.e. remove common amount of // whitespace at beginnings of lines: String[] text_lines = entry_ta.getText().split("\n"); int common_amt_whitespace_at_fronts = Integer.MAX_VALUE; // textline_preceding String textline_prev = null; for ( String text_line : text_lines ) { int ch_i; // not 'enhanced' |for| because using index later for ( ch_i = 0; ch_i < text_line.length() && ch_i < common_amt_whitespace_at_fronts; ch_i++ ) if ( !Character.isWhitespace(text_line.charAt(ch_i)) || textline_prev != null && text_line.charAt(ch_i) != textline_prev.charAt(ch_i) ) break; common_amt_whitespace_at_fronts = Math.min(ch_i, common_amt_whitespace_at_fronts); textline_prev = text_line; } if ( common_amt_whitespace_at_fronts > 0 ) { String text_outdented = ""; for ( String text_line : text_lines ) text_outdented += text_line.substring( common_amt_whitespace_at_fronts ) + '\n'; entry_ta.setText(text_outdented); } entry_ta.setText(entry_ta.getText().trim()); ; // Considering C++ "ostream os", it's tempting to // use such symbols. ByteArrayOutputStream preserve_em_ba_out = new ByteArrayOutputStream(); try { ((PB_TableModel) table.getModel()) .store_expressionsmgmt( new ObjectOutputStream(preserve_em_ba_out) ); } catch ( IOException ioe ) { ioe.printStackTrace(); return; } try { results = ((PB_TableModel) table.getModel()) .get_expressionsmgmt() .parse_and_further_constrain( entry_ta.getText(), allowing_free_variables, accepting_multiple_exprs, seeking_constant_term, original, original_text ); } // Should I not use |IllegalArgumentException| // as an ~~expected part of the processing? catch ( IllegalArgumentException iae ) { try { ((PB_TableModel) table.getModel()) .restore_expressionsmgmt( new ObjectInputStream( new ByteArrayInputStream( preserve_em_ba_out.toByteArray() ) ) ); } catch ( IOException ioe ) { ioe.printStackTrace(); return; } catch ( Exception e ) { e.printStackTrace(); } String[] error_information = iae.getMessage() .split(Expressions_Mgmt.ERR_POSNS_SEP, 3) ; if ( error_information.length != 3 ) throw iae; int error_begin = Integer.parseInt(error_information[0]), error_end = Integer.parseInt(error_information[1]); if ( error_begin == error_end && error_begin > 0 && entry_ta.getText().charAt(error_begin - 1) == ' ' ) // achieve ~~extra highlighting: // (it's debatable whether this is better than // blinking bar) error_begin--; entry_ta.select(error_begin, error_end); message_ta.setText(error_information[2]); /* message_ta.append( "\n\nunderstood input symbols as follows:\n" + Expression.get_parse_input_symbols_given() ); */ /* JScrollBar scroll_bar; scroll_bar = message_scroll_pane.getHorizontalScrollBar(); scroll_bar.setValue(scroll_bar.getMinimum()); scroll_bar = message_scroll_pane.getVerticalScrollBar(); scroll_bar.setValue(scroll_bar.getMinimum()); */ /* // THE FOLLOWING HASN'T BEEN WORKING: message_scroll_pane.getViewport() .scrollRectToVisible( new Rectangle(0, 0, 1, 1) ); */ /* // WOULD HAVE TO RESIZE WINDOW? message_ta.setRows( error_information[2].split("\n").length ); */ entry_ta.requestFocusInWindow(); results = null; return; } if ( !accepting_multiple_exprs ) { Iterator results_it = results.iterator(); Grammar_Construct result_gc = null; comment_symbol = null; while ( results_it.hasNext() && (result_gc = results_it.next()) instanceof Symbol && (((Symbol) result_gc).get_specifier() == Symbol.Specifier.BREAK || (comment_symbol = (Symbol) result_gc) .get_specifier() == Symbol.Specifier.COMMENT ) ) ; assert result_gc != null : "result_gc != null"; assert result_gc instanceof Expression : "result_gc instanceof Expression"; assert comment_symbol == null || comment_symbol.get_specifier() == Symbol.Specifier.COMMENT : "comment_symbol == null\n" + "|| comment_symbol.get_specifier()" + " == " + "Symbol.Specifier.COMMENT"; result = (Expression) result_gc; } setVisible(false); ((PB_TableModel) table.getModel()) .get_expressionsmgmt().complete_spec_String_map(); } } ; buttons_panel.add(new JButton(submit_action)); AbstractAction cancel_entry_action = new AbstractAction("Cancel entry") { public void actionPerformed(ActionEvent ae) { setVisible(false); } } ; buttons_panel.add(new JButton(cancel_entry_action)); AbstractAction cancel_newproof_action = new AbstractAction("Cancel starting proof") { public void actionPerformed(ActionEvent ae) { System.exit(0); setVisible(false); } } ; cancel_newproof_button = new JButton(cancel_newproof_action); InputMap entry_input_map = entry_ta.getInputMap(); /* * I vaguely recall that somewhere "The JFC Swing Tutorial" says * that ESCAPE may get trapped by something else. * Maybe try a(nother) |KeyListener| for this. * Incidentally, don't want canceling to be too easy to type * (as with CTRL-[ )else would have to ask, * "do you really want to cancel, losing what you've typed?" entry_input_map.put( KeyStroke.getKeyStroke(KeyEvent.VK_ESCAPE, 0), cancel_entry_action ); entry_input_map.put( KeyStroke.getKeyStroke(KeyEvent.VK_X, InputEvent.CTRL_MASK), cancel_newproof_action ); */ entry_input_map.put( KeyStroke.getKeyStroke( KeyEvent.VK_C, InputEvent.CTRL_MASK + InputEvent.SHIFT_MASK ), new AbstractAction() { public void actionPerformed(ActionEvent ae) { if ( !entry_ta.getText().equals("") ) { // Intriguingly, this |StringSelection| appears to be // precisely what's needed to pass to // |Toolkit.getSystemClipboard().setContents()|. java.awt.datatransfer.StringSelection stringselection = new java.awt.datatransfer.StringSelection( entry_ta.getText() ); Toolkit.getDefaultToolkit().getSystemClipboard() .setContents(stringselection, stringselection); } setVisible(false); } } ); entry_input_map.put( KeyStroke.getKeyStroke( KeyEvent.VK_D, InputEvent.CTRL_MASK + InputEvent.SHIFT_MASK ), submit_action ); entry_input_map.put( KeyStroke.getKeyStroke( KeyEvent.VK_Z, InputEvent.CTRL_MASK + InputEvent.SHIFT_MASK ), submit_action ); entry_input_map.put( KeyStroke.getKeyStroke(KeyEvent.VK_B, InputEvent.CTRL_MASK), DefaultEditorKit.backwardAction ); entry_input_map.put( KeyStroke.getKeyStroke(KeyEvent.VK_F, InputEvent.CTRL_MASK), DefaultEditorKit.forwardAction ); entry_input_map.put( KeyStroke.getKeyStroke(KeyEvent.VK_N, InputEvent.CTRL_MASK), DefaultEditorKit.downAction ); entry_input_map.put( KeyStroke.getKeyStroke(KeyEvent.VK_P, InputEvent.CTRL_MASK), DefaultEditorKit.upAction ); entry_input_map.put( KeyStroke.getKeyStroke(KeyEvent.VK_J, InputEvent.CTRL_MASK), DefaultEditorKit.insertBreakAction ); entry_input_map.put( KeyStroke.getKeyStroke(KeyEvent.VK_H, InputEvent.CTRL_MASK), DefaultEditorKit.deletePrevCharAction ); entry_input_map.put( KeyStroke.getKeyStroke(KeyEvent.VK_D, InputEvent.CTRL_MASK), DefaultEditorKit.deleteNextCharAction ); entry_input_map.put( KeyStroke.getKeyStroke(KeyEvent.VK_A, InputEvent.CTRL_MASK), DefaultEditorKit.beginLineAction ); entry_input_map.put( KeyStroke.getKeyStroke(KeyEvent.VK_E, InputEvent.CTRL_MASK), DefaultEditorKit.endLineAction ); entry_input_map.put( KeyStroke.getKeyStroke(KeyEvent.VK_W, InputEvent.CTRL_MASK), DefaultEditorKit.nextWordAction ); entry_input_map.put( KeyStroke.getKeyStroke(KeyEvent.VK_Q, InputEvent.CTRL_MASK), DefaultEditorKit.previousWordAction // ? beginWordAction ? ); /* entry_input_map.put( KeyStroke.getKeyStroke(KeyEvent.VK_A, InputEvent.ALT_MASK), new AbstractAction() { public void actionPerformed(ActionEvent ae) { System.err.println("ae: " + ae); entry_ta.replaceRange( Character.toString(Symbol.FORALL_UNICODE), entry_ta.getSelectionStart(), entry_ta.getSelectionEnd() ); } } ); entry_input_map.put( KeyStroke.getKeyStroke(KeyEvent.VK_N, InputEvent.ALT_MASK), new AbstractAction() { public void actionPerformed(ActionEvent ae) { System.err.println("ae: " + ae); entry_ta.replaceRange( Character.toString(Symbol.NOT_UNICODE), entry_ta.getSelectionStart(), entry_ta.getSelectionEnd() ); } } ); entry_input_map.put( KeyStroke.getKeyStroke(KeyEvent.VK_MINUS, InputEvent.ALT_MASK), new AbstractAction() { public void actionPerformed(ActionEvent ae) { System.err.println("ae: " + ae); entry_ta.replaceRange( Character.toString(Symbol.NOT_UNICODE), entry_ta.getSelectionStart(), entry_ta.getSelectionEnd() ); } } ); . . . */ // DOCUMENTATION: // On my Mac laptop, to avoid interpretation of some keystrokes // such as ALT/OPTION-N, ALT/OPTION-U, ALT/OPTION-E as 'actions', // on my Mac I have to press CTRL as well as ALT/OPTION. entry_ta.addKeyListener( new KeyAdapter() { int altered_key_code; public void keyPressed(KeyEvent ke) { if ( ke.isAltDown() ) altered_key_code = ke.getKeyCode(); } public void keyTyped(KeyEvent ke) { if ( !ke.isAltDown() ) return; char mapped_sym_ch; switch ( altered_key_code ) { // I think it makes the code most consistent if the // cases here are in order according to this program's // material, which means the order of items // in |Symbol.Specifier|. /* case KeyEvent.VK_F: mapped_sym_ch = ke.isShiftDown() // |RFLOOR_UNICODE| appears poorly here ? Symbol.RIGHT_LOWER_CORNER_UNICODE // |LFLOOR_UNICODE| appears poorly here : Symbol.LEFT_LOWER_CORNER_UNICODE; break; */ /* case KeyEvent.VK_C: mapped_sym_ch = ke.isShiftDown() // |RCEIL_UNICODE| appears poorly here ? Symbol.RIGHT_UPPER_CORNER_UNICODE // |LCEIL_UNICODE| appears poorly here : Symbol.LEFT_UPPER_CORNER_UNICODE; break; */ case KeyEvent.VK_A: mapped_sym_ch = ke.isShiftDown() ? Symbol.FORALL_UNICODE : Symbol.AND_UNICODE; break; case KeyEvent.VK_E: if ( !ke.isShiftDown() ) { mapped_sym_ch = Symbol.IS_IN_UNICODE; break; } mapped_sym_ch = Symbol.EXISTS_UNICODE; break; case KeyEvent.VK_EQUALS: case KeyEvent.VK_PLUS: mapped_sym_ch = ke.isShiftDown() ? Symbol.SUM_UNICODE : Symbol.THREE_BAR_UNICODE; break; case KeyEvent.VK_B: mapped_sym_ch = ke.isShiftDown() ? Symbol.ARROW_LEFT_RIGHT_TWO_BARS_UNICODE : Symbol.ARROW_LEFT_RIGHT_ONE_BAR_UNICODE; break; case KeyEvent.VK_I: mapped_sym_ch = ke.isShiftDown() ? Symbol.ARROW_RIGHT_TWO_BARS_UNICODE : Symbol.ARROW_RIGHT_ONE_BAR_UNICODE; break; case KeyEvent.VK_J: mapped_sym_ch = Symbol.IMPLIES_U_COUNTERCLOCKWISE_UNICODE; break; case KeyEvent.VK_O: mapped_sym_ch = ke.isShiftDown() ? Symbol.THETA_UPPERCASE_UNICODE : Symbol.OR_UNICODE; break; case KeyEvent.VK_COLON: case KeyEvent.VK_SEMICOLON: if ( ke.isShiftDown() ) { mapped_sym_ch = Symbol.ARROW_LEFT_ONE_BAR_UNICODE; break; } return; case KeyEvent.VK_QUOTE: case KeyEvent.VK_QUOTEDBL: if ( !ke.isShiftDown() ) { mapped_sym_ch = Symbol.PRIME_UNICODE; break; } return; case KeyEvent.VK_U: mapped_sym_ch = Symbol.UNION_UNICODE; break; case KeyEvent.VK_T: mapped_sym_ch = Symbol.INTERSECT_UNICODE; break; case KeyEvent.VK_X: mapped_sym_ch = Symbol.TIMES_X_UNICODE; break; case KeyEvent.VK_1: mapped_sym_ch = ke.isShiftDown() && ke.isControlDown() ? Symbol.SUBSCRIPT_1_UNICODE : Symbol.SUPERSCRIPT_1_UNICODE; break; case KeyEvent.VK_2: case KeyEvent.VK_AT: mapped_sym_ch = ke.isShiftDown() ? (ke.isControlDown() ? Symbol.SUBSCRIPT_2_UNICODE : Symbol .TRIANGLE_FILLED_LEFT_POINTING_UNICODE ) : Symbol.SUPERSCRIPT_2_UNICODE; break; case KeyEvent.VK_3: mapped_sym_ch = ke.isShiftDown() ? (ke.isControlDown() ? Symbol.SUBSCRIPT_3_UNICODE : Symbol.NEQ_UNICODE ) : Symbol.SUPERSCRIPT_3_UNICODE; break; case KeyEvent.VK_D: mapped_sym_ch = ke.isShiftDown() ? Symbol.NEQ_UNICODE // "*d*ifferent" : Symbol.MIDDLE_DOT_UNICODE; break; case KeyEvent.VK_4: mapped_sym_ch = Symbol.SUPERSCRIPT_4_UNICODE; break; case KeyEvent.VK_5: mapped_sym_ch = Symbol.SUPERSCRIPT_5_UNICODE; break; case KeyEvent.VK_6: mapped_sym_ch = Symbol.SUPERSCRIPT_6_UNICODE; break; case KeyEvent.VK_7: mapped_sym_ch = Symbol.SUPERSCRIPT_7_UNICODE; break; case KeyEvent.VK_ASTERISK: case KeyEvent.VK_8: mapped_sym_ch = ke.isShiftDown() ? Symbol.PROD_UNICODE : Symbol.SUPERSCRIPT_8_UNICODE; break; case KeyEvent.VK_LEFT_PARENTHESIS: case KeyEvent.VK_9: mapped_sym_ch = ke.isShiftDown() ? Symbol.SUBSET_UNICODE : Symbol.SUPERSCRIPT_9_UNICODE; break; /* case KeyEvent.VK_RIGHT_PARENTHESIS: case KeyEvent.VK_0: mapped_sym_ch = ke.isShiftDown() ? Symbol.SUPERSET_UNICODE : Symbol.SUPERSCRIPT_0_UNICODE; break; */ case KeyEvent.VK_0: mapped_sym_ch = Symbol.SUPERSCRIPT_0_UNICODE; break; case KeyEvent.VK_MINUS: mapped_sym_ch = Symbol.SUPERSCRIPT_MINUS_UNICODE; break; case KeyEvent.VK_OPEN_BRACKET: mapped_sym_ch = ke.isShiftDown() // |LCEIL_UNICODE| appears poorly here ? Symbol.LEFT_UPPER_CORNER_UNICODE // |LFLOOR_UNICODE| appears poorly here : Symbol.LEFT_LOWER_CORNER_UNICODE; break; case KeyEvent.VK_CLOSE_BRACKET: mapped_sym_ch = ke.isShiftDown() // |RCEIL_UNICODE| appears poorly here ? Symbol.RIGHT_UPPER_CORNER_UNICODE // |RFLOOR_UNICODE| appears poorly here : Symbol.RIGHT_LOWER_CORNER_UNICODE; break; case KeyEvent.VK_SPACE: mapped_sym_ch = Symbol.THIN_SPACE_UNICODE; break; case KeyEvent.VK_LESS: case KeyEvent.VK_COMMA: if ( !ke.isShiftDown() ) return; case KeyEvent.VK_L: mapped_sym_ch = Symbol.LEQ_UNICODE; break; case KeyEvent.VK_GREATER: case KeyEvent.VK_PERIOD: mapped_sym_ch = ke.isShiftDown() ? Symbol.GEQ_UNICODE : Symbol.MIDDLE_DOT_UNICODE; break; case KeyEvent.VK_G: mapped_sym_ch = Symbol.GEQ_UNICODE; break; /* case KeyEvent.VK_X: //if ( ke.isShiftDown() ) { mapped_sym_ch = Symbol.C_NUMBERS_UNICODE; break; //} //return; */ case KeyEvent.VK_R: mapped_sym_ch = ke.isShiftDown() ? Symbol.R_NUMBERS_UNICODE : Symbol.NOT_IN_UNICODE; break; case KeyEvent.VK_Q: if ( ke.isShiftDown() ) { mapped_sym_ch = Symbol.Q_NUMBERS_UNICODE; break; } return; case KeyEvent.VK_Z: if ( ke.isShiftDown() ) { mapped_sym_ch = Symbol.Z_NUMBERS_UNICODE; break; } return; case KeyEvent.VK_N: mapped_sym_ch = ke.isShiftDown() ? Symbol.N_NUMBERS_UNICODE : Symbol.NOT_UNICODE; break; case KeyEvent.VK_S: mapped_sym_ch = Symbol.SUM_UNICODE; break; case KeyEvent.VK_P: mapped_sym_ch = ke.isShiftDown() ? Symbol.PROD_UNICODE : Symbol.SCRIPT_CAPITAL_P_UNICODE; break; case KeyEvent.VK_W: mapped_sym_ch = ke.isShiftDown() ? Symbol.OMEGA_UPPERCASE_UNICODE : Symbol.OMEGA_LOWERCASE_UNICODE; break; /* case KeyEvent.VK_O: if ( !ke.isShiftDown() ) return; case KeyEvent.VK_H: mapped_sym_ch = Symbol.THETA_UPPERCASE_UNICODE; break; */ case KeyEvent.VK_BACK_QUOTE: if ( !ke.isShiftDown() ) return; mapped_sym_ch = Symbol.CONGRUENT_UNICODE; break; case KeyEvent.VK_H: mapped_sym_ch = Symbol.THETA_UPPERCASE_UNICODE; break; case KeyEvent.VK_C: mapped_sym_ch = ke.isShiftDown() ? Symbol.SUBSETEQ_UNICODE : Symbol.SUBSET_UNICODE; break; case KeyEvent.VK_SLASH: if ( !ke.isShiftDown() ) { mapped_sym_ch = Symbol.EMPTYSET_UNICODE; break; } return; case KeyEvent.VK_Y: mapped_sym_ch = Symbol.INFINITY_UNICODE; break; default: return; } entry_ta.replaceRange(Character.toString(mapped_sym_ch), entry_ta.getSelectionStart(), entry_ta.getSelectionEnd() ); ke.consume(); } } ); //final Action pasteAction = new DefaultEditorKit.PasteAction(); entry_ta.addMouseListener( new MouseAdapter() { public void mouseReleased(MouseEvent me) { if ( me.getButton() == MouseEvent.BUTTON3 ) /* { // Some things have |fireActionPerformed()| // but would require an |ActionEvent| anyway. pasteAction.actionPerformed( new ActionEvent(me.getSource(), me.getID(), null) ); } */ entry_ta.paste(); } } ); pack(); } private void start_user_entry(String init_text) { entry_ta.setText(init_text); // modal so |setVisible(true)| won't return until finished // sometimes components weren't appearing, // so temporarily make this not modal // so below |setVisible(true)| returns // and then |paintComponents(getGraphics())|. //setModal(false); results = null; result = null; comment_symbol = null; /* ~~flame on * My opinion is that having the key steps being * here |setVisible(true)| and in actions |setVisible(false)| * (and |return| without that in an action letting this continue) * is not clear coding. But this seems to be necessary. */ setVisible(true); //paintComponents(getGraphics()); //setModal(true); } private void start_user_entry() { start_user_entry(""); } void get_theorem(boolean starting_new_proof) { PB_TableModel table_model = (PB_TableModel) table.getModel(); //table_model.get_expressionsmgmt().prep_for_user_to_spec_Strings(); //theorem_vs_presuppositions = true; message_ta.setText( "In the panel below, enter formula for theorem to be proved:" + "\n(Remember, you can copy/paste from Web pages, MS Word, PDF, etc.)" ); if ( starting_new_proof ) buttons_panel.add(cancel_newproof_button); start_user_entry(); if ( starting_new_proof ) buttons_panel.remove(cancel_newproof_button); if ( result == null ) return; //table_model.get_expressionsmgmt().complete_spec_String_map(); table_model.get_expressionsmgmt().consider_usingtildefornot(result); table_model.get_expressionsmgmt().consider_usingprimefornot(result); table_model .add( PB_TableModel.Column_ID.GOALS, "We start working with the formula being proved" + "\nas follows:", comment_symbol != null ? comment_symbol.get_comment_content() : null, entry_ta.getText(), result ); // on my Mac with Java 1.5.0_06-112, // weird things happened when tried listening // for |TableModelEvent.INSERT| and doing // |setRowSelectionInterval()| then table.setRowSelectionInterval( table_model.get_addedrowindex(), table_model.get_addedrowindex() ); // THE FOLLOWING HASN'T BEEN WORKING: table.scrollRectToVisible( table.getCellRect( table_model.get_addedrowindex(), table.convertColumnIndexToView( PB_TableModel.Column_ID.GOALS .ordinal() ), true ) ); } void get_theorem() { get_theorem(true); } void get_presuppositions() { PB_TableModel table_model = (PB_TableModel) table.getModel(); //theorem_vs_presuppositions = false; message_ta.setText( "Enter presuppositions in the panel below:" + "\n(Remember, you can copy/paste from Web pages, MS Word, PDF, etc.)" ); accepting_multiple_exprs = true; start_user_entry(); accepting_multiple_exprs = false; if ( results == null ) return; comment_symbol = null; int first_added_row_i = -1; for ( Grammar_Construct result_gc : results ) { if ( result_gc instanceof Symbol ) { Symbol result_symbol = (Symbol) result_gc; if ( result_symbol.get_specifier() == Symbol.Specifier.BREAK ) continue; comment_symbol = result_symbol; assert comment_symbol.get_specifier() == Symbol.Specifier.COMMENT : "comment_symbol.get_specifier()" + " == Symbol.Specifier.COMMENT"; continue; } Expression result_expr = (Expression) result_gc; int begin = result_expr.get_begin(); result_expr.context_shift(-begin); table_model.get_expressionsmgmt() .consider_usingtildefornot(result_expr); table_model.get_expressionsmgmt() .consider_usingprimefornot(result_expr); table_model .add( PB_TableModel.Column_ID.SUPPS, first_added_row_i == -1 ? "We presuppose the following:" : null, comment_symbol != null ? comment_symbol.get_comment_content() : null, entry_ta .getText() .substring( begin, begin + result_expr.get_limit() ), result_expr ); comment_symbol = null; if ( first_added_row_i == -1 ) first_added_row_i = table_model.get_addedrowindex(); } // on my Mac with Java 1.5.0_06-112, // weird things happened when tried listening // for |TableModelEvent.INSERT| and doing // |setRowSelectionInterval()| then table.setRowSelectionInterval( first_added_row_i, first_added_row_i ); // THE FOLLOWING HASN'T BEEN WORKING: table.scrollRectToVisible( table.getCellRect( first_added_row_i, table.convertColumnIndexToView( PB_TableModel.Column_ID.SUPPS .ordinal() ), true ) ); } LinkedList get_constant_terms_to_assign_to(String vars_texts) { boolean multiple = vars_texts.contains(","); String mult = multiple ? "s" : ""; message_ta.setText( "In the panel below, enter the constant term" + mult + " that you want to" + " assign to the variable" + mult + " \"" + vars_texts + '\"' + (multiple ? ",\nwith commas (\",\") separating the terms" : "" ) + ':' + "\n(Remember, you can copy/paste material \u2014" + " such as " + (multiple ? "" : "an") + " expression" + mult + " copied from your proof.)" ); seeking_constant_term = true; start_user_entry(); seeking_constant_term = false; // Consider accepting multiple expressions // instead of requiring using commas to separate // (but still request commas). return result == null ? null : result.multiary_op_args(Symbol.Specifier.COMMA); } Expression obtain_smply_eq_rplcmnt(Expression orig, String orig_text) { original = orig; original_text = orig_text; message_ta.setText( "In the panel below, enter " + "your simple-algebra equivalent replacement" + "\nfor the expression \"" + original_text + "\":" + "\n(Remember, you can copy/paste material \u2014" + " such as an expression copied from your proof.)" ); allowing_free_variables = true; start_user_entry(original_text); allowing_free_variables = false; original = null; original_text = null; return result; } String get_entered_text() { return entry_ta.getText(); } void set_fontsizes(float fontsize) { message_ta.setFont(message_ta.getFont().deriveFont(fontsize)); entry_ta.setFont(entry_ta.getFont().deriveFont(fontsize)); pack(); } }