private void shiftMappingVectorTokensLeft(int lineNum,int startCol,int shift){
  boolean lastWasBeginTLAToken=false;
  int lastBeginTLATokCol=-777;
  Vector line=(Vector)mappingVector.elementAt(lineNum);
  for (int i=0; i < line.size(); i++) {
    MappingObject obj=(MappingObject)line.elementAt(i);
    if (obj.getType() == MappingObject.BEGIN_TLATOKEN) {
      MappingObject.BeginTLAToken tobj=(MappingObject.BeginTLAToken)obj;
      int col=tobj.getColumn();
      if (col >= startCol) {
        tobj.setColumn(col - shift);
      }
      lastWasBeginTLAToken=true;
      lastBeginTLATokCol=tobj.getColumn();
    }
 else {
      if (obj.getType() == MappingObject.END_TLATOKEN) {
        MappingObject.EndTLAToken tobj=(MappingObject.EndTLAToken)obj;
        int col=tobj.getColumn();
        if (col >= startCol) {
          tobj.setColumn(col - shift);
        }
        if (lastWasBeginTLAToken && tobj.getColumn() <= lastBeginTLATokCol) {
          PcalDebug.ReportBug("PcalTLAGen.shiftMappingVectorTokensLeft created a null TLA Token");
        }
      }
 else       if (obj.getType() == MappingObject.SOURCE_TOKEN) {
        MappingObject.SourceToken tobj=(MappingObject.SourceToken)obj;
        int col=tobj.getBeginColumn();
        if (col >= startCol) {
          tobj.setBeginColumn(col - shift);
        }
        col=tobj.getEndColumn();
        if (col >= startCol) {
          tobj.setEndColumn(col - shift);
        }
        lastWasBeginTLAToken=false;
      }
    }
  }
}

private void shiftMappingVectorTokensLeft ( int lineNum , int startCol , int shift ) { boolean lastWasBeginTLAToken = false ; int lastBeginTLATokCol = - 777 ; Vector line = ( Vector ) mappingVector . elementAt ( lineNum ) ; for ( int i = 0 ; i < line . size ( ) ; i ++ ) { MappingObject obj = ( MappingObject ) line . elementAt ( i ) ; if ( obj . getType ( ) == MappingObject . BEGIN_TLATOKEN ) { MappingObject . BeginTLAToken tobj = ( MappingObject . BeginTLAToken ) obj ; int col = tobj . getColumn ( ) ; if ( col >= startCol ) { tobj . setColumn ( col - shift ) ; } lastWasBeginTLAToken = true ; lastBeginTLATokCol = tobj . getColumn ( ) ; } else { if ( obj . getType ( ) == MappingObject . END_TLATOKEN ) { MappingObject . EndTLAToken tobj = ( MappingObject . EndTLAToken ) obj ; int col = tobj . getColumn ( ) ; if ( col >= startCol ) { tobj . setColumn ( col - shift ) ; } if ( lastWasBeginTLAToken && tobj . getColumn ( ) <= lastBeginTLATokCol ) { PcalDebug . ReportBug ( "PcalTLAGen.shiftMappingVectorTokensLeft created a null TLA Token" ) ; } } else if ( obj . getType ( ) == MappingObject . SOURCE_TOKEN ) { MappingObject . SourceToken tobj = ( MappingObject . SourceToken ) obj ; int col = tobj . getBeginColumn ( ) ; if ( col >= startCol ) { tobj . setBeginColumn ( col - shift ) ; } col = tobj . getEndColumn ( ) ; if ( col >= startCol ) { tobj . setEndColumn ( col - shift ) ; } lastWasBeginTLAToken = false ; } } } }
adjusts the objects in line linenum of mappingvector so all column numbers starting with startcol are decreased by ` shift ' . if any begin / endtlatoken pairs are changed to have a non - positive width , a bug is reported . note : it is assumed that there is no aliasing of mappingtokens in mappingvector . that is , other than in transient local variables , the only pointer to a mappingtoken in mappingvector is the single one in its line of mappingvector . i can ' t see how any aliasing of mappingtokens could arise . this method is called only by genlabeledstmts .
