public static void shiftMappingVector(Vector mvec,int shift){
  for (int i=0; i < mvec.size(); i++) {
    Vector line=(Vector)mvec.elementAt(i);
    for (int j=0; j < line.size(); j++) {
      MappingObject mobj=(MappingObject)line.elementAt(j);
      if (mobj.type == BEGIN_TLATOKEN) {
        BeginTLAToken obj=(BeginTLAToken)mobj;
        obj.setColumn(obj.getColumn() + shift);
      }
 else       if (mobj.type == END_TLATOKEN) {
        EndTLAToken obj=(EndTLAToken)mobj;
        obj.setColumn(obj.getColumn() + shift);
      }
 else       if (mobj.type == SOURCE_TOKEN) {
        SourceToken obj=(SourceToken)mobj;
        obj.setBeginColumn(obj.getBeginColumn() + shift);
        obj.setEndColumn(obj.getEndColumn() + shift);
      }
    }
  }
}

public static void shiftMappingVector ( Vector mvec , int shift ) { for ( int i = 0 ; i < mvec . size ( ) ; i ++ ) { Vector line = ( Vector ) mvec . elementAt ( i ) ; for ( int j = 0 ; j < line . size ( ) ; j ++ ) { MappingObject mobj = ( MappingObject ) line . elementAt ( j ) ; if ( mobj . type == BEGIN_TLATOKEN ) { BeginTLAToken obj = ( BeginTLAToken ) mobj ; obj . setColumn ( obj . getColumn ( ) + shift ) ; } else if ( mobj . type == END_TLATOKEN ) { EndTLAToken obj = ( EndTLAToken ) mobj ; obj . setColumn ( obj . getColumn ( ) + shift ) ; } else if ( mobj . type == SOURCE_TOKEN ) { SourceToken obj = ( SourceToken ) mobj ; obj . setBeginColumn ( obj . getBeginColumn ( ) + shift ) ; obj . setEndColumn ( obj . getEndColumn ( ) + shift ) ; } } } }
a mapping vector is a vector of vectors of mappingobject objects . this transforms a mapping vector obtained from a tlaexpr object by a call of tomappingvector to produce the mapping vector that would have resulted from that call if the entire expression had been moved to the right by ` shift ' characters .
