public class TXRDoc : TXRObject {
public int doc_field;
public override void copy (TXRObject copy) {
stdout.printf ("TXRDoc:copy() called\n");
if (copy is TXRObject) {
base.copy (copy);
((TXRDoc)copy).doc_field = this.doc_field;
}