private Vector stringToTLATokens(String token){
  Vector result=new Vector(3);
  String trimmedToken=token.trim();
  int numberOfLeftTrimmedTokens=(trimmedToken.length() == 0) ? -1 : token.indexOf(trimmedToken.charAt(0));
  if (numberOfLeftTrimmedTokens == -1) {
    numberOfLeftTrimmedTokens=0;
    trimmedToken=token;
  }
  int objBegin=numberOfLeftTrimmedTokens;
  result.addElement(new MappingObject.BeginTLAToken(objBegin));
  result.addElement(new MappingObject.EndTLAToken(objBegin + trimmedToken.length()));
  return result;
}

private Vector stringToTLATokens ( String token ) { Vector result = new Vector ( 3 ) ; String trimmedToken = token . trim ( ) ; int numberOfLeftTrimmedTokens = ( trimmedToken . length ( ) == 0 ) ? - 1 : token . indexOf ( trimmedToken . charAt ( 0 ) ) ; if ( numberOfLeftTrimmedTokens == - 1 ) { numberOfLeftTrimmedTokens = 0 ; trimmedToken = token ; } int objBegin = numberOfLeftTrimmedTokens ; result . addElement ( new MappingObject . BeginTLAToken ( objBegin ) ) ; result . addElement ( new MappingObject . EndTLAToken ( objBegin + trimmedToken . length ( ) ) ) ; return result ; }
returns the vector of mappingobjects containing the begintlatoken and endtlatoken that are put in the mappingvector by a call of addonelineoftla . the code was essentially copied from addonetokentotla .
