/* 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 javax.swing.table.AbstractTableModel;
import java.util.ArrayList;
import java.util.LinkedList;
import java.io.*;
import java.util.ListIterator;
import java.awt.event.MouseAdapter;
import java.awt.event.MouseEvent;
import java.awt.Toolkit;
import java.util.Arrays;
import java.util.EnumMap;
import java.util.Map;
import java.util.HashSet;
import javax.swing.JOptionPane;

/**
 * Manages data for <CODE>JTable</CODE> of deductive tableau.
 * @author Hugh McGuire
 */
class PB_TableModel extends AbstractTableModel {
				// implements java.io.Serializable

    // "The Java Language Specification" specified:
    // "nested enum types are implicitly static."
    enum Column_ID { REF_NUMS, COMMENTS, SUPPS, USED, GOALS }

    /*
    private static Column_ID[] col_id_table =
        { Column_ID.NARRATIVE, Column_ID.SUPPS, Column_ID.USED, Column_ID.GOALS };

    private static String[] col_names_table =
        { "Narrative", "Suppositions", "Used", "Theorem and subgoals" };
    */

    private static EnumMap<Column_ID,String> cols_names;
    static {
        cols_names = new EnumMap<Column_ID, String>(Column_ID.class);
        cols_names.put(Column_ID.REF_NUMS, "(#)");	// consider "[#]"
		// original intention for Comments was names
		// including Gries & Schneider's angle-bracketed labels
        cols_names.put(Column_ID.COMMENTS, "Comments");
					// "Suppositions and deriveds
					// "Suppositions and derivatives
					// "Suppositions and their derivatives
					// "Suppositions and derivations
        cols_names.put(Column_ID.SUPPS, "Suppositions and derivations");
        cols_names.put(Column_ID.USED, "Used");
        cols_names.put(Column_ID.GOALS, "Theorem and subgoals");
        }
                    //return "Premises, Suppositions, and Deductions";
                                                        // I'm not entirely
                                                        // happy about
                                                        // "Deductions" here.
                                                        // An alternative I
                                                        // considered is
                                                        // "Derivations".
                                            // alternatively "Used/Reduced"
                                            // "Theorem and Subgoals to Prove"
                                            // "Theorem/Subgoals"
                                            // "Theorem/subgoals"
                                            // "Theorem, subgoals"
                                            // "Theorem and subgoals"

    private static EnumMap<Column_ID,Class> cols_classes;
    static {
        cols_classes = new EnumMap<Column_ID, Class>(Column_ID.class);
        cols_classes.put(Column_ID.REF_NUMS, String.class);
        cols_classes.put(Column_ID.COMMENTS, String.class);
        cols_classes.put(Column_ID.SUPPS, Entry.class);
        cols_classes.put(Column_ID.USED, Boolean.class);
        cols_classes.put(Column_ID.GOALS, Entry.class);
        }



    private static class Row implements java.io.Serializable {
        private final Column_ID entry_col_id;
        private final Entry entry;
        private HashSet<Part_Info> parts_in_which_used;
        private String comment;
        private final Part_Info part_info;
	private int ref_num = -1;
        private final long timestamp; 	// to enable detecting whether
					// a proof has been copied
	private boolean flows_with_preceding_row;

        Row(Column_ID columnspec_given,
                Entry entry_given,
                Part_Info partinfo_given,
		String comment_given,
		boolean flowswithprecedingrow_given
                )
            {
            assert
                columnspec_given == Column_ID.GOALS  
                    ||  columnspec_given == Column_ID.SUPPS  
                :
                "columnspec_given == Column_ID.GOALS"
                + "\n    ||  columnspec_given == Column_ID.SUPPS";
            entry_col_id = columnspec_given;
            if ( (entry = entry_given).has_expr() )
                parts_in_which_used = new HashSet<Part_Info>();
            part_info = partinfo_given;
	    comment = comment_given;
            timestamp = System.currentTimeMillis();
	    flows_with_preceding_row = flowswithprecedingrow_given;
            }

        Row(Column_ID columnspec_given,
                Entry entry_given,
                Part_Info partinfo_given,
		String comment_given
                )
            {
	    this(
		columnspec_given,
		entry_given,
		partinfo_given,
		comment_given,
		false
		);
	    }

        Row(Column_ID columnspec_given,
                Entry entry_given,
                Part_Info partinfo_given,
		boolean flowswithprecedingrow_given
                )
            {
	    this(
		columnspec_given,
		entry_given,
		partinfo_given,
		null,
		flowswithprecedingrow_given
		);
	    }

        Row(Column_ID entry_col_id_given,
		Entry entry_given,
		Part_Info partinfo_given
		)
	    {
	    this(entry_col_id_given, entry_given, partinfo_given, null); 
	    			// CONSIDER |""| FOR DEFAULT |comment|
            }

	void new_comment(String newcomment) {
	    comment = newcomment;
	    }

        Entry get_entry() { return entry; }

        Column_ID get_entrycolid() { return entry_col_id; }

        Part_Info get_partinfo() { return part_info; }

        boolean get_flowswithprecedingrow() { return flows_with_preceding_row; }

        int get_refnum() { return ref_num; }

	HashSet<Part_Info> get_partsinwhichused() {
	    return  parts_in_which_used;
	    }

	Object getValueAt(Column_ID col_id) {
	    switch( col_id ) {
		case  /*Column_ID.*/REF_NUMS:
		    return
			ref_num >= 0
			    // manually center:
			?  (ref_num < 10  ?  " ("  :  "(")
			    + ref_num
			    + ')'
			:  null;

		case  /*Column_ID.*/COMMENTS:
		    return  comment;

		case  /*Column_ID.*/USED:
		    return  parts_in_which_used;	// you may start
		    					// sniffing a kludge
							// (;-)

		case /*Column_ID.*/SUPPS:
		case /*Column_ID.*/GOALS:
		    return   col_id == entry_col_id  ?  entry  :  null;
		}
	    throw new IllegalArgumentException(col_id.toString());
            }

        Object getValueAt(int col) {
	    return  getValueAt(Column_ID.values()[col]);
	    }

	boolean used_at_all() {
	    return
		parts_in_which_used != null
		&&  !parts_in_which_used.isEmpty();
	    }

        boolean isCellEditable(int col) {
            // Rem. the data/cell address is constant,
            // no matter where the cell appears onscreen.
            //return  false;
            return
		/*
		entry.has_expr()
		&&
		(Column_ID.values()[col] == Column_ID.COMMENTS
		    ||  Column_ID.values()[col] == entry_col_id
		    );
		*/
		Column_ID.values()[col] == Column_ID.COMMENTS
		||  entry.has_expr()
		    &&  Column_ID.values()[col] == entry_col_id;
            }

        /*
        public void setValueAt(Object value, int row, int col) {
            data[row][col] = value;
            fireTableCellUpdated(row, col);
            }
        */

        void note_used_in_part(Part_Info part_info) {
	    entry.note_used_subexpr_selected();
	    //parts_in_which_used.add(part_info);
	    part_info.add_this_and_ancestors_with_all_subparts(
		parts_in_which_used
		);
	    }

		// partsinwhichused_contains_or_has_ancestor
	boolean partsinwhichused_contains_super(Part_Info part_info) {
	    // NEED TO WORK ON THIS IN |Entry.java|
	    // PLUS |ListSelectionListener| IN |ProofBuilder.java|
	    //return  !parts_in_which_used.isEmpty();

	    // return  parts_in_which_used.contains(part_info);

	    for ( Part_Info part_in_which_used : parts_in_which_used )
		if ( part_in_which_used.has_as_some_subpart(part_info) )
		    return  true;

	    return  false;
	    }

	void increment_ref_nums_geq(int ref_num_limit) {
	    if ( ref_num >= ref_num_limit )
		ref_num++;
	    if ( !entry.has_expr() )
		entry.increment_narrative_ref_nums_geq(ref_num_limit);
	    }

	/*
        static void output_header_as_HTML(Writer writer) throws IOException {
            // Consider indicating 'preferred' widths
            writer.write("\n<TR>\n");
	    for ( Map.Entry<Column_ID,String> c_n : cols_names.entrySet() )
		if ( c_n.getKey() != Column_ID.USED ) {
		    writer.write("    <TH>");
		    + c_n.getValue() +
		    writer.write("</TH>\n");
		    }
            writer.write("\n</TR>\n");
            }
	*/

        void output_as_HTML(Writer writer) throws IOException {
            writer.write("\n<TR>\n    <!-- " + timestamp + " -->\n");
	    for ( Column_ID col_id : Column_ID.values() )
		if ( col_id != Column_ID.USED ) {
		    writer.write("    <TD>\n");
		    if ( col_id == entry_col_id )
			entry.output_as_HTML(writer);
		    else {
			if ( col_id == Column_ID.COMMENTS )
			    writer.write("<I>");
			String cell_material = (String) getValueAt(col_id);
			Entry.output_as_HTML(
				writer,
				//((String) getValueAt(col_id)).trim()
				cell_material
				);
			if ( col_id == Column_ID.COMMENTS ) {
			    if ( parts_in_which_used != null
				    && parts_in_which_used.isEmpty()
				    )
				{
				if ( cell_material != null
					&&  !cell_material.equals("")
					// pedagogical note:
					// this can't even be simplified to:
					// if ( !"".equals(cell_material) )
					)
				    writer.write("<BR>\n");
				writer.write(Symbol.UNUSED_NOTE + '\n');
				}
			    writer.write("</I>");
			    }
			}
		    writer.write("    </TD>\n");
		    }
            writer.write("</TR>\n");
            }

        }



    /**
     * Used to keep track of segments of proof belonging to different parts.
     * @author Hugh McGuire
     */
    private static class Part_Info implements java.io.Serializable {
	/*
        private final static int NAMES_NONE = 0;
        private final static int NAMES_ARABIC = 1;
        private final static int NAMES_ALPHABETIC = 2;
        private final static int NAMES_ROMAN = 3;
        private final static int NAMES_TYPE_LIMIT = 3;
	*/
        private static final int IDS_NONE = -1;
        private static final int IDS_ARABIC = 0;
        private static final int IDS_ALPHABETIC = 1;
        private static final int IDS_ROMAN = 2;
        private static final int IDS_TYPE_LIMIT = 3;

        private final Part_Info parent;
        private final int id_type;
        private final String case_or_part_;
	String id;
        private Part_Info[] subparts;
        private boolean completed;

	private boolean did_supp_neg;
	private Row transformation_goal_row;
	private boolean achieving_strict_step_for_transforming;
	private Expression transformation_goal;
	    // I would like |const Expression * transformation_goal|.
	private Symbol.Specifier transformationgoal_relationship;

        Part_Info() {        // default values for fields
            // Error message from compiler indicated
            // need to explicitly give default value for a |final| field
            parent = null;
            id_type = -1;
	    case_or_part_ = "";
            id = "the main part";
            }

        String get_label() { return  case_or_part_ + id; }

        private Part_Info(Part_Info p, int i, boolean case_instead_of_part) {
            parent = p;
            id_type = (parent.id_type + 1) % IDS_TYPE_LIMIT;
	    // I'm not using |StringBuilder id_accum| because
	    // not changing much and |String| is nice/convenient with |+=|.
	    case_or_part_ =  case_instead_of_part ? "Case " : "Part ";
	    String id_base =  parent.is_root() ? "" : parent.id;
            switch ( id_type ) {
                case IDS_ARABIC:
		    id = id_base + (i + 1);
                    break;

                case IDS_ALPHABETIC:
                    id = id_base + (char) ('a' + i);
                    break;

                case IDS_ROMAN:
		    String tens_id = "";
                    // I think the possibility of a ridiculously large number
                    // of tens is ridiculous. (;-)
		    for ( int tens = (i + 1)/10; tens > 0; tens-- )
			tens_id += 'x';
                    switch ( (i + 1) % 10 ) {
                        case 1:  id = id_base + '(' + tens_id + "i)";  break;
                        case 2:  id = id_base + '(' + tens_id + "ii)";  break;
                        case 3:  id = id_base + '(' + tens_id + "iii)";  break;
                        case 4:  id = id_base + '(' + tens_id + "iv)";  break;
                        case 5:  id = id_base + '(' + tens_id + "v)";  break;
                        case 6:  id = id_base + '(' + tens_id + "vi)";  break;
                        case 7:  id = id_base + '(' + tens_id + "vii)";  break;
                        case 8:  id = id_base + '(' + tens_id + "viii)";  break;
                        case 9:  id = id_base + '(' + tens_id + "ix)";  break;
                        }
                    break;
                }
            }

        Part_Info[] new_subparts(int s, boolean case_instead_of_part) {
	    /*
            // assert  subparts == null;
            subparts = new Part_Info[s];
	    // not 'enhanced' |for| because assigning to element
	    // (and using index as well as element)
            for ( int i = 0; i < subparts.length; i++ )
                subparts[i] = new Part_Info(this, i + 1, case_instead_of_part);
            return  subparts;
	    */
	    // assert  s > 0  :  "s > 0";
	    Part_Info[] old_subparts =
		subparts == null  ?  new Part_Info[0]  :  subparts;
	    subparts = new Part_Info[old_subparts.length + s];
	    System.arraycopy(old_subparts, 0, subparts, 0, old_subparts.length);
            for ( int i = old_subparts.length; i < subparts.length; i++ )
                subparts[i] = new Part_Info(this, i, case_instead_of_part);

	    Part_Info[] result = new Part_Info[s];
	    System.arraycopy(subparts, old_subparts.length, result, 0, s);
            return  result;
            }

        Part_Info[] new_subparts(int s) { return new_subparts(s, false); }

	Part_Info[] get_subparts() { return  subparts; }

        boolean has_as_some_subpart(Part_Info cs) {
            return
                this == cs  ||  cs != null  &&  has_as_some_subpart(cs.parent);
            }

        boolean is_root() { return  parent == null; }

        void add_this_and_ancestors_with_all_subparts(HashSet<Part_Info> s) {
	    s.add(this);
	    if ( parent == null )
		return;
	    for ( Part_Info subpart : parent.subparts )
                if ( !s.contains(subpart) )
                    return;
            parent.add_this_and_ancestors_with_all_subparts(s);
            }

        private boolean check_completing_to_root() {
            // assert  subparts != null;
	    for ( Part_Info subpart : subparts )
                if ( !subpart.completed )
                    return  false;
            return  note_completing_root();
            }

        boolean note_completing_root() {
            boolean  completed_prev = completed;
            completed = true;
            if ( parent != null )
                return  parent.check_completing_to_root();
            // CONSIDER NOTE_COMPLETED() ALL SUBCASES ...
            return  completed != completed_prev;
            }

        boolean singleton_subpart() {
            return  parent == null  ||  parent.subparts.length == 1;
            }

        boolean singleton_subparts() {
	    // pedagogical note: |NullPointerException| if try the following:
	    // singleton_subpart() && parent.singleton_subparts()
            return
		parent == null
		||  parent.subparts.length == 1
		    &&  parent.singleton_subparts();
            }

	boolean get_didsuppneg() { return  did_supp_neg; }
	
	void note_supp_neg() { did_supp_neg = true; }

	void note_transformation_goal(
		Row tg_row_given,
		Symbol.Specifier tg_relationship_given,
		Expression transformation_goal_given
		)
	    {
	    transformation_goal_row = tg_row_given;
	    transformation_goal = transformation_goal_given;
	    transformationgoal_relationship = tg_relationship_given;
	    }

	void note_achieving_strict_step_for_transforming() {
	    achieving_strict_step_for_transforming = true;
	    }

	boolean get_achievingstrictstepfortransforming() {
	    return  achieving_strict_step_for_transforming;
	    }

	Row get_transformationgoalrow() { return  transformation_goal_row; }

	Symbol.Specifier get_transformationgoal_relationship() {
	    return  transformationgoal_relationship;
	    }

	boolean basic_possible_match_tg(Expression expr) {
	    return
		transformation_goal != null
		    &&  transformation_goal.op_spec_equals(
			    expr.get_operator().get_specifier()
			    );
	    }

	Expression get_transformationgoal_clone() {
	    return  (Expression) transformation_goal.clone();
	    }

        }


    
    private static final int REF_NUM_START = 1;

    static final String SPACES_AT_FRONT_OF_EQUALS_ETC_BY_ = "    ";
    static final String SPACES_BY_ = "      by ";
    				// Consider "    =    //  by ".
    				// Consider enabling user to set preferences
				// specifying something other than "//"
				// including parentheses around the material
				// or angle brackets around it.
				// Consider having this somewhat |"Monospaced"|.
    static final String EQUALS_BY_ =
	// "    =      by ";
	SPACES_AT_FRONT_OF_EQUALS_ETC_BY_ + '=' + SPACES_BY_;
    static final String EQUIV_BY_ =
	SPACES_AT_FRONT_OF_EQUALS_ETC_BY_
	+ Symbol.THREE_BAR_UNICODE
	+ SPACES_BY_;
    /*
    static final String EQUIV_BY_OUT =
	" &nbsp; &nbsp; = &nbsp; &nbsp; &nbsp; by ";
    */
    static final String REDUCES_BY_ =
	SPACES_AT_FRONT_OF_EQUALS_ETC_BY_
	+ Symbol.ARROW_DOWNWARD_ONE_BAR_UNICODE
		// This should be interpreted as
		// 'implies' in the Suppositions/Derivations column,
		// 'is implied by' in the Goals column.
	+ SPACES_BY_;
    /*
    static final String REDUCES_BY_OUT =
	" &nbsp; &nbsp; &darr; &nbsp; &nbsp; &nbsp; by ";
    */

    static final String DEFAULT_TITLE = "ProofBuilder";
    static final String DEFAULT_FILENAMEBASE = "TITLE";


    private ArrayList<Row> rows;
    // The base alternative data structure is a two-dimensional array of
    // |Object| (see code of base(s)).  But such inspecifity of types
    // appears unappealing to me.
    // An alternative is to have multiple arrays here, one for each column.
    // But I think an organization like that went out of fashion when
    // computer scientists transitioned from original Fortran
    // to Algol/Pascal etc.
    private Row theorem_row;
    private long time_of_last_mod;
    private Expressions_Mgmt expressions_management;
    private String title, file_name_base;

    //boolean hilbert_style;

    // not saved:
    private int added_row_index = -1;
    private Row remembered_added_row;

    void set_addedrowindex_neg1() { added_row_index = -1; }

    int get_addedrowindex() { return added_row_index; }

    void remember_added_row() {
	remembered_added_row = rows.get(added_row_index);
	}

    void set_addedrowindex_to_remembered() {
	// assert rem'd != null  and somehow 
	/*
	for ( added_row_index = 0;
		rows.get_added_row_index != remembered_added_row;
		added_row_index++
		)
	    ;
	*/
	added_row_index = rows.indexOf(remembered_added_row);
	}

    void store_expressionsmgmt(ObjectOutputStream object_output)
		throws IOException
	{
	object_output.writeObject(expressions_management);
	}

    @SuppressWarnings("unchecked")	// (ArrayList<Row>) readObject()
    void restore_expressionsmgmt(ObjectInputStream object_input)
		throws Exception
	{
	expressions_management = (Expressions_Mgmt) 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|
    // .
    void output_native(ObjectOutputStream object_output) throws IOException {
	object_output.writeObject(rows);
	object_output.writeObject(theorem_row);
	object_output.writeLong(time_of_last_mod);
	object_output.writeObject(expressions_management);
	//object_output.writeBoolean(hilbert_style);
	object_output.writeObject(title);
	object_output.writeObject(file_name_base);
	}

    @SuppressWarnings("unchecked")	// (ArrayList<Row>) readObject()
    public PB_TableModel(ObjectInputStream object_input) throws Exception {
	rows = (ArrayList<Row>) object_input.readObject();
	theorem_row = (Row) object_input.readObject();
	time_of_last_mod = object_input.readLong();
	expressions_management = (Expressions_Mgmt) object_input.readObject();
	//hilbert_style = object_input.readBoolean();
	title = (String) object_input.readObject();
	file_name_base = (String) object_input.readObject();
	}

    // See Java API documentation for |Serializable| regarding the following:
    private void readObject(ObjectInputStream stream)
	     throws IOException, ClassNotFoundException
	 {
	 throw new NotSerializableException();
	 }
    private void writeObject(ObjectOutputStream stream) throws IOException
	{
	throw new NotSerializableException();
	}

    public PB_TableModel(String preferences_lc) {
	assert
	    preferences_lc.equals(preferences_lc.toLowerCase())
	    : "preferences_lc.equals(preferences_lc.toLowerCase())";
	rows = new ArrayList<Row>();
	expressions_management = new Expressions_Mgmt(preferences_lc);
	//hilbert_style |= preferences_lc.contains("hilbertstyle");
	title = DEFAULT_TITLE;
	file_name_base = DEFAULT_FILENAMEBASE;
	}


    static String basename(String name) {
        int lastdot_i = name.lastIndexOf('.');
        return  lastdot_i == -1  ?  name  :  name.substring(0, lastdot_i);
        }

    String get_title() { return title; }

    String get_filenamebase() { return file_name_base; }

    void set_title(String new_title) {
	if ( new_title == null )
	    return;
	title = new_title;
	if ( file_name_base == DEFAULT_FILENAMEBASE )
	    file_name_base = title;
	}

    void set_filenamebase(String new_filenamebase) {
	if ( new_filenamebase == null )
	    return;
	file_name_base = new_filenamebase;
	}

    Expressions_Mgmt get_expressionsmgmt() { return expressions_management; }

    public long get_time_of_last_mod() { return time_of_last_mod; }

    boolean have_theorem() { return  theorem_row != null; }

    String get_theorem_text() { return  theorem_row.get_entry().get_text(); }

    Symbol.Specifier get_transformationgoal_relationship(int row_i) {
	return  rows.get(row_i).get_partinfo()
		.get_transformationgoal_relationship();
	}

    /*
     * JTable uses this method to determine the default renderer/
     * editor for each cell.  If we didn't implement this method,
     * then the used column would contain text ("true"/"false"),
     * rather than a check box.
     */
    public Class getColumnClass(int c) {
        return cols_classes.get(Column_ID.values()[c]);
        }

    public int getColumnCount() { return Column_ID.values().length; }

    public String getColumnName(int col) {
        return cols_names.get(Column_ID.values()[col]);
        }

    public int getRowCount() { return rows.size(); }

    Column_ID get_entrycolid_of_row(int row) {
        return  rows.get(row).get_entrycolid();
        }

    Entry get_entry(int row) {
        return  rows.get(row).get_entry();
        }

    public Object getValueAt(int row, int col) {
        return  rows.get(row).getValueAt(col);
        }

    public boolean isCellEditable(int row, int col) {
        return  rows.get(row).isCellEditable(col);
        }

    public void setValueAt(Object value, int row, int col) {
	if( col == Column_ID.COMMENTS.ordinal() ) {
	    /*
	    assert
		value instanceof String
		: "value instanceof String";
	    */
	    //data[row][col] = value;
	    rows.get(row).new_comment((String) value);
	    fireTableCellUpdated(row, col);
	    }
	}

    void note_used_row_in_part(int used_row_i, Part_Info part_info) {
        rows.get(used_row_i).note_used_in_part(part_info);
        fireTableCellUpdated(used_row_i, Column_ID.USED.ordinal());
        }

    void note_used_rows_in_part(int[] used_rows_i, Part_Info part_info) {
	for ( int used_row_i : used_rows_i )
	    note_used_row_in_part(used_row_i, part_info);
	}

    void note_supp_neg(int neg_row) {
	rows.get(neg_row).get_partinfo().note_supp_neg();
	}

    void note_transformation_goal(
	    int transforming_row_i,
	    int tg_row_i,
	    Symbol.Specifier tg_relationship_given,
	    Expression tg_expr
	    )
	{ 
	rows.get(transforming_row_i).get_partinfo()
		.note_transformation_goal(
		    rows.get(tg_row_i),
		    tg_relationship_given,
		    tg_expr
		    );
	}

    void note_achieving_strict_step_for_transforming(int t_row_i) {
	rows.get(t_row_i).get_partinfo()
		.note_achieving_strict_step_for_transforming();
	}

    /*
    boolean row_consistent_with_a_part(int row, int[] selected_rows) {
	for ( int selected_row : selected_rows )
	    if ( parts_consistent(row, selected_row) )
		return  true;
	return  false;
	}

    boolean row_used_by_a_part(int row, int[] selected_rows) {
	for ( int selected_row : selected_rows )
	    if ( rows.get(row)
		    .partsinwhichused_contains_super(
			rows.get(selected_row).get_partinfo()
			)
		    )
		return  true;
	return  false;
	}

    boolean used_at_all(int row) {
	return  !rows.get(row).parts_in_which_used.isEmpty();
	}

    boolean used_wrt_selected_rows(int row, int[] selections) {
	return
	    row_consistent_with_a_part(row, selections)
	    ? row_used_by_a_part(row, selections)
	    : used_at_all(row);
	}
    */

    boolean used_wrt_selected_rows(int row_i, int[] selected_row_is) {
	Row row = rows.get(row_i);
	boolean row_is_superpart_of_a_sel = false;
	for ( int selected_row_i : selected_row_is ) {
	    if ( selected_row_i >= rows.size() )	// was deleted
		continue;
	    Row selected_row = rows.get(selected_row_i);
	    // not using |parts_consistent()| here
	    // because here want superpart to appear ~~inconsistent with subpart
	    boolean row_is_superpart_of_sel =
		row.get_partinfo()
			.has_as_some_subpart(
			    selected_row.get_partinfo()
			    );
	    row_is_superpart_of_a_sel |= row_is_superpart_of_sel;
	    if ( row_is_superpart_of_sel	// for efficiency(?)
		   && row.partsinwhichused_contains_super(
			    selected_row.get_partinfo()
			    )
		    )
		return  true;
	    }
	return
	    !row_is_superpart_of_a_sel && !row.parts_in_which_used.isEmpty();
	}

    		// "clearly" a.k.a. "easily"
    // if true, returns nonnegative index of row providing the inference;
    // otherwise returns negative value
    int can_clearly_infer_nonnegative(Expression expr, int row_index) {
	/*
	while ( row_index + 1 < rows.size()
		&&  rows.get(row_index + 1).get_partinfo() == part_info
		)
	    row_index++;
	*/
	Part_Info part_info = rows.get(row_index).get_partinfo();
	row_index = end_part_seg_rows(row_index);
	for ( ; row_index >= 0; row_index-- )  {
	    Row row = rows.get(row_index);
	    Entry entry = row.get_entry();
	    if ( entry.has_expr()
		    &&  row.get_entrycolid() == Column_ID.SUPPS
		    &&  row.get_partinfo().has_as_some_subpart(part_info)
		    &&  Symbol.is_transitive_numeric_comparator(
				entry.get_expr_op_spec()
				)
		    &&  entry.get_expr_op_spec() != Symbol.Specifier.EQUALS
		    )
		{
		Expression
		    entry_expr = entry.get_expr_clone(),
		    arg1_ungrp = entry_expr.get_argument1().ungroup(),
		    arg2_ungrp = entry_expr.get_argument2().ungroup();
		switch ( entry_expr.get_operator().get_specifier() ) {
		    case  LEQ:
		    case  LESS_THAN:
			if ( arg2_ungrp.equivalent_form(expr)
				&& (arg1_ungrp.op_spec_equals(
					    Symbol.Specifier.INT
					    )
					&&  0
					    <=
					    arg1_ungrp.get_operator().get_val()
				    || expressions_management
					.is_variable(arg1_ungrp)
				    )
				)
			    return  row_index;
			break;

		    case  GEQ:
		    case  GREATER_THAN:
			if ( arg1_ungrp.equivalent_form(expr)
				&& (arg2_ungrp.op_spec_equals(
					    Symbol.Specifier.INT)
					&&  arg2_ungrp.get_operator().get_val()
					    >=
					    0
				    || expressions_management
					.is_variable(arg2_ungrp)
				    )
				)
			    return  row_index;
			break;
		    }
		}
	    }
	return  -1;
	}

    int matching_row_spec_column(
		int row_index,
		Part_Info part_info,
		Expression expr,
		Column_ID col_id
		)
	{
	assert
	    col_id == Column_ID.GOALS  ||  col_id == Column_ID.SUPPS
	    :  "col_id == Column_ID.GOALS"
		+ "  ||  col_id == Column_ID.SUPPS";
	/*
	while ( row_index + 1 < rows.size()
		&&  rows.get(row_index + 1).get_partinfo() == part_info
		)
	    row_index++;
	*/
	row_index = end_part_seg_rows(row_index);
	for ( ; row_index >= 0; row_index-- )  {
	    Row row = rows.get(row_index);
	    if ( !(row.get_entry().has_expr()
			&&  row.get_entrycolid() == col_id
			)
		    )
		continue;
	    /*
	    assert
		row.get_entry().has_expr()
		    && (row.get_entrycolid() == Column_ID.GOALS
			||  row.get_entrycolid() == Column_ID.SUPPS
			)
		:
		". . .";
	    */
	    if ( !row.get_partinfo().has_as_some_subpart(part_info) )
		continue;
	    			// Checking |unify()| for each --- involving
				// invoking |clone()| for each (twice) ---
				// appears excessive; and it may be more
				// educational to make the user apply
				// |Combine| to the two relevant rows.
				// Maybe consider trying |unify()|
				// for 'unused' entries with matching operators
				// (including matching names if they are
				// predicates).
	    if ( row.get_entry().expr_equiv_form(expr) )
		//return  ((String) row.getValueAt(Column_ID.REF_NUMS)).trim();
		return  row_index;
	    }
	return  row_index;
	}

    String achieves_transformation_goal(Part_Info part_info, Expression expr) {
		    // basic check before trying more work:
	if ( !part_info.basic_possible_match_tg(expr) )
	    return  null;
	Expression tg_clone = part_info.get_transformationgoal_clone(),
	    expr_clone = (Expression) expr.clone();
	LinkedList<Expressions_Mgmt.Variable_Binding_to_Expression>
	    transformationgoal_unifier;
	if ( (transformationgoal_unifier =
		    expressions_management
			.unify(tg_clone, expr_clone, tg_clone, expr_clone)
		    )
		    == null
		|| (part_info.get_transformationgoal_relationship()
			    == Symbol.Specifier.LESS_THAN
			||  part_info.get_transformationgoal_relationship()
			    == Symbol.Specifier.GREATER_THAN
			)
		    &&  !part_info.get_achievingstrictstepfortransforming()
		)
	    return  null;
	String result =
	    ((String)
		part_info.get_transformationgoalrow()
			.getValueAt(Column_ID.REF_NUMS)
		)
	    .trim();
	if ( !transformationgoal_unifier.isEmpty() ) {
	    result += "\nwith \"";
	    do {
		Expressions_Mgmt.Variable_Binding_to_Expression binding =
		    transformationgoal_unifier.remove();
		result +=
		    binding.variable
		    + " := "
		    + binding.expression.gen_text()
		    + (transformationgoal_unifier.isEmpty()
			? "\""
			: ", "
			);
		}
	      while ( !transformationgoal_unifier.isEmpty() );
	    }
	return  result;
	}

    String possible_conclusion(
            Expression expr,
            Column_ID entry_col_id,
            Part_Info part_info
            )
        {
        String result = null;
        if ( expr.op_spec_equals(Symbol.Specifier.TRUE)
                &&  entry_col_id == Column_ID.GOALS
                )
	    {
	    if ( !part_info.is_root() )
	    	    // when said cases had |&&  part_info.singleton_subpart()|
		return  "That concludes this part of the proof.";
            result =  "That concludes the proof";
	    }
        else if ( expr.op_spec_equals(Symbol.Specifier.FALSE)
                    &&  entry_col_id == Column_ID.SUPPS
                    )
            result =
                part_info.get_didsuppneg()
                ? "Thus, the earlier supposition of"
                    + "\nthe negation of the goal to prove"
                    + "\nyields a contradiction ("
                            + expr.get_operator().get_text()
                            + ").  Therefore,"
                    + "\nthe original theorem that was given"
                    + "\nmust be true"
                    // Reductio Ad Absurdem
                : "Thus, the suppositions"
                    + "\nyield a contradiction ("
                            + expr.get_operator().get_text()
                            + ")."
                    + "\nThen since something false implies anything,"
                    + "\nthe theorem that was given is true";
        if ( result != null )
            result +=
		part_info.is_root()  ?  "."  :  " for this part of the proof.";
        return  result;
        }

    int end_part_seg_rows(int row_i) {
	Part_Info part_info = rows.get(row_i).get_partinfo();
        while ( row_i + 1 < rows.size()
                    &&  rows.get(row_i + 1).get_partinfo() == part_info
		    )
	    row_i++;
        return  row_i;
        }

    int end_part_seg_rows(Part_Info part_info) {
	int result;
	for ( result = rows.size(); 
		rows.get(--result).get_partinfo() != part_info;
		)
	    ;
	return  result;
        }

    /*
    int end_flowing_rows(int row_i) {
        while ( row_i + 1 < rows.size()
                    &&  rows.get(row_i + 1).get_flowswithprecedingrow()
		    )
	    row_i++;
        return  row_i;
        }
    */

    private void add_row(final int dest_index, Row row_adding) {
	if ( row_adding.entry.has_expr() ) {
	    int index;
	    for ( index = dest_index;
		    --index >= 0  &&  !rows.get(index).entry.has_expr();
		    )
		;
	    row_adding.ref_num =
		index < 0
		?  REF_NUM_START
		:  rows.get(index).get_refnum() + 1;
	    for ( int i = dest_index; i < rows.size(); i++ )
		rows.get(i).increment_ref_nums_geq(row_adding.ref_num);
	    }
	fireTableDataChanged();
	rows.add(dest_index, row_adding);
	time_of_last_mod = System.currentTimeMillis();
	fireTableRowsInserted(dest_index, dest_index);
	    // Beyond |fireTableDataChanged()|, this generates
	    // |TableModelEvent.INSERT|
	if ( row_adding.entry.has_expr() )
	    if ( row_adding.entry.get_selected_subexpr_ungroup_op_spec()
		    == (row_adding.entry_col_id == Column_ID.GOALS
			? Symbol.Specifier.FALSE
			: Symbol.Specifier.TRUE
			)
		    )
		{
		// A student doing this indicated that allowing insertion
		// of the result while alerting like this appeared best,
		// and the rest of the class went along with this.
		// If this software prevents the insertion, users may
		// think that the software simply isn't working.
		Toolkit.getDefaultToolkit().beep();
		String[] message = {
		    // "Be advised that obtaining that ..."
		    "Be advised that that result does not conclude the proof:",
		    "you need to obtain \"true\" in the Goals column",
		    "or \"false\" in the Suppositions column."
		    };
		JOptionPane.showMessageDialog(
		    null,
		    message,
		    "That doesn't conclude proof",
		    JOptionPane.WARNING_MESSAGE
		    );
		if ( row_adding.comment == null
			||  row_adding.comment.equals("")
			)
		    row_adding.new_comment("inconsequential");
		    			// "useless"
					// "inconsequential"
					// "of no use"
		}
	}


    // base version |add()| when not partitioning into parts.
    // @return index of added expression row
    private void add(
	    int row_index_to_follow,
	    Column_ID entry_col_id,
	    String narrative_flowing_with_preceding_row,
	    String narrative_independent,
	    String comment_content,
	    String expr_text,
	    Expression expr,
	    boolean in_sequence
	    )
        {
	Part_Info part_info;
        Entry entry_to_follow = null;
	boolean flows_with_preceding_row = false;
	String narrative = null;
	boolean presupposition = false;
	if ( row_index_to_follow == -1 ) {	// this condition signals
						// theorem or
						// presupposition/presupposition
	    assert
		entry_col_id == Column_ID.SUPPS
		    ||  entry_col_id == Column_ID.GOALS
			&&  theorem_row == null
		:
		"entry_col_id == Column_ID.SUPPS\n"
		    +  "\n||  entry_col_id == Column_ID.GOALS"
			+ "  &&  theorem_row == null";

	    part_info =
		rows.size() > 0
		?  rows.get(0).get_partinfo()
		:  new Part_Info();
	    flows_with_preceding_row = true;

	    // If there are any presuppositions, they have
	    // "We presuppose the following:" at the beginning
	    // and a blank goal at the end.  Code depends on these
	    // details such as the blank entry at the end of the presuppositions
	    // being a goal.  E.g. consider "Delete highest-numbered step"
	    // applied to theorem row followed by entering theorem.

	    // Advance |row_index_to_follow|
	    // to index of last presupposition (if any):
	    while ( row_index_to_follow + 1 < rows.size()
		    &&  rows.get(row_index_to_follow + 1).entry_col_id
			== Column_ID.SUPPS
		    )
		row_index_to_follow++;

	    if ( entry_col_id == Column_ID.GOALS ) {
		narrative = narrative_independent;
		    /*
		    "We start working with the formula being proved"
		    + "\nas follows:";
		    */
		if ( row_index_to_follow > -1 )
		    // There must be some presuppositions already;
		    // in this case, have a blank row between them and theorem:
		    add_row(
			++row_index_to_follow,
			new Row(Column_ID.GOALS,
				new Entry(/*"\n"*/""),
				part_info,
				true
				)
			);
		}
	    else {  	//if ( entry_col_id == Column_ID.SUPPS )
	    		// presupposition
		presupposition = true;
		// With presupposition(s), arrange to have
		// "We presuppose the following:" at the beginning of them
		// and a blank row at the end of them:
		// (see also some discussion a little above regarding this):
		if ( row_index_to_follow == -1 ) {
		    narrative = narrative_independent;
			// "We presuppose the following:";
		    if ( have_theorem() )
			add_row(
			    0,
			    new Row(Column_ID.GOALS,
				    new Entry(/*"\n"*/""),
				    part_info,
				    true
				    )
			    );
		    }
		}
	    }
        else {
	    if ( in_sequence
		    ||  row_index_to_follow + 1 >= rows.size()
		    ||  !rows.get(row_index_to_follow + 1)
				.get_flowswithprecedingrow()
		    )
		flows_with_preceding_row =
		    // actually still not sure when to set |flows|
		    (narrative = narrative_flowing_with_preceding_row) != null;
	    else {
		//row_index_to_follow = end_flowing_rows(row_index_to_follow);
		row_index_to_follow = end_part_seg_rows(row_index_to_follow);
		narrative = narrative_independent;
		}
            Row row_to_follow = rows.get(row_index_to_follow);
            part_info = row_to_follow.get_partinfo();
            entry_to_follow = row_to_follow.get_entry();
            }
	if ( narrative != null )
	    add_row(
		++row_index_to_follow,
		new Row(
			entry_col_id,
			new Entry(narrative),
			part_info,
			flows_with_preceding_row
			)
		);
	int result;
        add_row(
	    result = ++row_index_to_follow,
            new Row(entry_col_id,
                    new Entry(expr_text, expr),
                    part_info,
		    comment_content,
		    narrative != null  ||  flows_with_preceding_row
                    )
	    );
	if ( theorem_row == null  &&  entry_col_id == Column_ID.GOALS ) {
            theorem_row = rows.get(result);
	    set_title(comment_content);
	    }

	// Checking these conditions here in addition to following |simplify()|
	// useful e.g. to prove  even(a) /\ even(b) ==> even(ab)
	// because  ab = (2j)(2k) = 2(j*2k) simplified to 4jk  
	// and intermediate unsimplified expression(s) unchecked against  2z.
	String achievedtransf_info = null;
	int matchingsuppvsgoal_row_i = -1;
	if ( entry_col_id == Column_ID.SUPPS
		||  (achievedtransf_info
			= achieves_transformation_goal(part_info, expr)
			)
		    == null
		)
	    matchingsuppvsgoal_row_i =
		matching_row_spec_column(
			row_index_to_follow,
			part_info,
			expr,
			entry_col_id == Column_ID.SUPPS
			    ?  Column_ID.GOALS
			    :  Column_ID.SUPPS
			);

        boolean simplify =
	    achievedtransf_info == null
	    &&  matchingsuppvsgoal_row_i == -1
	    &&  expressions_management.simplify(expr);
	expr.clear_excessive_basic_grps_internal();
	expr = expr.ungroup();
        if ( simplify
		/*
                &&
                    (entry_col_id == Column_ID.SUPPS
                        ?  !expr.op_spec_equals(Symbol.Specifier.TRUE)
                                ||  !presupposition
                        :  entry_to_follow == null
                                ||  !entry_to_follow.has_expr()
                                ||  !entry_to_follow.expr_equiv_form(expr)
                        )
		*/
                &&  !(entry_col_id == Column_ID.SUPPS
                        &&  expr.op_spec_equals(Symbol.Specifier.TRUE)
			&&  presupposition
			)
		&&  matching_row_spec_column(
			    row_index_to_follow,
			    part_info,
			    expr,
			    entry_col_id
			    )
		    < 0
		/*
                && (sel_row_max < 0
                    || !rows.get(sel_row_max).get_entry()
			    .expr_equiv_form(expr)
                        && (sel_row_max == sel_row_min
                            || !rows.get(sel_row_min).get_entry()
                                    .expr_equiv_form(expr)
                            )
                    )
		*/
                )
            {
            note_used_row_in_part(row_index_to_follow, part_info);
	    String narrative_addition = "";
	    if ( row_index_to_follow + 1 < rows.size()
		    &&  rows.get(row_index_to_follow + 1)
				.get_flowswithprecedingrow()
		    )
		{
		narrative_addition =
		    "Formula "
		    + ((String)
			getValueAt(
				row_index_to_follow,
				Column_ID.REF_NUMS.ordinal()
				)
			)
			.trim()
		    + ' ';
		//row_index_to_follow = end_flowing_rows(row_index_to_follow);
		row_index_to_follow = end_part_seg_rows(row_index_to_follow);
		}
	    add_row(
		++row_index_to_follow,
		new Row(entry_col_id,
			new Entry(
			    narrative_addition
			    + (expr.get_operator().spec_boolean()
				    ||  part_info
					    .get_transformationgoal_relationship()
					== Symbol.Specifier.EQUIV
				?  EQUIV_BY_
				:  EQUALS_BY_
				)
			    + "simplifying"
			    ),
						// "simplification(s)"
			part_info,
			true
			)
		);
	    add_row(
		result = ++row_index_to_follow,
		new Row(entry_col_id,
			new Entry(expr),
			part_info,
			true
			)
		);

	    if ( entry_col_id == Column_ID.SUPPS
		    ||  (achievedtransf_info
			    = achieves_transformation_goal(part_info, expr)
			    )
			== null
		    )
		matchingsuppvsgoal_row_i =
		    matching_row_spec_column(
			    row_index_to_follow,
			    part_info,
			    expr,
			    entry_col_id == Column_ID.SUPPS
				?  Column_ID.GOALS
				:  Column_ID.SUPPS
			    );
            }

	if ( achievedtransf_info != null ) {
	    note_used_row_in_part(row_index_to_follow, part_info);
	    add_row(
		++row_index_to_follow,
		new Row(
			entry_col_id,	// Column_ID.GOALS,
			new Entry(
				"And that satisfies our earlier goal "
				+ achievedtransf_info
				+ "; i.e. we have:"
				),
			part_info
			)
		);
	    add_row(
		result = ++row_index_to_follow,
		new Row(
			entry_col_id,	// Column_ID.GOALS,
			new Entry(
				expr
				=
				new Expression(
					expressions_management
					.new_Symbol(Symbol.Specifier.TRUE)
					)
				),
			part_info
			)
		);
	    }
	else if ( matchingsuppvsgoal_row_i >= 0 ) {
	    note_used_row_in_part(row_index_to_follow, part_info);
	    note_used_row_in_part(matchingsuppvsgoal_row_i, part_info);
	    // consider odd possibility:
	    // |row_index_to_follow < matchingsuppvsgoal_row_i|
	    String matchingsuppvsgoal_info =
		((String)
		    rows.get(matchingsuppvsgoal_row_i)
			    .getValueAt(Column_ID.REF_NUMS)
		    )
		.trim();
	    narrative_independent =
		"And formula "
		+ ((String) rows.get(result).getValueAt(Column_ID.REF_NUMS))
		    .trim()
		+ " matches formula "
		+ matchingsuppvsgoal_info
		+ "\nso we get:";
	    narrative =
		entry_col_id == Column_ID.GOALS
		? EQUIV_BY_ + matchingsuppvsgoal_info
		: narrative_independent;
	    boolean flowing_with_preceding_row = true;
	    if ( row_index_to_follow + 1 < rows.size()
		    &&  rows.get(row_index_to_follow + 1)
				.get_flowswithprecedingrow()
		    )
		{
		narrative = narrative_independent;
		row_index_to_follow = end_part_seg_rows(row_index_to_follow);
		flowing_with_preceding_row = false;
		}
	    add_row(
		++row_index_to_follow,
		new Row(
			Column_ID.GOALS,
			new Entry(narrative),
			part_info,
			flowing_with_preceding_row
			)
		);
	    add_row(
		result = ++row_index_to_follow,
		new Row(
			entry_col_id = Column_ID.GOALS,
			new Entry(
				expr
				=
				new Expression(
					expressions_management
					.new_Symbol(Symbol.Specifier.TRUE)
					)
				),
			part_info,
			true
			)
		);
	    }

	String poss_concl =
	    possible_conclusion(expr, entry_col_id, part_info);
	if ( poss_concl != null ) {
	    note_used_row_in_part(row_index_to_follow, part_info);
	    add_row(
		++row_index_to_follow,
		new Row(
			entry_col_id,
			new Entry(poss_concl),
			part_info,
			true
			)
		);
	    if ( part_info.note_completing_root() && !part_info.is_root() ) {
		add_row(
		    rows.size(),
		    new Row(entry_col_id, new Entry(""), null)
		    );
		add_row(
		    rows.size(),
		    new Row(entry_col_id,
			new Entry(
			    "Thus, the theorem that was given is true"
			    + (part_info.singleton_subparts()
				? "."
				/*
				: ",\nconsidering all aspects of the situation."
				    upon handling all
				    for each element that needed to be handled
				    for each case that needed to be handled
				    for every component that needed to be handled
				    as everything necessary has been handled
				    since all possibilities have been addressed
				    based on handling the different
				    as all necessary ____ have been handled
					in this proof's different (sub)parts above
				    considering all of the above subparts of this proof subparts above.
				    considering the above breakdown of this proof into different subparts
				    considering the splitting of this proof into subparts above.
				    considering the division of this proof into subparts above.
				    by the above partitioning of
					    the overall proof here
					    this overall proof
					    this proof
					into subparts
					each of which has now been completed
				*/
				: ",\nby the above partitioning of this proof into subparts."
				)
			    ),
			null	// debatable
			)
		    );
		}
	    }

        added_row_index = result;
        }

    private void add(
	    int row_index_to_follow,
	    Column_ID entry_col_id,
	    String narrative_flowing_with_preceding_row,
	    String narrative_independent,
	    String comment_content,
	    String expr_text,
	    Expression expr
	    )
        {
	add(
	    row_index_to_follow,
	    entry_col_id,
	    narrative_flowing_with_preceding_row,
	    narrative_independent,
	    comment_content,
	    expr_text,
	    expr,
	    false
	    );
	}


    // |add()| for theorem and presuppositions
    void add(
                    Column_ID entry_col_id,
		    String narrative,
                    String comment,	// comment_content
                    String expr_text,
                    Expression expr
                    )
        {
	assert
	    entry_col_id == Column_ID.SUPPS
		||  entry_col_id == Column_ID.GOALS  &&  theorem_row == null
	    :  "entry_col_id == Column_ID.SUPPS\n"
		+  "\n||  entry_col_id == Column_ID.GOALS"
		+ "  &&  theorem_row == null";

	/*
	if ( hilbert_style  &&  entry_col_id == Column_ID.GOALS ) {
	    assert
		expr.ungroup().op_spec_equals(Symbol.Specifier.IMPLIES)
		:
		"expr.ungroup().op_spec_equals(Symbol.Specifier.IMPLIES)";
	    theorem_row =
		// kludge
		new Row(entry_col_id,
			new Entry(expr_text, expr),
			null,
			comment
			);
	    int result = rows.size() - 1;
	    for ( Expression goal = expr.ungroup();
		    goal.op_spec_equals(Symbol.Specifier.IMPLIES);
		    goal = goal.get_argument2().ungroup()
		    )
		{
		Expression antecedent = goal.get_argument1();
		LinkedList<Expression> presuppositions;
		if ( antecedent.op_spec_equals(Symbol.Specifier.AND) ) 
		    presuppositions = antecedent.multiary_op_args_ungroup();
		else {
		    presuppositions = new LinkedList<Expression>();
		    presuppositions.add(antecedent);
		    }
		for ( Expression presupposition : presuppositions ) {
		    add_row(
			++result,
			new Row(Column_ID.SUPPS, new Entry("Premise:"), null)
			);
		    add_row(
			++result,
			new Row(Column_ID.SUPPS,
				new Entry(presupposition),
				null,
				comment
				)
			);
		    }
		}
	    return  result;
	    }
	*/

	add(-1, entry_col_id, null, narrative, comment, expr_text, expr);
	}

    // second main version |add()| does some processing
    // used generally by deductions:
    void add(int[] selected_rows,
	    Column_ID entry_col_id,
	    String narrative_flowing_with_preceding_row,
	    String narrative_independent,
	    Expression expr
	    )
        {
        expr.clear_excessive_basic_grps_internal();
        expr = expr.ungroup();
	add(/*hilbert_style
		? rows.size() - 1
		:*/ selected_rows[selected_rows.length - 1],
	    entry_col_id,
	    narrative_flowing_with_preceding_row,
	    narrative_independent,
	    null,
	    expr.gen_text(),
	    expr
	    );
	note_used_rows_in_part(
		selected_rows,
		rows.get(added_row_index).get_partinfo()
		);
        }

    void add_elements(
	    LinkedList<Expression> elements,
	    Column_ID column_id,
	    String narrative_flowing_with_preceding_row,
	    String narrative_independent,
	    int[] selected_row_indexes,
	    boolean in_sequence
	    )
	{
	String narrative_front = narrative_flowing_with_preceding_row;
	int row_index_to_follow = selected_row_indexes[selected_row_indexes.length - 1];
	if ( !in_sequence
		&&  row_index_to_follow + 1 < rows.size()
		&&  rows.get(row_index_to_follow + 1)
			    .get_flowswithprecedingrow()
		)
	    {
	    narrative_front = narrative_independent;
	    //row_index_to_follow = end_flowing_rows(row_index_to_follow);
	    row_index_to_follow = end_part_seg_rows(row_index_to_follow);
	    }
	// not 'foreach' a.k.a. 'enhanced' |for| because proceeding
	// in reverse order to achieve certain linkages
	// plus allowing |table_model().add()| to |simplify()|
	// without interfering with this adding,
	// and using index in addition to element
	for ( ListIterator<Expression> elements_it =
		    elements.listIterator(elements.size());
		elements_it.hasPrevious();
		)
	    {
	    // developmental/pedagogical note: using
	    // the actual expression "elements_it.previousIndex() == 0"
	    // below where "is_follower" is being used now was erroneous
	    // because "elements_it.previous()" changes...
	    boolean front =  elements_it.previousIndex() == 0;
	    Expression expr = elements_it.previous();
	    expr.clear_excessive_basic_grps_internal();
	    expr = expr.ungroup();
	    add(
		row_index_to_follow,
		column_id,
		front
		    ?  narrative_front
		    :  (column_id == PB_TableModel.Column_ID.SUPPS
			? "and also:"
			: "or alternatively:"
			),
		front ? narrative_front : null,
		null,
		expr.gen_text(),
		expr,
		true
		);
	    }
	note_used_rows_in_part(
		selected_row_indexes,
		rows.get(added_row_index).get_partinfo()
		);
	}

    void add_elements(
	    LinkedList<Expression> elements,
	    Column_ID column_id,
	    String narrative_flowing_with_preceding_row,
	    String narrative_independent,
	    int[] selected_row_indexes
	    )
	{
	add_elements(
	    elements,
	    column_id,
	    narrative_flowing_with_preceding_row,
	    narrative_independent,
	    selected_row_indexes,
	    false
	    );
	}

    // independent of the preceding versions of |add()|
    void add_subparts(
	    Part_Info parent_part_info,
            int row_index_to_follow,
            Column_ID entry_col_id,
	    String narrative,
            LinkedList<Expression> exprs
            )
        {
	// assert  exprs.size() > 0  :  "exprs.size() > 0";
        // assert  selected_rows.length == 1;
	for( Part_Info[] parent_subparts;
		(parent_subparts = parent_part_info.get_subparts()) != null
		    //  &&  parent_subparts.length > 0
		    &&  parent_subparts.length > 1;	// don't split
		    					// inside transform.
		)
	    {
	    String[] part_options = new String[1 + parent_subparts.length];
		// |1 +| for parent part --- though it's actually placed at end
	    int i = part_options.length;
	    part_options[--i] =
		"really "
		+ parent_part_info.get_label()
		+ " instead of a subpart";
	    HashSet<Part_Info> parts_in_which_row_used =
		rows.get(row_index_to_follow).get_partsinwhichused();
	    String initialSelectionValue = null;
	    while ( --i >= 0 ) {
		part_options[i] = parent_subparts[i].get_label();
		if ( !parts_in_which_row_used.contains(part_options[i]) )
		    initialSelectionValue = part_options[i];
		}
	    if ( initialSelectionValue == null )
		break;
	    // String cancel_option = "Cancel";
	    String[] message_split
				// "have" but "should have" means ...
		= { "You should make this split inside one of the subparts of "
			+ parent_part_info.get_label()
			+ '.',
		    "(Otherwise, different parts are not considered consistent;"
		    ,
		    					// extant
		    "i.e. if you make this split outside the subparts that you have already, then you"
		    ,
		    "wouldn't be able to use the material of this split inside",
		    "any of those already existing subparts, and you wouldn't be able to use the",
		    "material of any of those already existing subparts inside this split.)",
		    "So please choose the subpart"
			// + " inside which you'll have this split:"
			// + " inside which you'll make this split:"
			// + " that you'll make this split inside:"
			+ " that'll have this split inside it:"
		    };
	    String[] message_transform
				// "have" but "should have" means ...
		= { "You should make this partition inside one of the subparts of "
			+ parent_part_info.get_label()
			+ '.',
		    "(Otherwise, different parts are not considered consistent;"
		    ,
		    						// extant
		    "i.e. if you make this partition outside the subparts that you already have, then you"
		    ,
		    "wouldn't be able to use the material of this partition inside",
		    "any of those subparts, and you wouldn't be able to use the",
		    "material of any of those subparts inside this partition.)",
		    "So please choose the subpart"
			// + " inside which you'll have this split:"
			// + " inside which you'll make this split:"
			// + " that you'll make this split inside:"
			+ " that'll have this split inside it:"
		    };
	    String opt =
		(String)
		    JOptionPane.showInputDialog(
			null,
			exprs.size() == 1
			    ?  message_transform
			    :  message_split,
			"Choose subpart for split",
			JOptionPane.QUESTION_MESSAGE,
			null,
			part_options,
			initialSelectionValue
			);
	    if ( opt == /* cancel_option */ null )
		return/*  -1*/;
	    while ( part_options[++i] != opt )
		;
	    if ( i < parent_subparts.length )
		parent_part_info = parent_subparts[i];
	    }
	note_used_row_in_part(row_index_to_follow, parent_part_info);
        Part_Info[] new_subparts =
	    parent_part_info.new_subparts(
		exprs.size(),
		entry_col_id == PB_TableModel.Column_ID.SUPPS
		);
	// not 'enhanced' |for| because using index as well as element
        row_index_to_follow = end_part_seg_rows(parent_part_info);
	int row_i = row_index_to_follow;
        for ( ListIterator<Expression> exprs_it = exprs.listIterator();
                exprs_it.hasNext();
                )
            {
            int i = exprs_it.nextIndex();
            add_row(
		++row_i,
		new Row(entry_col_id, new Entry(""), new_subparts[i])
		);
	    if ( exprs.size() > 1 )
		add_row(
		    ++row_i,
		    new Row(
			    entry_col_id,
			    new Entry(new_subparts[i].get_label() + ':'),
			    new_subparts[i]
			    )
		    );
            Expression expr = exprs_it.next().ungroup();
            add_row(
                ++row_i,
                new Row(
                        entry_col_id,
                        new Entry(expr),
                        new_subparts[i]
                        )
                );
            // fireTableRowsInserted(new_row_i, new_row_i);
            // fireTableRowsInserted(new_row_i, new_row_i);
            }
        //new_row_i = end_part_seg_rows(selected_rows[selected_rows.length - 1]);
        add_row(
            row_index_to_follow += 2,
	    /*
            new Row(entry_col_id,
		    new Entry(
                            prior_references(selected_rows) + narrative_base
			    ),
                    parent_part_info)
	    */
	    new Row(entry_col_id, new Entry(narrative), new_subparts[0])
            );
        added_row_index = row_index_to_follow + (exprs.size() == 1  ?  1  :  2);
        }

    // independent of the preceding versions of |add()|
    void add_subparts(
            int row_index_to_follow,
            Column_ID entry_col_id,
	    String narrative,
            LinkedList<Expression> exprs
            )
        {
	add_subparts(
	    rows.get(row_index_to_follow).get_partinfo(),
	    row_index_to_follow,
	    entry_col_id,
	    narrative,
	    exprs
	    );
	}

    boolean parts_consistent(int row_a, int row_b) {
        Row min_row = rows.get(Math.min(row_a, row_b));
        return
            min_row.get_partinfo()
                .has_as_some_subpart(
                    rows.get(Math.max(row_a, row_b)).get_partinfo()
                    );
        }

    public static final String HEAD_TEXT =
	"Proof of the following formula:"
	+ "                               "
	+ '\n';

    public String get_identification_one_line() {
	if ( rows.size() <= 0 )
	    return  "";
	Row row0 = rows.get(0);
	long timestamp_end = rows.get(rows.size() - 1).timestamp;
	return
	    timestamp_end
	    + ","
	    + row0.timestamp
	    + ','
	    + (timestamp_end - row0.timestamp);
	}

    void output_as_HTML(Writer writer) throws IOException {
	Row row0 =  rows.size() > 0  ?  rows.get(0)  :  null;
        if ( row0 != null  &&  theorem_row != row0  &&  theorem_row != null ) {
	    if ( theorem_row.timestamp < row0.timestamp )
		row0 = theorem_row;
            writer.write("<H4>" + HEAD_TEXT + "</H4>\n" + "<BLOCKQUOTE>\n");
            Entry.output_as_HTML(
                    writer,
                    theorem_row.get_entry().get_text(),
                    true
                    );
            writer.write("</BLOCKQUOTE>\n<BR>\n\n");
            }
        writer.write("<TABLE BORDER>\n");
	/*
        Row.output_header_as_HTML(writer);
	*/
	// Consider indicating 'preferred' widths
	writer.write("\n<TR>\n");
	for ( Map.Entry<Column_ID,String> c_n : cols_names.entrySet() )
	    if ( c_n.getKey() != Column_ID.USED ) {
		writer.write("    <TH> ");
		boolean column_empty = true;
		for ( int row_i = 0; row_i < rows.size(); row_i++ ) {
		    if ( getValueAt(row_i, c_n.getKey().ordinal()) != null
			    ||  c_n.getKey() == Column_ID.COMMENTS
				&&  rows.get(row_i).entry.has_expr()
				&&  !rows.get(row_i).used_at_all()
			    )
			{
			column_empty = false;
			break;
			}
		    }
		writer.write(column_empty ? "&nbsp;" : c_n.getValue());
		writer.write(" </TH>\n");
		}
	writer.write("\n</TR>\n");
        for ( Row row : rows )
            row.output_as_HTML(writer);
        writer.write("\n</TABLE>\n");
	if ( row0 != null ) {
	    long timestamp_end = rows.get(rows.size() - 1).timestamp;
	    writer.write(
		    				// hash codes
		    "\n<SMALL><P ALIGN=RIGHT><VAR>\nidentification:<BR>\n"
			+ timestamp_end
			+ "<BR>\n"
		    + row0.timestamp
			+ "<BR>\n"
		    + (timestamp_end - row0.timestamp)
			+ "</VAR></P></SMALL>\n"
		    );
	    }
        }

    void delete_last_row() {
        if ( rows.remove(rows.size() - 1) == theorem_row )
            theorem_row = null;
	time_of_last_mod = System.currentTimeMillis();
        fireTableRowsDeleted(rows.size(), rows.size());
        }
    }