/*
* Node that has never been entered.
*
* Copyright 2000 Andy Gill
*
* $Revision: 1.1 $
* $Date: 2000/09/15 16:14:17 $
*/
import java.util.*;
/**
* @version 0.1
* @author Andy Gill
*/
public class CDSUnknown extends CDS {
public static CDSUnknown unknown = new CDSUnknown();
CDSUnknown() {
nodeId = -1;
}
public void addChild(CDS child,int portNo) {
Message.abort("Unknown node has no children");
}
protected void addEnterId(int enterId) {
Message.abort("Can't have entered something before this");
}
protected CDS adding(CDS newChild) {
return newChild.singleton();
}
public Pretty render(PrettyStep parent,int prec,boolean par) {
return Pretty.text(parent,unknownText,Pretty.UNEVAL);
}
public static String unknownText = "_";
public String toString() {
return unknownText;
}
}
|