/* 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.awt.print.*; import javax.swing.*; import javax.swing.event.*; import javax.swing.filechooser.FileFilter; import java.io.*; import java.util.*; import javax.swing.table.*; import javax.swing.text.*; import java.text.*; // Having the name of the overall program be more conventional // will hopefully help this product be more widely acceptable. // This class doesn't extend |JFrame| // because future version may allow more than one proof // open at a time, in which case each |Proof| or |Tableau| // should be a |JFrame|, not this application. /** * Facilitates building proofs (main code). * @author Hugh McGuire */ class ProofBuilder { public static void main(String[] args) throws IOException { System.out.println( "ProofBuilder Copyright (C) 2008 Hugh McGuire" + "\nThis program comes with ABSOLUTELY NO WARRANTY." + "\nThis is free software, and you are welcome to redistribute it" + "\nunder certain conditions." + "\nFor details, see documentation with this program." + '\n' ); System.out.println( "You can obtain help from the manual or email" + "\nwhich are accessible as follows:" + "\n http://www.cis.gvsu.edu/~mcguire/ProofBuilder/manual/" + "\n mcguire@cis.gvsu.edu" + '\n' ); if ( args.length > 0 ) { String[] no_args_msg = { "ProofBuilder takes no arguments.", // this version "Were you trying to enable assertions?", "For that, position \"-ea\" immediately following \"java\".", args[0].equals("ProofBuilder") ? "And after specifying \"ProofBuilder.jar\", you *don't*" + " need to specify \"ProofBuilder\" again." : "" }; Toolkit.getDefaultToolkit().beep(); for ( String nam : no_args_msg ) System.err.println(nam); JOptionPane.showMessageDialog( null, no_args_msg, "ProofBuilder takes no arguments", JOptionPane.ERROR_MESSAGE ); System.exit(1); } //Schedule a job for the event-dispatching thread: //creating and showing this application's GUI. javax.swing.SwingUtilities.invokeLater( new Runnable() { public void run() { new ProofBuilder() .createAndShowGUI(); } } ); } // static boolean dont_collect_terms; // static String preferences; private String preferences_lc = ""; private JFrame frame; private PB_TableModel table_model; // CONSIDER avoiding maintaining variable |table_model| to // facilitate resetting table's model (data) or such administration // such as when might have multiple proofs open simultaneously. // See also |Ded_Action.table_model()|. private JTable table; private User_Entry_Dialog user_entry_dialog; private long time_of_last_save; private JSplitPane main_splitpane; private JTextPane head_theorem_textpane; private String username; private JScrollPane table_scroll_pane; private JMenuBar menu_bar; private JMenu deductions_menu; private float fontsize_original; private int fontsizefactor_i; private JMenuItem entertheorem_menuitem = new JMenuItem("Enter theorem"); private JCheckBoxMenuItem usetildefornot_menuitem = // e.g. Epp new JCheckBoxMenuItem("Use " + Symbol.TILDE_ASCII + " for NOT"); private JCheckBoxMenuItem useprimefornot_menuitem = // e.g. Gersting new JCheckBoxMenuItem("Use " + Symbol.PRIME_UNICODE + " for NOT"); private Deduction_Prep[] deduction_preps; private static final float[] FONT_SIZE_FACTORS_SUPPORTED = {0.5F, 0.75F, 0.8F, 0.9F, 1F, 1.2F, 1.5F, 2F}; // I've noticed that initially menu font size is 14 and others 12 static final float MENU_FONTSIZE_FACTOR = 1.17F; /** * Create the GUI and show it. For thread safety, * this method should be invoked from the * event-dispatching thread. */ void createAndShowGUI() { // Request nice window decorations: JFrame.setDefaultLookAndFeelDecorated(true); frame = new JFrame("ProofBuilder"); frame.setDefaultCloseOperation(JFrame.DO_NOTHING_ON_CLOSE); // should catch frame.addWindowListener( new WindowAdapter() { public void windowClosing(WindowEvent we) { if ( discard_modifications_since_save() ) System.exit(0); } } ); //super(new GridLayout(1,0)); System.out.print("checking for preferences..."); try { File prefs_file = new File("PBprefs.txt"); // Somewhat intriguingly to me, the preceding line of code // generally doesn't throw an exception. I guess it just // creates a representation of the pathname for the file, // it doesn't actually try to do anything with the file. // the necessity for this cast amuses me char[] prefs_ch = new char[(int) prefs_file.length()]; new FileReader(prefs_file) .read(prefs_ch, 0, prefs_ch.length); System.out.print(" handling preferences..."); preferences_lc = new String(prefs_ch) .toLowerCase(); /* java.util.Scanner prefs_scanner = new java.util.Scanner(new java.io.File("PBprefs.txt")); while ( prefs_scanner.hasNextLine() ) { String preference = prefs_scanner.nextLine(); Expression.use_prime_for_not |= preferences.contains("useprimefornot"); PB_TableModel.hilbert_style |= preferences.contains("hilbertstyle"); } */ /* use_prime_for_not |= preferences.contains("useprimefornot"); PB_TableModel.hilbert_style |= preferences.contains("hilbertstyle"); */ } /* catch ( java.io.FileNotFoundException filenotfoundexception ) { // in this case do nothing } */ catch ( java.io.IOException ioe ) { // in this case do nothing } System.out.println("\nfinished checking preferences\n"); System.out.print("preparing table..."); /* JPanel head_panel = new JPanel(new BorderLayout()); JLabel head_label = new JLabel(PB_TableModel.head_text); head_label.setFont(head_label.getFont().deriveFont(Font.BOLD)); head_panel.add(head_label, BorderLayout.PAGE_START); */ head_theorem_textpane = new JTextPane(); head_theorem_textpane.setEditable(false); /* int h = head_theorem_textpane.getFontMetrics( head_theorem_textpane.getFont() ) .getHeight(); head_theorem_textpane.setMargin(new Insets(h/2, h*2, h, 0)); */ //head_panel.add(head_theorem_textpane, BorderLayout.CENTER); table = new JTable(table_model = new PB_TableModel(preferences_lc)); fontsize_original = (float) Math.max( table.getFont().getSize2D(), head_theorem_textpane.getFont().getSize2D() ); if ( fontsize_original > table.getFont().getSize2D() ) table.setFont(table.getFont().deriveFont(fontsize_original)); // assert (FONT_SIZE_FACTORS_SUPPORTED) fontsizefactor_i = Arrays.binarySearch(FONT_SIZE_FACTORS_SUPPORTED, 1F); assert fontsizefactor_i >= 0 : "fontsizefactor_i >= 0"; // Scrolling the header with the table didn't work --- I wasn't seeing // the table header; but actually this was because // I overlooked the fact (as mentioned in "The JFC Swing Tutorial") // that I was supposed to get the table-header separately and // display it myself if the table wasn't directly inside // a |JScrollPane|. // Anyway, it makes sense that Java would discourage what I was trying // since one should want a table's header to remain // while the rows are scrolled. //frame.getContentPane().add(new JScrollPane(table), BorderLayout.CENTER); table_scroll_pane = new JScrollPane(table); main_splitpane = new JSplitPane(JSplitPane.VERTICAL_SPLIT, head_theorem_textpane, table_scroll_pane ); main_splitpane.setOneTouchExpandable(true); frame.setContentPane(main_splitpane); table.setPreferredScrollableViewportSize(new Dimension(1000, 500)); /* * Doing this made the table not display anything past 500: table.setPreferredSize(new Dimension(1000, 500)); */ //table.setAutoResizeMode(JTable.AUTO_RESIZE_NEXT_COLUMN); //table.getTableHeader().setReorderingAllowed(false); table.setRowMargin(table.getRowMargin() + 2); table.setShowVerticalLines(false); // seems silly but needed on my Mac through 2007: if ( table.getGridColor().equals(Color.WHITE) ) table.setGridColor(Color.LIGHT_GRAY); table.setDefaultRenderer(Entry.class, new Entry.Renderer(/*table*/)); table.setDefaultEditor(Entry.class, new Entry.Editor()); final TableCellRenderer string_renderer_default = table.getDefaultRenderer(String.class); table.setDefaultRenderer( String.class, new TableCellRenderer() { public Component getTableCellRendererComponent( JTable table, Object String_o, boolean isSelected, boolean hasFocus, int row, int column ) { Component rendererComponent = string_renderer_default .getTableCellRendererComponent( table, String_o, isSelected, hasFocus, row, column ); if ( column == PB_TableModel.Column_ID.COMMENTS.ordinal() ) rendererComponent.setFont( rendererComponent.getFont().deriveFont(Font.ITALIC) ); return rendererComponent; } } ); final Color UNUSED_BACKGROUND_COLOR = Color.BLUE; // Color.ORANGE // GREEN.brighter().brighter(); // ORANGE.darker() // regular |ORANGE| // appeared more golden, // conflicting with // color used to highlight // |Boolean| renderer given draws 'false' box when |null|; to avoid: final TableCellRenderer boolean_renderer_default = table.getDefaultRenderer(Boolean.class); table.setDefaultRenderer( Boolean.class, new TableCellRenderer() { private Component blank_used = new JLabel(); private Boolean Boolean_false = new Boolean(false); private Boolean Boolean_true = new Boolean(true); public Component getTableCellRendererComponent( JTable table, Object Boolean_o, boolean isSelected, boolean hasFocus, int row, int column ) { if ( Boolean_o == null ) return blank_used; boolean used_wrt_selected_rows = table_model.used_wrt_selected_rows( row, table.getSelectedRows() ); Component used_box = boolean_renderer_default .getTableCellRendererComponent( table, used_wrt_selected_rows ? Boolean_true : Boolean_false, isSelected, hasFocus, row, column ); if ( !isSelected && !used_wrt_selected_rows ) used_box.setBackground(UNUSED_BACKGROUND_COLOR); return used_box; } } ); set_columns_widths(); /* on my Mac with Java 1.5.0_06-112, * though immediately only the one row gets * selected, later the next row-index also appears selected table.getModel().addTableModelListener( new TableModelListener() { public void tableChanged(TableModelEvent table_model_event) { / * table.clearSelection(); table.setRowSelectionInterval( table_model.get_newrowi(), table_model.get_newrowi() ); * / if ( table_model_event.getType() == TableModelEvent.INSERT ) { System.err.println("table_model_event.getFirstRow() : " + table_model_event.getFirstRow() ); System.err.println("table_model_event.getLastRow() : " + table_model_event.getLastRow() ); table.setRowSelectionInterval( table_model_event.getFirstRow(), table_model_event.getLastRow() ); System.err.println("table.getSelectedRowCount() : " + table.getSelectedRowCount() ); } } } ); */ //frame.getContentPane().add(new JScrollPane(table), BorderLayout.CENTER); System.out.println("\nfinished table\n"); //System.out.println("preparing user-entry dialog..."); user_entry_dialog = new User_Entry_Dialog(table); //Create and set up the menu bar: System.out.print("preparing menu bar..."); menu_bar = new JMenuBar(); AbstractAction not_yet_impl_action = new AbstractAction() { public void actionPerformed(ActionEvent event) { JOptionPane.showMessageDialog( frame, "That operation has not yet been implemented; sorry." ); } } ; // temporary variables: JMenu menu; JMenuItem menu_item; menu = new JMenu(getClass().getName()); menu.setMnemonic(menu.getText().charAt(0)); /* menu_item = new JMenuItem(... "Preferences..." ...); menu.add(menu_item); menu.addSeparator(); menu_item = new JMenuItem(... "Quit" + getClass().getName() ...); menu.add(menu_item); */ // See basic information about ... menu_item = new JMenuItem("About " + getClass().getName()); menu_item.addActionListener( new AbstractAction() { Object[] info_objs = { "ProofBuilder version 0.3, 2008", "by Hugh McGuire", "You can obtain help from the manual or email" + "\nwhich are accessible as follows:", // using |JTextField| so users can copy the texts: new JTextField("http://www.cis.gvsu.edu/~mcguire/ProofBuilder/manual/"), new JTextField("mcguire@cis.gvsu.edu") }; public void actionPerformed(ActionEvent ae) { for ( Object info_obj : info_objs ) if ( info_obj instanceof JTextField ) ((JTextField) info_obj).setEditable(false); JOptionPane.showMessageDialog( frame, info_objs, ((JMenuItem) ae.getSource()).getText(), JOptionPane.PLAIN_MESSAGE ); } } ); menu.add(menu_item); menu_item = new JMenuItem("View copyright and license (etc.)"); menu_item.addActionListener( new AbstractAction() { final String[] message = { "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", " " }; public void actionPerformed(ActionEvent ae) { JOptionPane.showMessageDialog( frame, message, ((JMenuItem) ae.getSource()).getText(), JOptionPane.PLAIN_MESSAGE ); } } ); menu.add(menu_item); menu.addSeparator(); menu_item = new JMenuItem("Quit ProofBuilder"); // "Exit" menu_item.addActionListener( new AbstractAction() { public void actionPerformed(ActionEvent event) { if ( discard_modifications_since_save() ) System.exit(0); } } ); menu_item.setMnemonic(KeyEvent.VK_Q); menu_item.setAccelerator( KeyStroke.getKeyStroke( KeyEvent.VK_Q, ActionEvent.CTRL_MASK | ActionEvent.SHIFT_MASK ) ); menu.add(menu_item); menu_bar.add(menu); menu = new JMenu("System"); // "System Actions" / "File" menu.setMnemonic(menu.getText().charAt(0)); final JFileChooser file_chooser = new JFileChooser(System.getProperty("user.dir")); file_chooser.addChoosableFileFilter( new FileFilter() { public boolean accept(File f) { if ( f.isDirectory() ) return true; String suffix_lc = suffix_lowercase(f.getName()); return suffix_lc.equals("pb") /* suffix_lc.equals("prf") || suffix_lc.equals("prms") // premises || suffix_lc.equals("txt") // premises */ || suffix_lc.equals("html") || suffix_lc.equals("htm"); } public String getDescription() { return "Just Webpages" + " and files in ProofBuilder's native format"; } } ); /* file_chooser.setSelectedFile( new File(file_chooser.getCurrentDirectory(), "TITLE.html") ); */ /* final JCheckBoxMenuItem assume_nonneg_int_vars_menuitem = //new JCheckBoxMenuItem("Assume nonnegative integer variables"); new JCheckBoxMenuItem( "Assume domain " + Symbol.N_NUMBERS_UNICODE + ", nonnegative integers" ); */ // Apply final JMenuItem induct_menuitem = new JMenuItem("Invoke induction"); menu_item = new JMenuItem("New proof"); menu_item.setMnemonic(KeyEvent.VK_N); menu_item.setAccelerator( KeyStroke.getKeyStroke( KeyEvent.VK_N, ActionEvent.CTRL_MASK + ActionEvent.SHIFT_MASK ) ); menu_item.addActionListener( new AbstractAction() { public void actionPerformed(ActionEvent event) { if ( !discard_modifications_since_save() ) return; try { head_theorem_textpane.getStyledDocument() .remove( 0, head_theorem_textpane.getStyledDocument() .getLength() ); } catch ( BadLocationException e ) { e.printStackTrace(); } time_of_last_save = 0; //table_model.get_expressionsmgmt().clear_identifiers(); table.setModel( table_model = new PB_TableModel(preferences_lc) ); set_columns_widths(); entertheorem_menuitem.setEnabled(true); /* assume_nonneg_int_vars_menuitem.setEnabled(true); assume_nonneg_int_vars_menuitem.setSelected(false); */ user_entry_dialog.get_theorem(); setthings_if_havetheorem(); } } ); menu.add(menu_item); menu.addSeparator(); // "Reset username" // "Specify username" // "Update username" menu_item = new JMenuItem("Set title"); final Action settitle_action = new AbstractAction() { public void actionPerformed(ActionEvent event) { String new_title = (String) JOptionPane.showInputDialog( frame, "Set title for document:", event.getActionCommand(), JOptionPane.PLAIN_MESSAGE, null, null, table_model.get_title() != PB_TableModel.DEFAULT_TITLE ? table_model.get_title() : "" ); // The documentation for // |JOptionPane.showInputDialog(Object message, Object initialSelectionValue)| // didn't clearly show this, but apparently (considering // documentation of other methods of |JOptionPane|) // it returns |null| if the user chooses "Cancel"; hence: if ( new_title != null && !new_title.equals("") ) { table_model.set_title(new_title); frame.setTitle(new_title); } } }; menu_item.addActionListener(settitle_action); menu.add(menu_item); // "Reset username" // "Specify username" // "Update username" menu_item = new JMenuItem("Update username"); menu_item.addActionListener( new AbstractAction() { public void actionPerformed(ActionEvent event) { String new_username = JOptionPane.showInputDialog( event.getActionCommand() + ':', System.getProperty("user.name") ); // The documentation for // |JOptionPane.showInputDialog(Object message, Object initialSelectionValue)| // didn't clearly show this, but apparently (considering // documentation of other methods of |JOptionPane|) // it returns |null| if the user chooses "Cancel"; hence: if ( new_username != null ) username = new_username; } } ); menu.add(menu_item); menu_item = new JMenuItem("Save as Web page"); menu_item.addActionListener( new AbstractAction() { public void actionPerformed(ActionEvent event) { if ( table_model.get_title() == table_model.DEFAULT_TITLE ) settitle_action.actionPerformed(event); if ( username == null ) username = JOptionPane.showInputDialog( "Please ensure username is accurate:", System.getProperty("user.name") ); if ( username == null ) return; File file; /* File file = file_chooser.getSelectedFile(); if ( file == null ) */ file_chooser.setSelectedFile( new File( file_chooser.getCurrentDirectory(), table_model.get_filenamebase() + ".html" ) ); /* else if ( time_of_last_save > 0 && suffix_lowercase(file.getName()).equals("pb") ) file_chooser.setSelectedFile( new File( PB_TableModel.basename(file.getName()) + ".html" ) ); */ for ( ; ; ) { if ( file_chooser.showSaveDialog(frame) != JFileChooser.APPROVE_OPTION ) return; file = file_chooser.getSelectedFile(); String suffix_lc = suffix_lowercase(file.getName()); if ( suffix_lc.equals("html") || suffix_lc.equals("htm") ) break; Toolkit.getDefaultToolkit().beep(); JOptionPane.showMessageDialog( frame, "For a Web-page, the file name should end" + " with \".html\" or \".htm\".", "Web-page file name should end \".html\" or \".htm\"", JOptionPane.ERROR_MESSAGE ); } // assert file != null : "file != null"; try { table_model.set_filenamebase(file.getName()); FileWriter file_writer = new FileWriter(file); file_writer.write( "\n\n" + "\n\n\n" + "\n\n\n" + "\n" + table_model.get_title() + "\n\n\n\n\n\n" + "

\n" ); Entry.output_as_HTML( file_writer, table_model.get_title() ); file_writer.write( "\n

\n\n" + "

\n" ); Entry.output_as_HTML(file_writer, username); file_writer.write( "\n

\n\n" ); table_model.output_as_HTML(file_writer); file_writer.write("\n\n\n\n"); file_writer.close(); time_of_last_save = System.currentTimeMillis(); } catch ( IOException e ) { e.printStackTrace(); } } } ); menu_item.setMnemonic(KeyEvent.VK_S); menu_item.setAccelerator( KeyStroke.getKeyStroke( KeyEvent.VK_S, ActionEvent.CTRL_MASK | ActionEvent.SHIFT_MASK ) ); menu.add(menu_item); menu.addSeparator(); // temporarily // in intermediate form // raw // binary // natively // native form // in native format // in native format file // native format // using native format // current state of proof menu_item = new JMenuItem("Save current state of proof"); menu_item.addActionListener( new AbstractAction() { public void actionPerformed(ActionEvent event) { if ( table_model.get_title() == table_model.DEFAULT_TITLE ) settitle_action.actionPerformed(event); File file; /* File file = file_chooser.getSelectedFile(); if ( file == null ) */ file_chooser.setSelectedFile( new File( file_chooser.getCurrentDirectory(), table_model.get_filenamebase() + ".pb" ) ); /* else if ( time_of_last_save > 0 && (suffix_lowercase(file.getName()).equals("html") || suffix_lowercase(file.getName()) .equals("htm") ) ) file_chooser.setSelectedFile( new File( PB_TableModel.basename(file.getName()) + ".pb" ) ); */ for ( ; ; ) { if ( file_chooser.showSaveDialog(frame) != JFileChooser.APPROVE_OPTION ) return; file = file_chooser.getSelectedFile(); String suffix_lc = suffix_lowercase(file.getName()); if ( suffix_lc.equals("pb") ) break; Toolkit.getDefaultToolkit().beep(); JOptionPane.showMessageDialog( frame, "To save current state," + " use a file name ending" + " with \".pb\" (or \".PB\".)", "Current-state file name should end \".pb\" (or \".PB\")", JOptionPane.ERROR_MESSAGE ); } // assert file != null : "file != null"; try { table_model.set_filenamebase(file.getName()); ObjectOutputStream object_output = new ObjectOutputStream(new FileOutputStream(file)); /* object_output.writeObject(table_model); // |ObjectOutputStream.writeObject(PB_TableModel)| encountered difficulties, // I think because |PB_TableModel extends AbstractTableModel| which // contains |TableModelListener|s which includes the |JTable| which // (among other problems) uses a |SizeSequence| which was not |Serializable| // . */ table_model.output_native(object_output); object_output.close(); time_of_last_save = System.currentTimeMillis(); } catch ( IOException e ) { e.printStackTrace(); } } } ); /* menu_item.setMnemonic(KeyEvent.VK_S); menu_item.setAccelerator( KeyStroke.getKeyStroke( KeyEvent.VK_S, ActionEvent.CTRL_MASK | ActionEvent.SHIFT_MASK ) ); */ menu.add(menu_item); // Reopen native-format file // Reopen proof in saved state // Reopen proof whose state was saved // Reopen proof for which state was saved menu_item = new JMenuItem("Reopen proof for which state was saved"); menu_item.addActionListener( new AbstractAction() { public void actionPerformed(ActionEvent event) { if ( !discard_modifications_since_save() ) return; File file; /* File file = file_chooser.getSelectedFile(); if ( file == null ) */ file_chooser.setSelectedFile( new File( file_chooser.getCurrentDirectory(), // While it might be appropriate to // have nothing here, it may happen // that a user wants to reopen the // same file table_model.get_filenamebase() + ".pb" ) ); /* else if ( time_of_last_save > 0 && (suffix_lowercase(file.getName()).equals("html") || suffix_lowercase(file.getName()) .equals("htm") ) ) file_chooser.setSelectedFile( new File( PB_TableModel.basename(file.getName()) + ".pb" ) ); */ for ( ; ; ) { if ( file_chooser.showOpenDialog(frame) != JFileChooser.APPROVE_OPTION ) return; file = file_chooser.getSelectedFile(); String suffix_lc = suffix_lowercase(file.getName()); if ( suffix_lc.equals("pb") ) break; Toolkit.getDefaultToolkit().beep(); JOptionPane.showMessageDialog( frame, "To reopen material saved in ProofBuilder's native format," + " use a file name ending" + " with \".pb\" (or \".PB\".)", "Native-format file name should end \".pb\" (or \".PB\")", JOptionPane.ERROR_MESSAGE ); } // assert file != null : "file != null"; try { ObjectInputStream object_input = new ObjectInputStream(new FileInputStream(file)); /* table_model = (PB_TableModel) object_input.readObject(); // |ObjectOutputStream.writeObject(PB_TableModel)| encountered difficulties, // I think because |PB_TableModel extends AbstractTableModel| which // contains |TableModelListener|s which includes the |JTable| which // (among other problems) uses a |SizeSequence| which was not |Serializable| // . */ table_model = new PB_TableModel(object_input); object_input.close(); table.setModel(table_model); set_columns_widths(); setthings_if_havetheorem(); time_of_last_save = System.currentTimeMillis(); /* if ( table_model.get_expressionsmgmt().get_nonnegintvars() ) { assume_nonneg_int_vars_menuitem.setEnabled(false); assume_nonneg_int_vars_menuitem.setSelected(true); induct_menuitem.setEnabled( ((Ded_Action) induct_menuitem.getActionListeners()[0] ) .appears_applicable(induct_menuitem.getText()) ); } else { assume_nonneg_int_vars_menuitem.setEnabled(true); assume_nonneg_int_vars_menuitem.setSelected(false); } */ } catch ( IOException ioe ) { ioe.printStackTrace(); } catch ( Exception e ) { e.printStackTrace(); Toolkit.getDefaultToolkit().beep(); JOptionPane.showMessageDialog( frame, "Reopening that file didn't work.", "Reopening that file didn't work.", JOptionPane.ERROR_MESSAGE ); } } } ); /* menu_item.setMnemonic(KeyEvent.VK_O); menu_item.setAccelerator( KeyStroke.getKeyStroke( KeyEvent.VK_O, ActionEvent.CTRL_MASK / * | ActionEvent.SHIFT_MASK * / // ctrl-shift-o wasn't getting through ) ); */ menu.add(menu_item); /* menu_item = new JMenuItem("Close"); //menu_item.setMnemonic(KeyEvent.VK_W); //menu_item.setAccelerator( //KeyStroke.getKeyStroke(KeyEvent.VK_W, ActionEvent.CTRL_MASK) //); menu_item.addActionListener(not_yet_impl_action); menu.add(menu_item); */ menu.addSeparator(); // selection // selected expression // selected (sub)expression menu_item = new JMenuItem("Copy selected (sub)expression to clipboard"); menu_item.addActionListener( new AbstractAction() { public void actionPerformed(ActionEvent event) { // see |copy_selected_subexpr_menuitem.setEnabled(...)| below // in |ListSelectionListener| assert table.getSelectedRowCount() == 1 : "table.getSelectedRowCount() == 1"; /* if ( table.getSelectedRowCount() != 1 ) { Toolkit.getDefaultToolkit().beep(); JOptionPane.showMessageDialog( frame, "This operation needs exactly 1 row" + " to be selected.", "Need 1 row selected", JOptionPane.ERROR_MESSAGE ); return; } */ Entry entry = table_model.get_entry(table.getSelectedRows()[0]); // see |copy_selected_subexpr_menuitem.setEnabled(...)| below // in |ListSelectionListener| assert entry.has_expr() : "entry.has_expr()"; /* if( !entry.has_expr() ) { JOptionPane.showMessageDialog( frame, "To do this operation," + " you need to select a row containing a" + " formula.", "Need 1 formula selected", JOptionPane.ERROR_MESSAGE ); return; } */ // 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.get_text().substring( entry.get_selection_start(), entry.get_selection_limit() ) ); Toolkit.getDefaultToolkit().getSystemClipboard() .setContents(stringselection, stringselection); } } ); menu_item.setMnemonic(KeyEvent.VK_C); menu_item.setAccelerator( KeyStroke.getKeyStroke( KeyEvent.VK_C, ActionEvent.CTRL_MASK | ActionEvent.SHIFT_MASK ) ); menu.add(menu_item); final JMenuItem copy_selected_subexpr_menuitem = menu_item; menu.addSeparator(); /* menu_item = new JMenuItem("Page Setup..."); menu_item.addActionListener(not_yet_impl_action); menu.add(menu_item); menu_item = new JMenuItem("Print Preview..."); menu_item.addActionListener(not_yet_impl_action); menu.add(menu_item); menu_item = new JMenuItem("Print..."); menu_item.addActionListener(not_yet_impl_action); menu.add(menu_item); */ /* menu_item = new JMenuItem("About printing"); menu_item.addActionListener( new AbstractAction() { final String[] message = { "To print a proof produced in ProofBuilder," + ' ' + "choose the \"Save as Web page\" menu item,", "and then use a Web browser to open and print" + ' ' + "the Web page containing your proof.", "(Web browsers provide more options for handling" + " output \u2014 changing paper orientation, changing", "font size, 'printing' to a PDF file instead of really" + " to a printer, etc. \u2014 than ProofBuilder might.)" }; public void actionPerformed(ActionEvent ae) { JOptionPane.showMessageDialog( frame, message, ((JMenuItem) ae.getSource()).getText(), JOptionPane.PLAIN_MESSAGE ); } } ); menu.add(menu_item); */ menu_item = new JMenuItem("Print"); menu_item.addActionListener( new AbstractAction() { final javax.print.attribute.PrintRequestAttributeSet print_request_attribute_set = new javax.print.attribute.HashPrintRequestAttributeSet( javax.print.attribute.standard.OrientationRequested .LANDSCAPE ); public void actionPerformed(ActionEvent ae) { if ( table_model.get_title() == table_model.DEFAULT_TITLE ) settitle_action.actionPerformed(ae); if ( username == null ) username = JOptionPane.showInputDialog( "Please ensure username is accurate:", System.getProperty("user.name") ); if ( username == null ) return; // SHOULD ASK WHETHER WANT SHRINK TO FIT OR ... try { table.print( JTable.PrintMode.FIT_WIDTH, new MessageFormat( table_model.get_title() + ", Page {0}" ), new MessageFormat( "by " + username + "; identification " + table_model.get_identification_one_line() ), true, print_request_attribute_set, true ); } catch ( PrinterException pe ) { pe.printStackTrace(); } } } ); menu_item.setMnemonic(KeyEvent.VK_P); menu_item.setAccelerator( KeyStroke.getKeyStroke( KeyEvent.VK_P, ActionEvent.CTRL_MASK | ActionEvent.SHIFT_MASK ) ); menu.add(menu_item); /* menu_item = new JMenuItem("Don't Collect Terms"); menu_item.addActionListener( new AbstractAction() { public void actionPerformed(ActionEvent event) { dont_collect_terms = true; } } ); menu.add(menu_item); */ menu_bar.add(menu); // "Editing" // "Setup" // "Framework" // "Management" menu = new JMenu("Management"); menu.setMnemonic(menu.getText().charAt(0)); menu_item = entertheorem_menuitem; menu_item.addActionListener( new AbstractAction() { public void actionPerformed(ActionEvent event) { assert !table_model.have_theorem() : "!table_model.have_theorem()"; /* if ( table_model.have_theorem() ) { Toolkit.getDefaultToolkit().beep(); JOptionPane.showMessageDialog( (JFrame) table.getTopLevelAncestor(), "You already specified a theorem in this proof.", // entered // for "Already specified theorem", JOptionPane.ERROR_MESSAGE ); return; } */ //entertheorem_menuitem.setEnabled(true); user_entry_dialog.get_theorem( table_model.getRowCount() == 0 ); setthings_if_havetheorem(); } } ); menu.add(menu_item); // Add Premises // Add Presuppositions // Add Assumptions menu_item = new JMenuItem("Add presuppositions"); menu_item.addActionListener( new AbstractAction() { public void actionPerformed(ActionEvent event) { user_entry_dialog.get_presuppositions(); if ( table_model.get_expressionsmgmt() .get_useprimefornot() ) useprimefornot_menuitem.setEnabled(false); if ( table_model.get_expressionsmgmt() .get_usetildefornot() ) usetildefornot_menuitem.setEnabled(false); } } ); menu_item.setMnemonic(KeyEvent.VK_P); menu_item.setAccelerator( KeyStroke.getKeyStroke(KeyEvent.VK_P, ActionEvent.CTRL_MASK) ); menu.add(menu_item); menu.addSeparator(); final JMenuItem increase_fontsize_menu_item = new JMenuItem("Increase font size"); final JMenuItem decrease_fontsize_menu_item = new JMenuItem("Decrease font size"); menu_item = increase_fontsize_menu_item; menu_item.addActionListener( new AbstractAction() { public void actionPerformed(ActionEvent event) { assert fontsizefactor_i < FONT_SIZE_FACTORS_SUPPORTED.length - 1 : "fontsizefactor_i < FONT_SIZE_FACTORS_SUPPORTED.length - 1"; fontsizefactor_i++; set_fontsizes(); decrease_fontsize_menu_item.setEnabled(true); if ( fontsizefactor_i == FONT_SIZE_FACTORS_SUPPORTED.length - 1 ) increase_fontsize_menu_item.setEnabled(false); } } ); //menu_item.setMnemonic(KeyEvent.VK_I); /* THIS WASN'T WORKING menu_item.setAccelerator( KeyStroke.getKeyStroke(KeyEvent.VK_PLUS, ActionEvent.CTRL_MASK) ); */ /* THIS WASN'T WORKING menu_item.setAccelerator( KeyStroke.getKeyStroke( KeyEvent.VK_EQUALS, ActionEvent.CTRL_MASK // | ActionEvent.SHIFT_MASK ) ); menu_item.setAccelerator( KeyStroke.getKeyStroke(KeyEvent.VK_PLUS, ActionEvent.CTRL_MASK) ); */ menu_item.setAccelerator( KeyStroke.getKeyStroke( KeyEvent.VK_MINUS, ActionEvent.CTRL_MASK | ActionEvent.SHIFT_MASK ) ); menu.add(menu_item); menu_item = decrease_fontsize_menu_item; menu_item.addActionListener( new AbstractAction() { public void actionPerformed(ActionEvent event) { assert fontsizefactor_i > 0 : "fontsizefactor_i > 0"; fontsizefactor_i--; set_fontsizes(); increase_fontsize_menu_item.setEnabled(true); if ( fontsizefactor_i == 0 ) decrease_fontsize_menu_item.setEnabled(false); } } ); //menu_item.setMnemonic(KeyEvent.VK_D); menu_item.setAccelerator( KeyStroke.getKeyStroke(KeyEvent.VK_MINUS, ActionEvent.CTRL_MASK) ); menu.add(menu_item); menu.addSeparator(); // It's not clear to me where code checks or unchecks this. // (Does "setEnabled()" do that in addition to changing color?) menu_item = usetildefornot_menuitem; menu_item.addActionListener( new AbstractAction() { public void actionPerformed(ActionEvent ae) { table_model.get_expressionsmgmt().note_usetildefornot(); ((JCheckBoxMenuItem) ae.getSource()).setEnabled(false); } } ); //menu_item.setMnemonic(KeyEvent.VK_T); menu.add(menu_item); // It's not clear to me where code checks or unchecks this. // (Does "setEnabled()" do that in addition to changing color?) menu_item = useprimefornot_menuitem; menu_item.addActionListener( new AbstractAction() { public void actionPerformed(ActionEvent ae) { table_model.get_expressionsmgmt().note_useprimefornot(); ((JCheckBoxMenuItem) ae.getSource()).setEnabled(false); } } ); //menu_item.setMnemonic(KeyEvent.VK_N); menu.add(menu_item); // It's not clear to me where code checks or unchecks this. // (Does "setEnabled()" do that in addition to changing color?) menu_item = // e.g. Sundstrom new JCheckBoxMenuItem("Start " + Symbol.N_NUMBERS_UNICODE + " at 1"); menu_item.addActionListener( new AbstractAction() { public void actionPerformed(ActionEvent ae) { table_model.get_expressionsmgmt().note_startNat1(); ((JCheckBoxMenuItem) ae.getSource()).setEnabled(false); } } ); //menu_item.setMnemonic(KeyEvent.VK_N); menu.add(menu_item); /* menu.addSeparator(); menu_item = assume_nonneg_int_vars_menuitem; menu_item.addActionListener( new AbstractAction() { public void actionPerformed(ActionEvent event) { table_model.get_expressionsmgmt().assume_nonneg_int_vars(); induct_menuitem.setEnabled( ((Ded_Action) induct_menuitem.getActionListeners()[0]) .appears_applicable(induct_menuitem.getText()) ); assume_nonneg_int_vars_menuitem.setEnabled(false); } } ); menu_item.setMnemonic(KeyEvent.VK_N); menu.add(menu_item); */ menu.addSeparator(); menu_item = new JMenuItem("Delete highest numbered step"); menu_item.addActionListener( new AbstractAction() { public void actionPerformed(ActionEvent event) { if ( table.getModel().getRowCount() < 1 ) { Toolkit.getDefaultToolkit().beep(); JOptionPane.showMessageDialog( frame, "There is no row to delete.", /* entered */ /* for */ "No row to delete", JOptionPane.ERROR_MESSAGE ); return; } do { int [] pre_del_selected_rows = table.getSelectedRows(); table_model.delete_last_row(); if ( pre_del_selected_rows.length == 1 && pre_del_selected_rows[0] == table.getModel().getRowCount() && pre_del_selected_rows[0] > 0 ) table.setRowSelectionInterval( pre_del_selected_rows[0] - 1, pre_del_selected_rows[0] - 1 ); } while ( table_model.getRowCount() > 0 && !table_model.get_entry( table_model.getRowCount() - 1 ) .has_expr() ); if ( !table_model.have_theorem() ) { try { head_theorem_textpane.getStyledDocument() .remove( 0, head_theorem_textpane.getStyledDocument() .getLength() ); } catch ( BadLocationException e ) { e.printStackTrace(); } entertheorem_menuitem.setEnabled(true); } } } ); menu_item.setMnemonic(KeyEvent.VK_D); menu_item.setAccelerator( KeyStroke.getKeyStroke( KeyEvent.VK_D, // make a little difficult to type // to try to avoid annoying mistakes ActionEvent.CTRL_MASK | ActionEvent.SHIFT_MASK ) ); menu.add(menu_item); menu_bar.add(menu); /* menu = new JMenu("Premises"); // "Managing Premises" menu_item = new JMenuItem("Load Premises"); // additional scrollable |JTextArea| not editable // always zero or one premise selected // maybe |BorderLayout.PAGE_END| // -- wide, each premise on one line menu_item.addActionListener(not_yet_impl_action); menu.add(menu_item); menu_item = new JMenuItem("Add Premise"); menu_item.addActionListener(not_yet_impl_action); menu.add(menu_item); menu_bar.add(menu); */ menu = new JMenu("Deduction"); menu.setMnemonic(menu.getText().charAt(0)); menu_item = new JMenuItem("Transform one side to the other"); menu_item.addActionListener(new Ded_Action.Transform(/*this,*/ table)); menu_item.setMnemonic(KeyEvent.VK_T); menu_item.setAccelerator( KeyStroke.getKeyStroke(KeyEvent.VK_T, ActionEvent.CTRL_MASK) ); menu.add(menu_item); // Substitute/Replace/Change // Change according to relation or equivalence // VK_G/VK_H menu_item = new JMenuItem( Ded_Action .Apply_Equation_Equivalence_or_Comparison .APPLY_EQ_CMD ); menu_item.addActionListener( new Ded_Action.Apply_Equation_Equivalence_or_Comparison(/*this,*/ table) ); menu_item.setMnemonic(KeyEvent.VK_E); // VK_E/VK_N/VK_Y menu_item.setAccelerator( KeyStroke.getKeyStroke(KeyEvent.VK_E, ActionEvent.CTRL_MASK) ); menu.add(menu_item); menu_item = new JMenuItem("Rewrite using basic algebra or such manipulations"); menu_item.addActionListener( new Ded_Action.Rewrite_Using_Basic_Algebra_Or_Such( /*this,*/ table, user_entry_dialog ) ); menu_item.setMnemonic(KeyEvent.VK_R); menu_item.setAccelerator( KeyStroke.getKeyStroke(KeyEvent.VK_R, ActionEvent.CTRL_MASK) ); menu.add(menu_item); // Substitute/Replace/Change // Change according to relation or equivalence // VK_G/VK_H menu_item = new JMenuItem( "Apply comparison (\"<\", \"" + Symbol.LEQ_UNICODE + "\", \">\", or \"" + Symbol.GEQ_UNICODE + "\")" ); menu_item = new JMenuItem( Ded_Action .Apply_Equation_Equivalence_or_Comparison .APPLY_CMP_CMD ); menu_item.addActionListener( new Ded_Action.Apply_Equation_Equivalence_or_Comparison(/*this,*/ table) ); // "L" begins "less than" // and is near the keys "<" and ">" menu_item.setMnemonic(KeyEvent.VK_L); // VK_L/VK_LESSTHAN menu_item.setAccelerator( KeyStroke.getKeyStroke(KeyEvent.VK_L, ActionEvent.CTRL_MASK) ); menu.add(menu_item); // Partition // Separate components // ^ //menu_item.setDisplayedMnemonicIndex(5); // Split into separate parts of this proof menu_item = new JMenuItem("Split row's formula"); menu_item.addActionListener(new Ded_Action.Split(/*this,*/ table)); menu_item.setMnemonic(KeyEvent.VK_S); menu_item.setAccelerator( KeyStroke.getKeyStroke(KeyEvent.VK_S, ActionEvent.CTRL_MASK) ); menu.add(menu_item); Ded_Action.Resolve resolve_action = new Ded_Action.Resolve(/*this,*/ table); menu_item = new JMenuItem(Ded_Action.Resolve.RESOLVE_SELF_CMD); menu_item.addActionListener(resolve_action); menu_item.setMnemonic(KeyEvent.VK_B); menu_item.setAccelerator( KeyStroke.getKeyStroke( KeyEvent.VK_B, ActionEvent.CTRL_MASK // | ActionEvent.SHIFT_MASK ) ); menu.add(menu_item); menu_item = new JMenuItem(Ded_Action.Resolve.RESOLVE_2ROWS_CMD); // M-W resolution // for a while I tried having // this resolution action handle the // equivalence rule also menu_item.addActionListener(resolve_action); menu_item.setMnemonic(KeyEvent.VK_M); menu_item.setAccelerator( KeyStroke.getKeyStroke( KeyEvent.VK_M, ActionEvent.CTRL_MASK /* + ActionEvent.SHIFT_MASK */ ) ); menu.add(menu_item); // Plug in something for variable // Give/Specify/Assign/Choose value for/to variable // Instantiate variable // Assign to variable // "Assign a value to the selected variable" menu_item = new JMenuItem("Assign value(s) to variable(s)"); menu_item .addActionListener( new Ded_Action.Instantiate_Variable(/*this,*/ table, user_entry_dialog) ); menu_item.setMnemonic(KeyEvent.VK_A); // PLAIN |Ctrl-V| AND |Ctrl-A| DON'T WORK; FUTURE FINAGLE THEM menu_item.setAccelerator( // V taken for paste // and appears hard to change KeyStroke.getKeyStroke( KeyEvent.VK_A, ActionEvent.CTRL_MASK | ActionEvent.SHIFT_MASK ) ); menu.add(menu_item); // "Remove quantifier" // "Dequantify" // Manna&Waldinger: "Eliminate quantifier" menu_item = new JMenuItem("Remove quantifier"); menu_item.addActionListener( new Ded_Action.Dequantify(/*this,*/ table) ); menu_item.setMnemonic(KeyEvent.VK_Q); menu_item.setAccelerator( KeyStroke.getKeyStroke(KeyEvent.VK_Q, ActionEvent.CTRL_MASK) ); menu.add(menu_item); /* menu_item = new JMenuItem("Apply Modus Ponens"); menu_item.addActionListener(new Ded_Action.Modus_Ponens(table)); menu_item.setAccelerator( KeyStroke.getKeyStroke(KeyEvent.VK_M, ActionEvent.CTRL_MASK) ); menu.add(menu_item); "Use implication (that is a supposition)"? Modus Tollens? */ menu_item = induct_menuitem; menu_item.addActionListener(new Ded_Action.Induct(/*this,*/ table)); menu_item.setMnemonic(KeyEvent.VK_I); // Documentation says: "Not all look and feels may support this.": menu_item.setDisplayedMnemonicIndex(7); menu_item.setAccelerator( KeyStroke.getKeyStroke(KeyEvent.VK_I, ActionEvent.CTRL_MASK) ); menu.add(menu_item); menu_item = new JMenuItem("Suppose negation"); menu_item.addActionListener(new Ded_Action.Suppose_Negation(/*this,*/ table)); menu_item.setMnemonic(KeyEvent.VK_N); menu_item.setAccelerator( KeyStroke.getKeyStroke(KeyEvent.VK_N, ActionEvent.CTRL_MASK) ); menu.add(menu_item); /* // universal generalization menu_item = new JMenuItem("Generalize theorem"); menu_item.addActionListener(not_yet_impl_action); // probably have no accelerator for this: should be rarely used / * menu_item.setAccelerator( KeyStroke.getKeyStroke(KeyEvent.VK_I, ActionEvent.CTRL_MASK) ); * / menu.add(menu_item); */ menu.addSeparator(); /* if ( table_model.hilbert_style ) { menu.addSeparator(); CONJOIN AND QUANTIFIER-INTRODUCTIONS } */ menu.addSeparator(); /* menu_item = new JMenuItem("Hilbert-style natural deductions:"); menu_item.set */ menu_item = new JMenuItem("Conjoin two suppositions/derivations"); menu_item.addActionListener(new Ded_Action.Conjoin(/*this,*/ table)); menu_item.setMnemonic(KeyEvent.VK_J); menu_item.setAccelerator( KeyStroke.getKeyStroke( KeyEvent.VK_J, ActionEvent.CTRL_MASK | ActionEvent.SHIFT_MASK ) ); menu.add(menu_item); menu_item = new JMenuItem("Introduce existential quantifier"); menu_item = new JMenuItem( "Introduce existential quantifier \"" + Symbol.EXISTS_UNICODE + '"' ); menu_item.addActionListener( new Ded_Action.Existentially_Quantify(/*this,*/ table) ); //menu_item.setMnemonic(KeyEvent.VK_E); menu_item.setAccelerator( KeyStroke.getKeyStroke( KeyEvent.VK_E, ActionEvent.CTRL_MASK | ActionEvent.SHIFT_MASK ) ); menu.add(menu_item); menu_item = new JMenuItem( "Introduce universal quantifier \"" + Symbol.FORALL_UNICODE + '"' ); menu_item.addActionListener( new Ded_Action.Universally_Quantify(/*this,*/ table) ); //menu_item.setMnemonic(KeyEvent.VK_A); // I might let this menu item use CTRL-SHIFT-A after I make // CTRL-A (without SHIFT) work for "Assign value(s) to variable(s)" // but even then I might want CTRL-U (maybe with or without SHIFT) // to still work for this menu item anyway // considering that the conventional name for this deduction // is "universal generalization". menu_item.setAccelerator( KeyStroke.getKeyStroke( KeyEvent.VK_U, ActionEvent.CTRL_MASK | ActionEvent.SHIFT_MASK ) ); menu.add(menu_item); menu.addSeparator(); // useful if deleted simplification of a row menu_item = new JMenuItem("Try simplification"); menu_item.addActionListener(new Ded_Action.Try_Simplify(/*this,*/ table)); /* menu_item.setAccelerator( KeyStroke.getKeyStroke( KeyEvent.VK_S, ActionEvent.CTRL_MASK + ActionEvent.SHIFT_MASK ) ); */ menu.add(menu_item); menu_bar.add(menu); deductions_menu = menu; /* menu = new JMenu("Help"); menu.setMnemonic(menu.getText().charAt(0)); menu_item = new JMenuItem("Keymap"); menu_item.addActionListener(not_yet_impl_action); menu.add(menu_item); menu_item = new JMenuItem("List of rewritings"); menu_item.addActionListener(not_yet_impl_action); menu.add(menu_item); menu_bar.add(menu); */ table.getSelectionModel().addListSelectionListener( new ListSelectionListener() { // Does anyone care whether an anonymous inner class // uses |private|? /* private int[] prev_selected_rows_indexes = table.getSelectedRows(); */ public void valueChanged(ListSelectionEvent e) { if ( Ded_Action.get_actingvsjustcheckingapplicability() ) return; int[] selected_rows_indexes = table.getSelectedRows(); boolean selected_exprs = false; for ( int selected_row_index : selected_rows_indexes ) if ( table_model.get_entry(selected_row_index) .has_expr() ) selected_exprs = true; else { selected_exprs = false; break; } copy_selected_subexpr_menuitem.setEnabled( selected_exprs && selected_rows_indexes.length == 1 // table.getSelectedRowCount() == 1 ); deductions_menu.setForeground( selected_exprs ? Color.BLACK : Color.gray ); deduction_preps = new Deduction_Prep[selected_rows_indexes.length]; for ( int i = 0; i < deduction_preps.length; i++ ) { if ( !table_model.get_entry(selected_rows_indexes[i]) .has_expr() ) { deduction_preps = null; break; } deduction_preps[i] = new Deduction_Prep(table, i); } for ( int ded_menuitem_i = 0; ded_menuitem_i < deductions_menu.getItemCount(); ded_menuitem_i++ ) { JMenuItem ded_menu_item = deductions_menu.getItem(ded_menuitem_i); if ( ded_menu_item != null ) ded_menu_item.setForeground( deduction_preps != null && ((Ded_Action) ded_menu_item.getActionListeners()[0]) .consider( ded_menu_item.getText(), // C++: (const ...) deduction_preps deduction_preps ) ? Color.BLACK : Color.GRAY ); } // CONSIDER SETTING COLOR OF |deductions_menu| // DEPENDING ON WHETHER SOME OR NO DEDUCTIONS // APPEARED APPLICABLE /* MAKES TABLE JUMP WHILE USER DOES MOUSE-PRESS Arrays.sort(selected_rows_indexes); if ( selected_rows_indexes.length > 0 ) table_scroll_pane.getViewport() .scrollRectToVisible( table.getCellRect( selected_rows_indexes[ selected_rows_indexes.length - 1 ], table.convertColumnIndexToView( PB_TableModel.Column_ID.GOALS.ordinal() ), true ) ); */ /* for ( int row = 0; row < table_model.getRowCount(); row++ ) if ( Arrays.binarySearch(selected_rows_indexes, row) < 0 && table_model.getValueAt( row, PB_TableModel.Column_ID.USED.ordinal() ) != null && table_model.used_wrt_selected_rows( row, selected_rows_indexes ) != table_model.used_wrt_selected_rows( row, prev_selected_rows_indexes ) ) table_model.fireTableCellUpdated( row, PB_TableModel.Column_ID.USED.ordinal() ); prev_selected_rows_indexes = selected_rows_indexes; */ } } ); copy_selected_subexpr_menuitem.setEnabled(false); deductions_menu.setForeground(Color.gray); for ( int ded_menuitem_i = 0; ded_menuitem_i < deductions_menu.getItemCount(); ded_menuitem_i++ ) { JMenuItem ded_menu_item = deductions_menu.getItem(ded_menuitem_i); if ( ded_menu_item != null ) ded_menu_item.setForeground(Color.GRAY); } frame.setJMenuBar(menu_bar); System.out.println("\nfinished menu bar\n"); System.out.println("starting initial user-entry dialog..."); entertheorem_menuitem.setEnabled(true); user_entry_dialog.get_theorem(); System.out.println("finished initial user-entry dialog\n"); setthings_if_havetheorem(); //Display the window: frame.pack(); frame.setVisible(true); } static String suffix_lowercase(String name) { int lastdot_i = name.lastIndexOf('.'); return (lastdot_i == -1 ? "" : name.substring(lastdot_i + 1) ) .toLowerCase(); } // trying this considering noted the following (see elsewhere in this file): // "MAKES TABLE JUMP WHILE USER DOES MOUSE-PRESS" void scroll_to_row_i(int row_i) { table_scroll_pane.getViewport() .scrollRectToVisible( table.getCellRect( row_i, table.convertColumnIndexToView( PB_TableModel.Column_ID.GOALS.ordinal() ), true ) ); } boolean discard_modifications_since_save() { if ( table_model == null || time_of_last_save >= table_model.get_time_of_last_mod() ) return true; Toolkit.getDefaultToolkit().beep(); return JOptionPane.showConfirmDialog( (JFrame) table.getTopLevelAncestor(), "Discard modifications to current proof?", "Discard modifications done to current proof" + (time_of_last_save > 0 ? " since last save?" : "?" ), JOptionPane.YES_OPTION ) == JOptionPane.YES_OPTION; } static final SimpleAttributeSet attrs_head_text = new SimpleAttributeSet(); static { StyleConstants.setBold(attrs_head_text, true); } void setthings_if_havetheorem() { if ( !table_model.have_theorem() ) return; entertheorem_menuitem.setEnabled(false); if ( table_model.get_expressionsmgmt().get_usetildefornot() ) usetildefornot_menuitem.setEnabled(false); if ( table_model.get_expressionsmgmt().get_useprimefornot() ) useprimefornot_menuitem.setEnabled(false); frame.setTitle(table_model.get_title()); set_head_theorem_text(); } void set_head_theorem_text() { assert table_model.have_theorem() : "table_model.have_theorem()"; final String INDENT_STRING = "\n "; String theorem_text_for_head = table_model.get_theorem_text(); boolean newline_already_at_end = false; for ( int i = theorem_text_for_head.length() - 1; Character.isWhitespace(theorem_text_for_head.charAt(i)) || theorem_text_for_head.charAt(i) == '\n'; i-- ) if ( theorem_text_for_head.charAt(i) == '\n' ) { newline_already_at_end = true; break; } theorem_text_for_head = INDENT_STRING + theorem_text_for_head.replaceAll("\n", INDENT_STRING) + (newline_already_at_end ? " " : INDENT_STRING); StyledDocument head_theorem_doc = head_theorem_textpane.getStyledDocument(); try { head_theorem_doc.remove(0, head_theorem_doc.getLength()); head_theorem_doc.insertString( 0, theorem_text_for_head, Entry.Renderer.attrs_expr_regular ); head_theorem_doc.insertString( 0, PB_TableModel.HEAD_TEXT, attrs_head_text ); } catch ( BadLocationException ble ) { ble.printStackTrace(); } } private void set_columns_widths() { FontMetrics fm = table.getFontMetrics(table.getFont()); int n_ = fm.stringWidth(" (##) "); int u_ = fm.stringWidth( table.getModel() .getColumnName( PB_TableModel.Column_ID.USED.ordinal() ) + ' ' ); TableColumn table_column; table_column = table.getColumnModel() .getColumn(PB_TableModel.Column_ID.REF_NUMS.ordinal()); table_column.setPreferredWidth(n_); table_column.setMinWidth(n_); table_column.setMaxWidth(n_); //table_column.setResizable(false); table_column = table.getColumnModel() .getColumn(PB_TableModel.Column_ID.USED.ordinal()); table_column.setPreferredWidth(u_); table_column.setMinWidth(u_); table_column.setMaxWidth(u_); //table_column.setResizable(false); int width_n_u = table.getPreferredScrollableViewportSize().width - (n_ + u_); table.getColumnModel() .getColumn(PB_TableModel.Column_ID.COMMENTS.ordinal()) .setPreferredWidth((int) (width_n_u * .2)); table.getColumnModel() .getColumn(PB_TableModel.Column_ID.SUPPS.ordinal()) .setPreferredWidth((int) (width_n_u * .3)); table.getColumnModel() .getColumn(PB_TableModel.Column_ID.GOALS.ordinal()) .setPreferredWidth((int) (width_n_u * .5)); } void set_fontsizes() { float fontsize = fontsize_original * FONT_SIZE_FACTORS_SUPPORTED[fontsizefactor_i]; menu_bar.setFont( menu_bar.getFont().deriveFont(fontsize * MENU_FONTSIZE_FACTOR) ); /* for ( MenuElement menu_el : menu_bar.getSubElements() ) { JComponent menu_comp = (JComponent) menu_el; menu_comp.setFont( menu_comp.getFont() .deriveFont(fontsize * MENU_FONTSIZE_FACTOR) ); for ( MenuElement menu_item_el : menu_el.getSubElements() ) { JComponent menu_item_comp = (JComponent) menu_item_el; menu_item_comp.setFont( menu_item_comp.getFont() .deriveFont(fontsize * MENU_FONTSIZE_FACTOR) ); } } */ /* for ( int menu_i = menu_bar.getMenuCount() - 1; menu_i >= 0; menu_i-- ) */ for ( int menu_i = 0; menu_i < menu_bar.getMenuCount(); menu_i++ ) { JMenu menu = menu_bar.getMenu(menu_i); if ( menu == null ) continue; menu.setFont( menu.getFont().deriveFont(fontsize * MENU_FONTSIZE_FACTOR) ); for ( int menuitem_i = 0; menuitem_i < menu.getItemCount(); menuitem_i++ ) { JMenuItem menu_item = menu.getItem(menuitem_i); if ( menu_item == null ) continue; menu_item.setFont( menu_item.getFont() .deriveFont(fontsize * MENU_FONTSIZE_FACTOR) ); } } head_theorem_textpane.setFont( head_theorem_textpane.getFont().deriveFont(fontsize) ); main_splitpane.resetToPreferredSizes(); table.setFont(table.getFont().deriveFont(fontsize)); table.getTableHeader().setFont( table.getTableHeader().getFont().deriveFont(fontsize) ); set_columns_widths(); user_entry_dialog.set_fontsizes(fontsize); } }