Package wprover

Class DrawTextProcess

java.lang.Object

wprover.DrawBase

wprover.DrawProcess

wprover.DrawTextProcess

All Implemented Interfaces:

java.awt.event.ActionListener, java.awt.print.Printable, java.util.EventListener

public class DrawTextProcess
extends DrawProcess

DrawTextProcess is a class that handles the construction and animation of geometric diagrams based on textual input. It extends the DrawProcess class and provides methods for managing construction steps, point attributes, and geometric constraints.

Field Summary

Fields inherited from class wprover.DrawProcess

ANIMATION, ARROW, AUTOSHOWSTEP, CONSTRUCT_FROM_TEXT, CTrackPt, DEFINEPOLY, DRAWTRIALL, DRAWTRISQISO, EQMARK, EQUIVALENCE, FREE_TRANSFORM, gt, HIDEOBJECT, LOCUS, MOVE, MOVENAME, MULSELECTSOLUTION, nd, NTANGLE, panel, PARALLELOGRAM, PROVE, RA_TRAPEZOID, RAMARK, RATIO, RECTANGLE, SANGLE, SELECT, SETCCTANGENT, SETEQANGLE3P, SETEQSIDE, SETTRACK, SHOWOBJECT, status, TRANSFORM, TRANSLATE, TRAPEZOID, TRIANGLE, U_Obj, VIEWELEMENT, ZOOM_IN, ZOOM_OUT

Fields inherited from class wprover.DrawBase

anglelist, BARYCENTER, CatchList, CatchPoint, CatchType, catchX, catchY, CCTANGENT, charset, circlelist, CIRCUMCENTER, constraintlist, CurrentAction, D_3PCIRCLE, D_ABLINE, D_ALINE, D_ANGLE, D_BLINE, D_CCLINE, D_CIR_BY_DIM, D_CIRCLE, D_CIRCLEBYRADIUS, D_IOSTRI, D_LINE, D_MIDPOINT, D_PARELINE, D_PERPLINE, D_PFOOT, D_POINT, D_POLYGON, D_PRATIO, D_PSQUARE, D_PTDISTANCE, D_SQUARE, D_TCLINE, D_TEXT, D_TRATIO, DISTANCE, distancelist, DRAWGRID, file, footMarkLength, footMarkShown, gridColor, GridX, GridY, gxInstance, H_LINE, Height, INCENTER, isPointOnIntersection, isPointOnObject, lan, linelist, LRATIO, MEET, MIRROR, mouseCatchX, mouseCatchY, mouseInside, MouseX, MouseY, name, ORTHOCENTER, otherlist, paraBackup, paraCounter, parameter, pblist, pcircleCounter, PERPWITHFOOT, plineCounter, pnameCounter, pointlist, poly, polygonlist, polylist, POOL, pptrans, SelectList, SETEQANGLE, SNAP, STATUS, textlist, tracelist, V_LINE, Width

Fields inherited from interface java.awt.print.Printable

NO_SUCH_PAGE, PAGE_EXISTS

Constructor Summary

Constructors

Constructor	Description
DrawTextProcess()

Method Summary

Modifier and Type	Method	Description
CLine	add_Line(CPoint a, CPoint b)	Adds a line between two points.
void	addAcongFlash(Cond co, boolean cl)	Adds an angle congruence flash effect for a given condition.
void	addAllLn(int[] pp)	Adds all lines based on the given points.
void	addAngleToList2(CAngle ag)	Adds a CAngle to the angle list.
void	addAreaFlash(wprover.MAssertion ass)	Adds a flash effect for an area based on an assertion.
void	addAreaFlash1(wprover.MAssertion ass)	Adds a flash effect for an area based on an assertion.
void	addaux(CProveText cpt)	Processes auxiliary proof text to add the corresponding flashes, marks, or polygons.
void	addAuxPoint(AuxPt ax)	Adds an auxiliary point to the construction.
void	addCGFlash(CPoint p1, CPoint p2, CPoint p3, CPoint p4)	Adds a flash effect for congruent segments.
void	addConcLineOrCircle(Cond cc)	Adds lines or circles based on the given condition.
java.util.Vector	addCondAux(Cons co, boolean aux)	Adds auxiliary conditions for a given condition.
void	addCongFlash(Cond co, boolean cl)	Adds a congruence flash effect for a given condition.
JFlash	addFlashAngle(int a, int b, int c, int d)	Creates or retrieves a flash angle based on the given point indices.
JFlash	addFlashXtermAngle(XTerm x)	Creates or retrieves a flash angle based on an XTerm object.
boolean	addFreePt(Cons c)	Adds a free point to the construction.
boolean	addGTPt(Cons c)	Adds a geometric term point to the construction.
void	addInfinitelineFlash(CPoint p1, CPoint p2)	Adds a flash effect for an infinite line.
void	addlineFlash(CPoint p1, CPoint p2)	Adds a flash effect for a line.
CLine	addLnWC(CPoint a, CPoint b, int color, int d)	Adds a line with specific color and dash style between two points.
void	addObjectFlash(CClass c1, CClass c2, CClass c3)	Adds visual flashing effects for up to three objects.
CPoint	addPt2(int n)	Adds a point to the construction by its index.
void	addPt2Line(int p1, int p2, int p3)	Adds a point to a line in the construction.
void	addPtEnlargeFlash(CPoint pt)	Adds a flash effect to enlarge a point.
boolean	animateDiagramFromString(java.lang.String s)	Animates a diagram from the given string.
void	autoConstruct(GTerm g)	Automatically constructs the diagram from the given geometric term.
void	cleardText()	Clears the construction text.
JAngleFlash	find_angFlash(CPoint a, CPoint b, CPoint c, CPoint d)	Finds and returns a JAngleFlash from the flash list that matches the given four points.
Param	findConstantParam(java.lang.String name)	Finds a constant parameter by its name.
void	finishConstruction()	Finishes the construction process.
void	flashassert(wprover.MAssertion ass)	Renders visual flashing effects for a given assertion.
void	flashattr(CClass cc, javax.swing.JPanel panel)	Adds a flash effect for a geometric class.
void	flashCond(Cond co, boolean fb)	Renders visual flashing effects for a given condition.
void	flashcons(Cons c)	Renders visual flashing effects for a given construction.
void	flashmnode(wprover.MNode n)	Renders visual flashing effects for a given node.
void	flashmobj(wprover.MObject obj)	Renders visual flashing effects for a given object.
void	flashmobj(wprover.MObject obj, boolean clear)	Renders visual flashing effects for a given object.
JFlash	getAngleFlash(javax.swing.JPanel panel, int p1, int p2, int p3, int p4)	Retrieves an angle flash effect for two lines intersecting at a point.
JFlash	getAngleFlashLL(javax.swing.JPanel panel, int p, LLine l1, LLine l2)	Retrieves an angle flash effect for two lines intersecting at a point.
JFlash	getAreaFlash(wprover.MDrObj d)	Retrieves an area flash effect for a given drawing object.
int	getAreaFlashNumber()	Retrieves the number of area flash effects.
JFlash	getCond(Cond co, boolean fb)	Retrieves a flash effect for a given condition.
JFlash	getDrobjFlash(wprover.MDrObj d)	Retrieves a flash effect for a given drawing object.
JFlash	getFlashCond(javax.swing.JPanel panel, Cond co)	Retrieves a flash effect for a given condition.
JFlash	getFlashCond(javax.swing.JPanel panel, Cond co, boolean fb)	Retrieves a flash effect for a given condition.
JFlash	getMAngleFlash(javax.swing.JPanel panel, CPoint p1, CPoint p2, CPoint p3, CPoint p4, int t)	Retrieves a modified angle flash effect for two lines intersecting at a point.
CPoint	getPtN(Cons c, int n)	Retrieves a point from a condition by its index.
boolean	inConstruction()	Checks if the construction process is currently active.
boolean	isConsFinished()	Checks if the construction process is finished.
boolean	isFreePoint(int n)	Checks if a point is free.
CPoint	lcmeet(Circle c, CLine ln)	Finds the intersection point between a circle and a line.
CPoint	lcmeet(Circle c, CLine ln, CPoint p1)	Finds the intersection point between a circle and a line, excluding a specific point.
void	mouseDown(double x, double y)	Handles mouse down events at the specified coordinates.
void	mouseDown(double x, double y, boolean cc)	Handles mouse down events at the specified coordinates with an option to clear constraints.
void	pointAdded(Cons pt, int type, int[] pp, boolean cc, int index, double x, double y, CPoint cp, java.lang.Object[] pss)	Processes the provided construction point and applies the appropriate geometric constraints and operations based on its type.
void	setConstructLines(GTerm g)	Sets the construction lines for the given geometric term.
void	setPointAttrAsConstructed(CPoint pt)	Sets the attributes of a point as constructed.
void	writePointPosition(java.io.FileOutputStream out)	Writes the positions of points to the given output stream.

Methods inherited from class wprover.DrawProcess

actionPerformed, add_free_transform, add_line, add_PFOOT, add_rcircle, add_sp_angle_value, addADecidedPointWithUnite, addALine, addAngleToList, addCalculationCircle, addCalculationPolygon, addCalculationPX, addCalculationPY, addCgFlash, addCircleToList, addConstraintToList, addCr, addCTMark, addCTMark, addDiagramUpdaterListener, addedMark, addedMark, addFlash, addFlash1, addFlash2, addFlashPolygon, addFlashx, addisoAngle, addLineSlope, addLineToList, addNodeToUndoList, addObjectToList, addOrientedSegment, AddPointToCircle, AddPointToLine, AddPointToLine, AddPointToLineX, addPointToList, addPolygonToList, addSelectPoint, addsquare, addText, addToSelectList, addZeron, all_flash_finished, already_redo, animationOntime, animationStart, animationStop, autoAnimate, autoShowstep, autoUndoRedo, BackupParameter, calcu_m1, calculate, calculate_a_point, calculate_allpt, calculate_allResults, calculate_lccc, calculate_ocir, calculate_oline, calculate_text, calculate_trace, calform, calv_parameter, canAutoAnimate, cancelCurrentAction, CatchAngle, CatchList, charsetAndAddPoly, check_animation, CheckCommonPoint, checkCPfieldExists, clearAll, clearAllConstraint, clearConstruction, clearFlash, clearSelection, CreateANewPoint, CreateANewPoint, defineSpecificAngle, dialog_addText, doFlash, drawAuxLine, drawCurrentAct, drawFlash, drawLineAndAdd, drawSmartPVLine, drawTrackpt, DWButtonDown, DWButtonUp, DWMouseDbClick, DWMouseDrag, DWMouseMove, DWMouseRightClick, DWMouseRightDown, DWMouseWheel, eraseAPoly, ErasedADecidedPoint, fd_angle, fd_angle_4p, fd_angle_m, fd_circle, fd_circle, fd_circleOR, fd_edmark, fd_point, fd_polygon, fd_pt_on_which_circle, fd_pt_on_which_line, fd_rcircle, findPolygon, findPolygon1, flash_node_by_id, flashStep, get_Catch_Intersection, getActionType, getAllConstraint, getAllSolidObj, getANewParam, getAngleByid, getAngleSimpleName, getAnimateC, getCircleByid, getCommonPoint, getConstraintByid, getConstructionFromDraw, GetCurrentAction, getFile, GetFraction, getLastConstructedPoint, getLineByid, getName, getNDGS, getObjectFlash, getObjectInListById, getOjbectById, getParaForSpecificAngle, getParameter, getParameterByindex, getPBList, getPBMono, getPointById, getPointNameByCount, getPolyList, getRedolistSize, getSelectList, getSmartPV, getSnap, getSpecificAngleList, getStatus, getTextLocation, getTraceById, getTraceByPt, getUndoById, getUndolistSize, gterm, isDrawGrid, isFlashFinished, isitSaved, isPointAlreadyExists, isRedoAtEnd, isSnap, Load_global, LoadGGB2, MeetCCToDefineAPoint, MeetDefineAPoint, MeetDefineAPoint, MeetLCToDefineAPoint, meetTwoObject, moveCatch, moveUndoObjectFromList, mulSolutionSelect, need_save, nextProveStep, objectsListMoved, OnCatch, onDBClick, openOutputFile, optmizePolynomial, paintPoint, PolygonTransPointsCreated, popLeadingVariableDialog, popSelect, print, PrintContent, printNDGS, prove_run_to_end, provePlay, proveStop, pushbackup, re_generate_all_poly, recal_allFlash, reCalculate, redo, redo_step, redo_step, redo_step, reduce, removeConstraintFromList, RemoveDiagramUpdaterListener, repaint, resetAux, resetUndo, RightMenuPopup, roundn, run_to_prove, runto, runto1, Save_global, SelectACircle, SelectALine, SelectAllFromXY, SelectAPoint, SelectAPolygon, SelectByRect, SelectFromAList, SelectFromAList, SelectNameText, SelectOneFromXY, selectUndoObjectFromList, setCalMode0, setCalMode1, SetCurrentAction, setCurrentDrawPanel, setCurrentInstance, setcurrentStatus, SetDimension, setFile, setFirstPnt, SetGrid, setMeshStep, setName, setObjectListForFlash, setObjectListForFlash, setObjectListForFlash, setParameter, setParameter, setParameterValue, setRecal, setSavedTag, setSmartPVLine, SetSnap, setStatus, setTimerDelay, setTransformStatus, setUndoListForFlash, setUndoListForFlash1, setUndoStructForDisPlay, SetVarable, Smart, SmartAddPoint, SmartAddPoint, SmartgetApointFromXY, SmartgetApointFromXY, SmartmoveCatch, SmartmoveCatch, SmartmoveCatchLine, SmartmoveCatchPt, SmartPCircle, SmartPLine, SmartPoint, SmartPointOnLine, smartPVDragLine, startFlash, startTrackPt, stateChange, stopTrack, stopUndoFlash, translate_back, Undo, undo_step, undo_step, Undo_step, Undo_stepPure, UndoAdded, UndoAdded, UndoAdded, UndoAdded, UndoPure, updateFlashDelay, viewElement, viewElementFromXY

Methods inherited from class wprover.DrawBase

addCircle, addLine, check_cc_inter, check_lc_inter, check_same_side, check_triangle_inside, collv, containFreezedPoint, CreateATempPoint, decide_wu_identical, div_set, drawCatch, drawCatchInterCross, drawCatchObjName, drawCatchRect, drawcircle2p, drawCross, drawGrid, drawList, drawPerpFoot, drawpoint, drawPointNameLocation, drawPointOrCross, drawRect, drawSelect, drawTipRect, drawTipSquare, drawTipTirangle, drawTTFoot, fd_circle, fd_line, find_tmark, findCTMark, findPoint, getBounds, getCatchHVPoint, getPointList, getPoints, getPointSize, getPoolA, getPooln, getTMono, hvCatchPoint, intersect_cc, intersect_ll, isFrozen, isLineDrawn, isZero, near, printPoly, removeFromeListLastNElements, setAntiAlias, setCatchHVPoint, setCurrentDrawEnvironment, setLanguage, setMouseInside, signArea, unfreezeAllPoints, zoom_in, zoom_out

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Constructor Detail

DrawTextProcess

public DrawTextProcess()

Method Detail

inConstruction

public boolean inConstruction()

Checks if the construction process is currently active.

Returns:

true if the construction process is active, false otherwise

isConsFinished

public boolean isConsFinished()

Checks if the construction process is finished.

Returns:

true if the construction process is finished, false otherwise

setConstructLines

public void setConstructLines(GTerm g)

Sets the construction lines for the given geometric term.

Parameters:

g - the geometric term

cleardText

public void cleardText()

Clears the construction text.

animateDiagramFromString

public boolean animateDiagramFromString(java.lang.String s)

Animates a diagram from the given string.

Parameters:

s - the string representing the animation

Returns:

true if the animation was successfully loaded, false otherwise

autoConstruct

public void autoConstruct(GTerm g)

Automatically constructs the diagram from the given geometric term.

Parameters:

g - the geometric term

writePointPosition

public void writePointPosition(java.io.FileOutputStream out)
                        throws java.io.IOException

Writes the positions of points to the given output stream.

Parameters:

out - the output stream to write to

Throws:

java.io.IOException - if an I/O error occurs

addAuxPoint

public void addAuxPoint(AuxPt ax)

Adds an auxiliary point to the construction.

Parameters:

ax - the auxiliary point to add

setPointAttrAsConstructed

public void setPointAttrAsConstructed(CPoint pt)

Sets the attributes of a point as constructed.

Parameters:

pt - the point to set attributes for

addFreePt

public boolean addFreePt(Cons c)

Adds a free point to the construction.

Parameters:

c - the construction object

Returns:

true if a free point was added, false otherwise

addGTPt

public boolean addGTPt(Cons c)

Adds a geometric term point to the construction.

Parameters:

c - the construction object

Returns:

true if a geometric term point was added, false otherwise

addPt2

public CPoint addPt2(int n)

Adds a point to the construction by its index.

Parameters:

n - the index of the point

Returns:

the added point

addPt2Line

public void addPt2Line(int p1,
                       int p2,
                       int p3)

Adds a point to a line in the construction.

Parameters:

p1 - the index of the point to add

p2 - the index of the first point of the line

p3 - the index of the second point of the line

mouseDown

public void mouseDown(double x,
                      double y)

Handles mouse down events at the specified coordinates.

Parameters:

x - the x-coordinate

y - the y-coordinate

mouseDown

public void mouseDown(double x,
                      double y,
                      boolean cc)

Handles mouse down events at the specified coordinates with an option to clear constraints.

Parameters:

x - the x-coordinate

y - the y-coordinate

cc - a flag indicating whether to clear constraints

pointAdded

public void pointAdded(Cons pt,
                       int type,
                       int[] pp,
                       boolean cc,
                       int index,
                       double x,
                       double y,
                       CPoint cp,
                       java.lang.Object[] pss)

Processes the provided construction point and applies the appropriate geometric constraints and operations based on its type.

This method examines the type of the provided construction object and executes the corresponding logic to update the constraint and geometric element lists. Depending on the provided parameters, it adds points, lines, circles, angles, or other entities and registers constraints related to them.

Parameters:

pt - the construction object encapsulating geometric data and type information

type - the specific type of construction operation to execute

pp - an array of integers representing indices for points and other parameters

cc - a boolean flag indicating whether to perform specific additional operations

index - an identifier used for certain point creation methods

x - the x-coordinate value used for point creation if applicable

y - the y-coordinate value used for point creation if applicable

cp - a CPoint object that will be updated or used during the construction

pss - an array of additional parameters used for constructing constants or constraints

findConstantParam

public Param findConstantParam(java.lang.String name)

Finds a constant parameter by its name.

Parameters:

name - the name of the constant parameter

Returns:

the constant parameter, or null if not found

addObjectFlash

public void addObjectFlash(CClass c1,
                           CClass c2,
                           CClass c3)

Adds visual flashing effects for up to three objects.

Parameters:

c1 - the first object to flash

c2 - the second object to flash

c3 - the third object to flash

flashcons

public void flashcons(Cons c)

Renders visual flashing effects for a given construction.

Parameters:

c - the construction

finishConstruction

public void finishConstruction()

Finishes the construction process.

addConcLineOrCircle

public void addConcLineOrCircle(Cond cc)

Adds lines or circles based on the given condition.

Parameters:

cc - the condition

addAllLn

public void addAllLn(int[] pp)

Adds all lines based on the given points.

Parameters:

pp - the points

isFreePoint

public boolean isFreePoint(int n)

Checks if a point is free.

Parameters:

n - the index of the point

Returns:

true if the point is free, false otherwise

lcmeet

public CPoint lcmeet(Circle c,
                     CLine ln)

Finds the intersection point between a circle and a line.

Parameters:

c - the circle

ln - the line

Returns:

the intersection point, or null if no intersection

lcmeet

public CPoint lcmeet(Circle c,
                     CLine ln,
                     CPoint p1)

Finds the intersection point between a circle and a line, excluding a specific point.

Parameters:

c - the circle

ln - the line

p1 - the point to exclude from the search

Returns:

the intersection point, or null if no intersection

flashCond

public void flashCond(Cond co,
                      boolean fb)

Renders visual flashing effects for a given condition.

Parameters:

co - the condition

fb - a flag indicating whether to clear existing flash effects

getCond

public JFlash getCond(Cond co,
                      boolean fb)

Retrieves a flash effect for a given condition.

Parameters:

co - the condition

fb - a flag indicating whether to clear existing flash effects

Returns:

the flash effect

addCongFlash

public void addCongFlash(Cond co,
                         boolean cl)

Adds a congruence flash effect for a given condition.

Parameters:

co - the condition

cl - a flag indicating whether to clear existing flash effects

addAcongFlash

public void addAcongFlash(Cond co,
                          boolean cl)

Adds an angle congruence flash effect for a given condition.

Parameters:

co - the condition

cl - a flag indicating whether to clear existing flash effects

add_Line

public CLine add_Line(CPoint a,
                      CPoint b)

Adds a line between two points.

Parameters:

a - the first point

b - the second point

Returns:

the line, or null if the points are invalid

addLnWC

public CLine addLnWC(CPoint a,
                     CPoint b,
                     int color,
                     int d)

Adds a line with specific color and dash style between two points.

Parameters:

a - the first point

b - the second point

color - the color of the line

d - the dash style of the line

Returns:

the line

getPtN

public CPoint getPtN(Cons c,
                     int n)

Retrieves a point from a condition by its index.

Parameters:

c - the condition

n - the index of the point

Returns:

the point, or null if not found

addCondAux

public java.util.Vector addCondAux(Cons co,
                                   boolean aux)

Adds auxiliary conditions for a given condition.

Parameters:

co - the condition

aux - a flag indicating whether to add auxiliary conditions

Returns:

a vector of added lines

getFlashCond

public JFlash getFlashCond(javax.swing.JPanel panel,
                           Cond co,
                           boolean fb)

Retrieves a flash effect for a given condition.

Parameters:

panel - the panel to display the flash effect

co - the condition

fb - a flag indicating whether to clear existing flash effects

Returns:

the flash effect

getFlashCond

public JFlash getFlashCond(javax.swing.JPanel panel,
                           Cond co)

Retrieves a flash effect for a given condition.

Parameters:

panel - the panel to display the flash effect

co - the condition

Returns:

the flash effect

getAngleFlash

public JFlash getAngleFlash(javax.swing.JPanel panel,
                            int p1,
                            int p2,
                            int p3,
                            int p4)

Retrieves an angle flash effect for two lines intersecting at a point.

Parameters:

panel - the panel to display the flash effect

p1 - the first point of the first line

p2 - the second point of the first line

p3 - the first point of the second line

p4 - the second point of the second line

Returns:

the angle flash effect

getMAngleFlash

public JFlash getMAngleFlash(javax.swing.JPanel panel,
                             CPoint p1,
                             CPoint p2,
                             CPoint p3,
                             CPoint p4,
                             int t)

Retrieves a modified angle flash effect for two lines intersecting at a point.

Parameters:

panel - the panel to display the flash effect

p1 - the first point of the first line

p2 - the second point of the first line

p3 - the first point of the second line

p4 - the second point of the second line

t - the type of angle flash effect

Returns:

the modified angle flash effect

getAreaFlashNumber

public int getAreaFlashNumber()

Retrieves the number of area flash effects.

Returns:

the number of area flash effects

getAreaFlash

public JFlash getAreaFlash(wprover.MDrObj d)

Retrieves an area flash effect for a given drawing object.

Parameters:

d - the drawing object

Returns:

the area flash effect

getDrobjFlash

public JFlash getDrobjFlash(wprover.MDrObj d)

Retrieves a flash effect for a given drawing object.

Parameters:

d - the drawing object

Returns:

the flash effect

flashmnode

public void flashmnode(wprover.MNode n)

Renders visual flashing effects for a given node.

Parameters:

n - the node

flashmobj

public void flashmobj(wprover.MObject obj)

Renders visual flashing effects for a given object.

Parameters:

obj - the object

flashmobj

public void flashmobj(wprover.MObject obj,
                      boolean clear)

Renders visual flashing effects for a given object.

Parameters:

obj - the object

clear - whether to clear existing flash effects

addlineFlash

public void addlineFlash(CPoint p1,
                         CPoint p2)

Adds a flash effect for a line.

Parameters:

p1 - the first point of the line

p2 - the second point of the line

addInfinitelineFlash

public void addInfinitelineFlash(CPoint p1,
                                 CPoint p2)

Adds a flash effect for an infinite line.

Parameters:

p1 - the first point of the line

p2 - the second point of the line

flashassert

public void flashassert(wprover.MAssertion ass)

Renders visual flashing effects for a given assertion.

This method examines the type of the provided MAssertion and displays the corresponding flash pattern based on the assertion type. It supports various assertion types such as collinearity, parallelism, equality of distances, perpendicularity, cyclic configurations, angle equality, midpoint conditions, congruency, triangle properties, and several others.

Parameters:

ass - the geometric assertion to be processed and flashed; may be null

addPtEnlargeFlash

public void addPtEnlargeFlash(CPoint pt)

Adds a flash effect to enlarge a point.

Parameters:

pt - the point to enlarge

addCGFlash

public void addCGFlash(CPoint p1,
                       CPoint p2,
                       CPoint p3,
                       CPoint p4)

Adds a flash effect for congruent segments.

Parameters:

p1 - the first point of the first segment

p2 - the second point of the first segment

p3 - the first point of the second segment

p4 - the second point of the second segment

addAreaFlash1

public void addAreaFlash1(wprover.MAssertion ass)

Adds a flash effect for an area based on an assertion.

Parameters:

ass - the assertion containing the area information

addAreaFlash

public void addAreaFlash(wprover.MAssertion ass)

Adds a flash effect for an area based on an assertion.

Parameters:

ass - the assertion containing the area information

getAngleFlashLL

public JFlash getAngleFlashLL(javax.swing.JPanel panel,
                              int p,
                              LLine l1,
                              LLine l2)

Retrieves an angle flash effect for two lines intersecting at a point.

Parameters:

panel - the panel to display the flash effect

p - the intersection point

l1 - the first line

l2 - the second line

Returns:

the angle flash effect

flashattr

public void flashattr(CClass cc,
                      javax.swing.JPanel panel)

Adds a flash effect for a geometric class.

Parameters:

cc - the geometric class

panel - the panel to display the flash effect

find_angFlash

public JAngleFlash find_angFlash(CPoint a,
                                 CPoint b,
                                 CPoint c,
                                 CPoint d)

Finds and returns a JAngleFlash from the flash list that matches the given four points.

Parameters:

a - the first point

b - the second point

c - the third point

d - the fourth point

Returns:

the matching JAngleFlash if found; otherwise, null

addFlashXtermAngle

public JFlash addFlashXtermAngle(XTerm x)

Creates or retrieves a flash angle based on an XTerm object. The flash is added to the flash list and its color is adjusted based on the PV value.

Parameters:

x - the XTerm object containing variable and point indices information

Returns:

the created or restarted flash; null if the XTerm, its variable, or any required point is not found

addFlashAngle

public JFlash addFlashAngle(int a,
                            int b,
                            int c,
                            int d)

Creates or retrieves a flash angle based on the given point indices. The flash is added to the flash list and the panel is repainted.

Parameters:

a - the index of the first point

b - the index of the second point

c - the index of the third point

d - the index of the fourth point

Returns:

the created or restarted flash; null if any of the points is not found

addaux

public void addaux(CProveText cpt)

Processes auxiliary proof text to add the corresponding flashes, marks, or polygons.

Parameters:

cpt - the CProveText object containing condition and proof information

addAngleToList2

public void addAngleToList2(CAngle ag)

Adds a CAngle to the angle list. If an angle with similar intersection is already present, the radius is adjusted before adding.

Parameters:

ag - the CAngle object to be added