private void addOneSourceTokenToTLA(String str,Region region){
  if (region == null) {
    addOneTokenToTLA(str);
    return;
  }
  int beginCol=tlacodeNextLine.length();
  int endCol=beginCol + str.length();
  mappingVectorNextLine.addElement(new MappingObject.SourceToken(beginCol,endCol,region));
  tlacodeNextLine=tlacodeNextLine + str;
}

private void addOneSourceTokenToTLA ( String str , Region region ) { if ( region == null ) { addOneTokenToTLA ( str ) ; return ; } int beginCol = tlacodeNextLine . length ( ) ; int endCol = beginCol + str . length ( ) ; mappingVectorNextLine . addElement ( new MappingObject . SourceToken ( beginCol , endCol , region ) ) ; tlacodeNextLine = tlacodeNextLine + str ; }
if region is non - null , then adds string str to the tla output as a sourcetoken object with that region . otherwise , it adds it as a tlatoken , with begin / endtlatoken objects .
