/* 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.*;
import javax.swing.text.*;
import javax.swing.event.*;
import javax.swing.table.*;
import java.awt.*;
import java.awt.event.*;
import java.util.*;
import java.util.regex.*;
import java.io.Writer;
import java.io.IOException;

/**
 * Administration of material in a deductive tableau cell.
 * The material is either an <CODE>Expression</CODE>, or it is just
 * plain-text narrative.
 * @author Hugh McGuire
 */
class Entry implements java.io.Serializable {
    private Expression expr;
    private String text;
    private String[] lines;     // this is for convenience
    private Expression[] selection_map;
        // rem. not allowing external code to use this to get subexpressions
        // because safeguarding...
    private Expression subexpr_selected;
    private HashSet<Expression> subexprs_used = new HashSet<Expression>();
    private int last_width_addressed;
    private float last_fontsize_addressed;
    /*
    private int highlight_start, highlight_limit;
    */

    void context_map(Expression expr, Expression[] map) {
	if ( expr.get_operator().get_begin() < 0 )
	    /*
	     * |Expressions_Mgmt.parse()| adds grouping parentheses
	     * to material such as the following:
		    3 + 4 - 5
			*
		    6 - 7 + 8
	     */
	    return;
        for ( int i = expr.get_operator().get_begin();
		i < expr.get_operator().get_limit();
		i++
	    )
            selection_map[i] = expr;
        if ( expr.get_argument1() != null )
            context_map(expr.get_argument1(), selection_map);
        if ( expr.get_argument2() != null )
            if ( expr.get_argument2()
			.op_spec_equals(Symbol.Specifier.CLOSING_DELIMITER)
		    &&  expr.get_argument2().get_operator().get_text().length()
			== 1
		    )
		{
                assert  expr.op_spec_equals(Symbol.Specifier.OPENING_DELIMITER);
                selection_map[expr.get_argument2().get_operator().get_begin()]
		    = expr;
                }
            else
                context_map(expr.get_argument2(), selection_map);
        }

    private void change_text(String text_given) {
        text = text_given;
        selection_map = new Expression[text.length()];
        context_map(expr, selection_map);
	/*
	// debugging:
	for ( int i = 0; i < selection_map.length; i++ )
	    System.err.println(
                "selection_map[" + i + "]:  " + selection_map[i]
                );
	*/
        lines = text.split("\n");
        }

    Entry(String text0) {
	lines = (text = text0).split("\n");
	    // Be advised that splitting text containing only "\n"
	    // yields an array of length zero, not say an array
	    // containing an empty string.
	}

    Entry(String expr_text_given, Expression expr_given) {
        expr = (Expression) expr_given.clone();
                                    // Invoking |clone()| here may be
                                    // excessively paranoid;
                                    // but in 2006 the handling of
                                    // simplification
				    // in |PB_TableModel.add()|
                                    // relies on this.
        change_text(expr_text_given);
        last_width_addressed = Integer.MAX_VALUE;
        last_fontsize_addressed = Integer.MAX_VALUE;
        subexpr_selected = expr;
        }

    Entry(Expression expr_given) { this(expr_given.gen_text(), expr_given); }


    String get_text() { return  text; }

    String get_line(int index) { return  lines[index]; }

    boolean has_expr() { return  expr != null; }

    Expression get_expr_clone() { return  (Expression) expr.clone(); }
        // The |clone()|ing here is crucial:
        // [1] it avoids any mucking with subparts of this entry's |expr|
        // (there's no other public access to the |expr| here),
        // yet [2] it provides lots of useful information since the clone
	// carries all context values.

    int get_expr_begin() { return  expr.get_begin(); }
    int get_expr_limit() { return  expr.get_limit(); }

    int get_text_rows() { return lines.length; }

    int get_selection_start() { return subexpr_selected.get_begin(); }
    int get_selection_limit() { return subexpr_selected.get_limit(); }

    /*
    int get_selected_op_begin() {
	return  subexpr_selected.ungroup().get_operator().get_begin();
	}
    int get_selected_op_limit() {
	return  subexpr_selected.ungroup().get_operator().get_limit();
	}
    boolean subexpr_selected_has_arg1() {
	return  subexpr_selected.ungroup().get_argument1() != null;
	}
    */

    Symbol.Specifier get_expr_op_spec() {
	return  expr.get_operator().get_specifier();
	}

    // NEED TO UPDATE |appears_applicable()| IN |Ded_Action.java|
    // (REALLY USING THE NEW |Deduction_Prep[]| ARGUMENT(S))
    // TO GET RID OF THE FOLLOWING TWO METHODS:

    Symbol.Specifier get_selected_subexpr_ungroup_op_spec() {
	return  subexpr_selected.ungroup().get_operator().get_specifier();
	}

    boolean selected_subexpr_ungroup_is_variable(
	    Expressions_Mgmt expressions_mgmt
	    )
	{
	return  expressions_mgmt.is_variable(subexpr_selected.ungroup());
	}

    boolean expr_equiv_form(Expression other_expr) {
        return  expr.equivalent_form(other_expr);
        }

    void note_used_subexpr_selected() { subexprs_used.add(subexpr_selected); }

    public void try_select(int sel_start, int sel_limit) {
	Expression requested_select_expr =
	    expr.get_subexpr_covering(sel_start, sel_limit);
	if ( requested_select_expr != null )
		subexpr_selected = requested_select_expr;
	}

    static Pattern ref_start = Pattern.compile("\\((\\d+)\\)");

    void increment_narrative_ref_nums_geq(int ref_num_limit) {
	if ( has_expr() )
	    return;
	Matcher ref_start_matcher = ref_start.matcher(text);
	StringBuffer new_text_sb = new StringBuffer();
	    // As of 2008:March, |Matcher.appendReplacement()|
	    // and |Matcher.appendTail()| required |StringBuffer|,
	    // not |StringBuilder|; I conjecture that |Matcher| tries
	    // to ensure synchronized.
	while ( ref_start_matcher.find() ) {
	    int ref_num =
		    Integer.parseInt(
			text.substring(
			    ref_start_matcher.start(1),
			    ref_start_matcher.end(1)
			    )
			);
	    if ( ref_num >= ref_num_limit )
		ref_start_matcher.appendReplacement(
			new_text_sb, 
			"(" + (ref_num + 1) + ')'
			);
	    }
	if ( new_text_sb.length() == 0 )
	    return;
	ref_start_matcher.appendTail(new_text_sb);
	lines = (text = new_text_sb.toString()).split("\n");
	}




    /* derived from |ColorRenderer.java| which was obtained via:
     *   http://java.sun.com/docs/books/tutorial/uiswing/components/
     *	    example-1dot4/ColorRenderer.java
     * on May 15, 2006
     */
    static class Renderer extends JTextPane implements TableCellRenderer {
	static final String EXPR_FONT_FAMILY = "Monospaced";
						// tried |darker()| when
						// colored selected op itself

	static final SimpleAttributeSet attrs_expr_regular
	    = new SimpleAttributeSet();
	static final SimpleAttributeSet attrs_subexpr_used
	    = new SimpleAttributeSet();
	static final SimpleAttributeSet attrs_op_used
	    = new SimpleAttributeSet();
	/*
	static final SimpleAttributeSet attrs_highlight
	    = new SimpleAttributeSet();
	*/
	static final SimpleAttributeSet attrs_narrative
	    = new SimpleAttributeSet();

	static {
	    StyleConstants.setFontFamily(attrs_expr_regular, EXPR_FONT_FAMILY);
	    StyleConstants.setUnderline(attrs_subexpr_used, true);
			// Bold for selected op wasn't visible;
			// |setForeground()| for selected op with underlining
			// made "<" appear like "&leq;".
	    StyleConstants.setBold(attrs_op_used, true);
	    }


	private Font expr_font;
        //final JTable table;
	// NO LONGER TRYING TO USE |table.getSelectionBackground()|
	// SO COULD RETURN THE FOLLOWING TO |static| WITH THE PRECEDING
	final SimpleAttributeSet attrs_subexpr_selected
	    = new SimpleAttributeSet();
	final SimpleAttributeSet attrs_op_selected = new SimpleAttributeSet();

        Renderer(/*JTable table_given*/) {
            //table = table_given;
            expr_font = new Font("Monospaced", Font.PLAIN, getFont().getSize());

	    StyleConstants.setBackground(
		    attrs_subexpr_selected,
		    //table.getSelectionBackground()
		    Color.GREEN.brighter()
		    );
			// Bold alone for selected op wasn't visible;
			// |setForeground()| for selected op with underlining
			// made "<" appear like "&leq;".
	    StyleConstants.setBackground(
		    attrs_op_selected,
		    //table.getSelectionBackground().darker()
			// more |brighter()| wasn't different
		    //Color.GREEN.brighter().brighter().brighter()
		    //Color.YELLOW
		    Color.ORANGE
		    );
	    // Note some such as "&rarr;" don't appear different bold
	    StyleConstants.setBold(attrs_op_selected, true);
	    /*
	    StyleConstants.setForeground(
		    attrs_op_selected,
		    Color.BLACK.brighter()
		    );
	    */

            setOpaque(true); //MUST do this for background to show up.
            }

        void underline_all_occurrences(
                String id,
                Expression subexpr_b,
                Entry entry,
                Rectangle cell_rect,
                FontMetrics fm
                )
            {
            /*
            if ( subexpr_b == null )
                return;
            */
            if ( subexpr_b.op_spec_equals(Symbol.Specifier.IDENTIFIER)
                    &&  subexpr_b.get_operator().get_text().equals(id)
                    &&  subexpr_b.get_argument1() == null
                    )
		/*
                underline(subexpr_b.get_begin(),
                            subexpr_b.get_limit(),
                            entry,
                            cell_rect,
                            fm
                            )*/;
            if ( subexpr_b.get_argument1() != null )
                underline_all_occurrences(
                    id,
                    subexpr_b.get_argument1(),
                    entry,
                    cell_rect,
                    fm
                    );
            if ( subexpr_b.get_argument2() != null )
                underline_all_occurrences(
                    id,
                    subexpr_b.get_argument2(),
                    entry,
                    cell_rect,
                    fm
                    );
            }

        static int count_lines(String text) {
            // Doing more than simply counting newline characters
            // in case last line may not be terminated with a newline character.
            // Not simply doing |text.split("\n").length()| because that seems
            // ~~wasteful.
            int i = text.length();
            int result =
                text.length() > 0  &&  text.charAt(i - 1) != '\n'
                ?  1
                :  0;
            while ( --i >= 0 )
                if ( text.charAt(i) == '\n' )
                    result++;
            return  result;
            }

        public Component getTableCellRendererComponent(
                                JTable table, Object ent_o,
                                boolean isSelected, boolean hasFocus,
                                int row, int column
                                )
            {
	    float font_size = table.getFont().getSize2D();
	    Font font = getFont().deriveFont(font_size);
	    expr_font = expr_font.deriveFont(font_size);
	    setFont(font);	// debatable
            setBackground(
		isSelected
		? table.getSelectionBackground()
		: table.getBackground()
		);
            if ( ent_o == null )
		try {
		    getStyledDocument()
			.remove(0, getStyledDocument().getLength());
		    }
		catch ( BadLocationException e ) {
		    e.printStackTrace();
		    }
		finally {
		    return  this;
		    }
            Entry entry = (Entry) ent_o;
            int current_width =
                table.getColumnModel().getColumn(column).getWidth()
		- table.getIntercellSpacing().width;	// ~~kludge
	    int excessive_width_line_i;
	    FontMetrics fontmetrics = getFontMetrics(font);
	    FontMetrics expr_fontmetrics = getFontMetrics(expr_font);
	    for ( excessive_width_line_i = entry.lines.length;
		    --excessive_width_line_i >= 0;
		    )
		if ( current_width
			<
			(entry.has_expr() ? expr_fontmetrics : fontmetrics)
				.stringWidth(
				    entry.lines[excessive_width_line_i]
				    )
			)
		    break;
	    int nonempty_lines = 0;
	    for ( String line : entry.lines )
		if ( line.length() > 0 )
		    nonempty_lines++;
	    int lines_considering_wrapping = 0;
            if ( 0 <= excessive_width_line_i
		    ||  nonempty_lines > 1
			&& (entry.last_width_addressed < current_width
			    || font_size < entry.last_fontsize_addressed
			    )
		    )
		{
		if ( entry.has_expr() )
		    entry.change_text(
			    entry.expr.try_adjust_lines_to_fit(
				current_width,
				expr_fontmetrics
				    // though using |"Monospaced"|,
				    // not all characters have same width
				    // (in 2007:June on a Mac)
				)
			    );
		else
		    for ( String line : entry.lines )
			lines_considering_wrapping +=
				1
				    // wouldn't add 1
				    // if here counted just the additional
				    // lines due to wrapping
				+
				fontmetrics.stringWidth(line) / current_width;
					//- 1
                entry.last_width_addressed = current_width;
                entry.last_fontsize_addressed = font_size;
                }
	    /*
	     * TO ENSURE UNDERLINE VISIBLE AT BOTTOM OF CELL,
	     * NEED SOMETHING LIKE MARGIN;
	     * TUTORIAL CODE HAD:
	     *         textPane.setMargin(new Insets(5,5,5,5));
	     *
	    // DON'T COMPLETELY FLUSH BOTTOM BECAUSE UNDERLINE MAY NOT
	    // BE VISIBLE ON FLOOR OF CELL:
            blank_lines_for_expr_flush_bottom--;
	     */
	    try {
		getStyledDocument().remove(0, getStyledDocument().getLength());
		getStyledDocument()
		    .insertString(
			0,
			entry.text,
			entry.has_expr() ? attrs_expr_regular : attrs_narrative
			);
		}
	    catch ( BadLocationException e ) {
		e.printStackTrace();
		return  this;
		}

	    /* the following made dialogs including |JOptionPane| ones
	     * not display parts:
            table.setRowHeight(
                row,
                Math.max(table.getRowHeight(row), getRows() * getRowHeight())
                );
	     */
	    int height_need =
		(lines_considering_wrapping > 0
		    ?  lines_considering_wrapping * fontmetrics.getHeight()
		    :  getPreferredSize().height
		    )
		+ table.getRowMargin();
		// Regarding |+ table.getRowMargin()|,
		// see documentation of |JTable.setRowHeight()|.
				
	    if ( table.getRowHeight(row) != height_need )
		table.setRowHeight(row, height_need);

	    /*
	    if ( entry.highlight_start < entry.highlight_limit )
		getStyledDocument().setCharacterAttributes(
		    entry.highlight_start,
		    entry.highlight_limit - entry.highlight_start,
		    attrs_highlight,
		    false
		    );
	    */

	    if ( isSelected  &&  entry.subexpr_selected != null )  {
		// Originally I had here:
		// if ( entry.subexpr_selected != entry.expr ) 
		// but students suggested otherwise.
		getStyledDocument().setCharacterAttributes(
		    entry.subexpr_selected.get_begin(),
		    entry.subexpr_selected.get_limit()
			- entry.subexpr_selected.get_begin(),
		    attrs_subexpr_selected,
		    false
		    );

		/*
		if ( entry.subexpr_selected
				.op_spec_equals(Symbol.Specifier.IDENTIFIER)
			&&  entry.subexpr_selected.get_argument1() == null
			&&  BOOLEAN
			)
		    underline_all_occurrences(
			entry.subexpr_selected.get_operator().get_text(),
			entry.expr,
			entry,
			/ * cell_rect * /null,
			(entry.has_expr() ? expr_fontmetrics : fontmetrics)
			);

		else
		*/
		if ( entry.subexpr_selected.ungroup().get_argument2()
			    != null
			    /* INSTEAD OF THAT CONDITION, CONSIDER:
			     * if ( entry.subexpr_selected.get_begin()
			     *		    < op_selected.get_begin()
			     *		&&  op_selected.get_limit()
			     *		    < entry.subexpr_selected.get_limit()
			     *		)
			     */
			    )
		    {
		    Symbol op_selected =
			entry.subexpr_selected.ungroup().get_operator();
		    getStyledDocument().setCharacterAttributes(
			op_selected.get_begin(),
			op_selected.get_limit() - op_selected.get_begin(),
			attrs_op_selected,
			false
			);
		    /*
		    SimpleAttributeSet attrs_selected_op_size
			= new SimpleAttributeSet();
		    StyleConstants.setFontSize(
			attrs_selected_op_size,
			(int)
			(StyleConstants.getFontSize(
				getStyledDocument().getCharacterAttributes()
				)
			    *
			    1.17	// This factor should suffice for
			    		// basic font increments, of which
					// one of the proportionally greatest
					// is from 12 to 14.
			    )
			);
		    getStyledDocument().setCharacterAttributes(
			entry.get_selected_op_begin(),
			entry.get_selected_op_limit()
			    - entry.get_selected_op_begin(),
			attrs_selected_op_size,
			false
			);
		    */
		    }

		}

	    for ( Expression subexpr_used : entry.subexprs_used )  {
		if ( subexpr_used != entry.expr )
		    getStyledDocument().setCharacterAttributes(
			subexpr_used.get_begin(),
			subexpr_used.get_limit() - subexpr_used.get_begin(),
			attrs_subexpr_used,
			false
			);
			// CONSIDER MORE FINE CONDITION
			// SO FOR EXAMPLE |&not;| BOLD BUT PREDICATE NOT BOLD
		if ( entry.subexpr_selected.ungroup().get_argument2() != null )
		    {
		    Symbol op_used = subexpr_used.ungroup().get_operator();
		    getStyledDocument().setCharacterAttributes(
			op_used.get_begin(),
			op_used.get_limit() - op_used.get_begin(),
			attrs_op_used,
			false
			);
		    }

		/*
		if ( entry.subexpr_selected
				.op_spec_equals(Symbol.Specifier.IDENTIFIER)
			&&  entry.subexpr_selected.get_argument1() == null
			)
		    underline_all_occurrences(
			entry.subexpr_selected.get_operator().get_text(),
			entry.expr,
			entry,
			/ * cell_rect * /null,
			(entry.has_expr() ? expr_fontmetrics : fontmetrics)
			);
		*/
		}

            return this;
            }
        }




    static class Editor extends AbstractCellEditor
                             implements TableCellEditor, CaretListener
	{
	JTable table;
        JTextPane jtextpane;
        Entry entry;
	SimpleAttributeSet attrs_expr_regular, attrs_subexpr_selected;
	int row;
	int mark, dot;

        Editor() {
            //Set up the editor (from the table's point of view),
            //which is a |JTextPane|.
            //which is just a selection tool from the user's point of view.
            jtextpane = new JTextPane();
	    jtextpane.setEditable(false);
	    jtextpane.addCaretListener(this);
	    attrs_expr_regular = new SimpleAttributeSet();
	    StyleConstants.setFontFamily(attrs_expr_regular, "Monospaced");
	    attrs_subexpr_selected = new SimpleAttributeSet(attrs_expr_regular);
	    StyleConstants.setUnderline(attrs_subexpr_selected, true);
	    jtextpane.addMouseListener(
		new MouseAdapter() {
		    long mousepressed_when;

		    public void mousePressed(MouseEvent me) {
			mousepressed_when = me.getWhen();
			}

		    // wasn't seeing any |mouseClicked()|:
		    /*
		    public void mouseClicked(MouseEvent me) {
			}
		    */

		    public void mouseReleased(MouseEvent me) { 
			final long RESELECT_DELAY = 200;	// milliseconds
			int sel_start = Math.min(mark, dot),
			    sel_limit = Math.max(mark, dot);
			/*
			if ( me.isShiftDown()
				||  me.getButton() == MouseEvent.BUTTON3
				)
			    {
			    entry.highlight_start = sel_start;
			    entry.highlight_limit = sel_limit;
			    }
			else
			*/
			if (
				entry.has_expr()
				&& (me.getClickCount() == 2
				    ||  mousepressed_when + RESELECT_DELAY
					<
					me.getWhen()
				    )
				)
			    {
			    while ( sel_start < sel_limit
				    &&  Character.isWhitespace(
					    entry.text.charAt(sel_start)
					    )
				    )
				sel_start++;
			    while ( sel_start < sel_limit
				    &&  Character.isWhitespace(
					    entry.text.charAt(sel_limit - 1)
					    )
				    )
				sel_limit--;
			    entry.try_select(sel_start, sel_limit);
			    }

			table.removeRowSelectionInterval(row, row);
			table.addRowSelectionInterval(row, row);
			fireEditingStopped();
			}
		    }
		);
            }


        //Implement the one CellEditor method that AbstractCellEditor doesn't.
        public Object getCellEditorValue() {
            return entry;
            }

        //Implement the one method specified by TableCellEditor.
        public Component getTableCellEditorComponent(JTable table_given,
                                                     Object ent_o,
                                                     boolean isSelected,
                                                     int r,
                                                     int column)
            {
	    table = table_given;
	    jtextpane.setFont(
		jtextpane.getFont().deriveFont(table.getFont().getSize2D())
		);
            if ( ent_o == null ) {
		try {
		    jtextpane.getStyledDocument()
			.remove(0, jtextpane.getStyledDocument().getLength());
		    }
		catch ( BadLocationException e ) {
		    e.printStackTrace();
		    }
                return  jtextpane;
                }
            entry = (Entry) ent_o;
	    /*
	    if ( !entry.has_expr() )
		return  null;
	    */
	    row = r;
	    jtextpane.setBackground(table.getBackground());
	    try {
		jtextpane.getStyledDocument()
		    .remove(0, jtextpane.getStyledDocument().getLength());
		jtextpane.getStyledDocument()
		    .insertString(0, entry.text, attrs_expr_regular);
		}
	    catch ( BadLocationException e ) {
		e.printStackTrace();
		}
            return jtextpane;
            }

	public void caretUpdate(CaretEvent ce) {
	    mark = ce.getMark();
	    dot = ce.getDot();
	    }

        }



    private static void output_as_HTML(
	    Writer writer,
	    String string,
	    boolean pre,
	    Entry entry
	    )
		    throws IOException 
	{
	if ( string == null  ||  string.equals("") ) {
	    // ~~kludge?
	    writer.write("&nbsp;");
	    return;
	    }

	// not 'enhanced' |for| because using index as well as element
	HashSet<Integer> subexprs_to_highlight_beginnings = new HashSet<Integer>();
	HashSet<Integer> subexprs_to_highlight_limits = new HashSet<Integer>();
	HashSet<Integer> ops_to_highlight_beginnings = new HashSet<Integer>();
	HashSet<Integer> ops_to_highlight_limits = new HashSet<Integer>();
	if ( entry != null )
	    if ( entry.subexprs_used.isEmpty() ) {
		if ( entry.subexpr_selected != entry.expr ) {
		    subexprs_to_highlight_beginnings.add(entry.subexpr_selected.get_begin());
		    subexprs_to_highlight_limits.add(entry.subexpr_selected.get_limit());
		    }
			// CONSIDER MORE FINE CONDITION
			// SO FOR EXAMPLE |&not;| BOLD BUT PREDICATE NOT BOLD
		//if ( subexpr_selected.ungroup().get_argument2() != null )
		if ( entry.subexpr_selected.ungroup().get_argument1() != null
			&&  !entry.subexpr_selected.ungroup().op_spec_equals(
				Symbol.Specifier.IDENTIFIER
				)
			)
		    {
		    Symbol op_selected = entry.subexpr_selected.ungroup().get_operator();
		    ops_to_highlight_beginnings.add(op_selected.get_begin());
		    ops_to_highlight_limits.add(op_selected.get_limit());
		    }
		}
	    else
		for ( Expression subexpr_used : entry.subexprs_used ) {
		    if ( subexpr_used != entry.expr ) {
			subexprs_to_highlight_beginnings.add(subexpr_used.get_begin());
			subexprs_to_highlight_limits.add(subexpr_used.get_limit());
			}
			    // CONSIDER MORE FINE CONDITION
			    // SO FOR EXAMPLE |&not;| BOLD BUT PREDICATE NOT BOLD
		    //if ( subexpr_used.ungroup().get_argument2() != null )
		    if ( subexpr_used.ungroup().get_argument1() != null
			    &&  !subexpr_used.ungroup().op_spec_equals(
				    Symbol.Specifier.IDENTIFIER
				    )
			    )
			{
			Symbol op_used = subexpr_used.ungroup().get_operator();
			ops_to_highlight_beginnings.add(op_used.get_begin());
			ops_to_highlight_limits.add(op_used.get_limit());
			}
		    }
	/*
	subexprs_to_highlight_beginnings.removeAll(subexprs_used_limits);
	subexprs_to_highlight_limits.removeAll(subexprs_used_beginnings);
	*/
	// address zero-width operators (|QUANT_SEP|, |TIMES| in future):
	ops_to_highlight_beginnings.removeAll(ops_to_highlight_limits);
	ops_to_highlight_limits.removeAll(ops_to_highlight_beginnings);

	if ( pre )
	    writer.write("<PRE>\n");
	char c = '\0';
	boolean in_quotation = false;
	for ( int i = 0; i < string.length(); i++ ) {
	    if ( subexprs_to_highlight_beginnings.contains(i) )
		writer.write("<U>");
	    if ( ops_to_highlight_beginnings.contains(i) )
			// "<FONT COLOR=DARKGREEN>"
			// Underlining made "<" appear like "&leq;"
		writer.write("<B><BIG>");
	    c = string.charAt(i);
	    if ( c == '&' )
		writer.write("&amp;");
	    else if ( c == '<' )
		writer.write("&lt;");
	    else if ( c == '>' )
		writer.write("&gt;");
	    else if ( c == ' '
			&&  !pre
			&&  i + 1 < string.length()
			&&  string.charAt(i + 1) == ' '
			)
		writer.write("&nbsp;");
	    else if ( c == '\t'  &&  !pre )
		writer.write("&nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; ");
	    else if ( c == '"'  &&  !pre ) {
		writer.write(in_quotation ? "</CODE>\"" : "\"<CODE>");
		in_quotation = !in_quotation;
		}
	    else if ( 0 <= c  &&  c <= Byte.MAX_VALUE ) {
			// kludging 'isASCII()'
		// Consider not doing this:
		if ( !pre  &&  c == '\n' ) {
		    writer.write("<BR>");
		    while ( i + 1 < string.length()
			    &&  string.charAt(i + 1) == ' '
			    )
			{
			++i;
			c = ' ';
			writer.write("&nbsp;");
			}
		    }
		writer.write(c);
		}
	    else if ( '\u2081' <= c  &&  c <= '\u2083' )
		// avoid excessive spacing at end of |&#X2081;| et al.
		writer.write(
			"<SMALL><SUB>"
			+ (c - '\u2080')
			+ "</SUB></SMALL>"
			);
	    else {
		writer.write("&#X");
		//writer.write(Integer.toString((int) c, 16));
		writer.write(Integer.toHexString(c).toUpperCase());
		writer.write(';');
		}
	    if ( ops_to_highlight_limits.contains(i + 1) )
		writer.write("</BIG></B>");
	    if ( subexprs_to_highlight_limits.contains(i + 1) )
		writer.write("</U>");
	    }
	if ( c != '\n' )
	    if ( pre )
		writer.write('\n');
	    /*
	    else
		writer.write("<BR>\n");
	    */
	if ( pre )
	    writer.write("</PRE>\n");
	}

    static void output_as_HTML(Writer writer, String string, boolean pre)
	    throws IOException 
	{
	output_as_HTML(writer, string, pre, null);
	}

    static void output_as_HTML(Writer writer, String string)
	    throws IOException 
	{
	/*
	if ( string != null  &&  string.startsWith(EQUIV_BY_) ) {
	    writer.write(EQUIV_BY_OUT);
	    string = string.substring(EQUIV_BY_.length());
	    }
	if ( string != null  &&  string.startsWith(REDUCES_BY_) ) {
	    writer.write(REDUCES_BY_OUT);
	    string = string.substring(REDUCES_BY_.length());
	    }
	*/
	output_as_HTML(writer, string, false);
	}

    /*
    static void output_as_HTML(Writer writer, Object s_o)
	    throws IOException 
	{
	output_as_HTML(writer, (String) s_o);
	}
    */

    void output_as_HTML(Writer writer) throws IOException {
	if ( has_expr() )
	    output_as_HTML(writer, get_text(), true, this);
	else
	    output_as_HTML(writer, get_text());
	}

    }