forked from JavaTX/JavaCompilerCore
modified: ../../../main/java/de/dhbwstuttgart/syntaxtree/factory/UnifyTypeFactory.java
modified: ../../../main/java/de/dhbwstuttgart/typeinference/unify/model/PlaceholderType.java zurueck zum alten Zustand
This commit is contained in:
parent
755fd5c821
commit
58d757398d
@ -120,7 +120,7 @@ public class UnifyTypeFactory {
|
|||||||
}
|
}
|
||||||
|
|
||||||
public static UnifyType convert(TypePlaceholder tph){
|
public static UnifyType convert(TypePlaceholder tph){
|
||||||
PlaceholderType ntph = PlaceholderType.convertTypePlaceholder(tph.getName());//eingefuegt PL 2019-01-11 //new PlaceholderType(tph.getName());
|
PlaceholderType ntph = new PlaceholderType(tph.getName());
|
||||||
int in = PLACEHOLDERS.indexOf(ntph);
|
int in = PLACEHOLDERS.indexOf(ntph);
|
||||||
if (in == -1) {
|
if (in == -1) {
|
||||||
PLACEHOLDERS.add(ntph);
|
PLACEHOLDERS.add(ntph);
|
||||||
|
@ -23,7 +23,7 @@ public final class PlaceholderType extends UnifyType{
|
|||||||
* Static list containing the names of all existing placeholders.
|
* Static list containing the names of all existing placeholders.
|
||||||
* Used for generating fresh placeholders.
|
* Used for generating fresh placeholders.
|
||||||
*/
|
*/
|
||||||
public static final ArrayList<PlaceholderType> EXISTING_PLACEHOLDERS = new ArrayList<PlaceholderType>();
|
public static final ArrayList<String> EXISTING_PLACEHOLDERS = new ArrayList<String>();
|
||||||
|
|
||||||
/**
|
/**
|
||||||
* Prefix of auto-generated placeholder names.
|
* Prefix of auto-generated placeholder names.
|
||||||
@ -60,28 +60,17 @@ public final class PlaceholderType extends UnifyType{
|
|||||||
*/
|
*/
|
||||||
public PlaceholderType(String name) {
|
public PlaceholderType(String name) {
|
||||||
super(name, new TypeParams());
|
super(name, new TypeParams());
|
||||||
|
EXISTING_PLACEHOLDERS.add(name); // Add to list of existing placeholder names
|
||||||
IsGenerated = false; // This type is user generated
|
IsGenerated = false; // This type is user generated
|
||||||
}
|
}
|
||||||
|
|
||||||
public static PlaceholderType convertTypePlaceholder(String name) {//eingefuegt PL 2019-01-11
|
|
||||||
PlaceholderType newTph = new PlaceholderType(name);
|
|
||||||
int i = EXISTING_PLACEHOLDERS.indexOf(newTph);//equals vergleicht den Namen
|
|
||||||
if (i == -1) {
|
|
||||||
EXISTING_PLACEHOLDERS.add(newTph); // Add to list of existing placeholder names
|
|
||||||
return newTph;
|
|
||||||
}
|
|
||||||
else {
|
|
||||||
return EXISTING_PLACEHOLDERS.get(i);
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
/**
|
/**
|
||||||
* Creates a new placeholdertype
|
* Creates a new placeholdertype
|
||||||
* @param isGenerated true if this placeholder is auto-generated, false if it is user-generated.
|
* @param isGenerated true if this placeholder is auto-generated, false if it is user-generated.
|
||||||
*/
|
*/
|
||||||
protected PlaceholderType(String name, boolean isGenerated) {
|
protected PlaceholderType(String name, boolean isGenerated) {
|
||||||
super(name, new TypeParams());
|
super(name, new TypeParams());
|
||||||
EXISTING_PLACEHOLDERS.add(this); // Add to list of existing placeholder names
|
EXISTING_PLACEHOLDERS.add(name); // Add to list of existing placeholder names
|
||||||
IsGenerated = isGenerated;
|
IsGenerated = isGenerated;
|
||||||
}
|
}
|
||||||
|
|
||||||
|
Loading…
Reference in New Issue
Block a user