de.uka.ilkd.key.gui.proofdiff

Class diff_match_patch.Diff

java.lang.Object

de.uka.ilkd.key.gui.proofdiff.diff_match_patch.Diff

Enclosing class:

diff_match_patch

public static class diff_match_patch.Diff
extends java.lang.Object

Class representing one diff operation.

Field Summary

Fields

Modifier and Type	Field and Description
diff_match_patch.Operation	operation One of: INSERT, DELETE or EQUAL.
java.lang.String	text The text associated with this diff operation.

Constructor Summary

Constructors

Constructor and Description
Diff(diff_match_patch.Operation operation, java.lang.String text) Constructor.

Method Summary

Modifier and Type	Method and Description
boolean	equals(java.lang.Object obj) Is this Diff equivalent to another Diff?
int	hashCode() Create a numeric hash value for a Diff.
java.lang.String	toString() Display a human-readable version of this Diff.

Methods inherited from class java.lang.Object

clone, finalize, getClass, notify, notifyAll, wait, wait, wait

Field Detail

operation

public diff_match_patch.Operation operation

One of: INSERT, DELETE or EQUAL.

text

public java.lang.String text

The text associated with this diff operation.

Constructor Detail

Diff

public Diff(diff_match_patch.Operation operation,
            java.lang.String text)

Constructor. Initializes the diff with the provided values.

Parameters:

operation - One of INSERT, DELETE or EQUAL.

text - The text being applied.

Method Detail

toString

public java.lang.String toString()

Display a human-readable version of this Diff.

Overrides:

toString in class java.lang.Object

Returns:

text version.

hashCode

public int hashCode()

Create a numeric hash value for a Diff. This function is not used by DMP.

Overrides:

hashCode in class java.lang.Object

Returns:

Hash value.

equals

public boolean equals(java.lang.Object obj)

Is this Diff equivalent to another Diff?

Overrides:

equals in class java.lang.Object

Parameters:

obj - Another Diff to compare against.

Returns:

true or false.