private void addOneLineOfTLA(String line){
  if (tlacode.size() != mappingVector.size()) {
    PcalDebug.ReportBug("tlacode and mappingVector have different lengths");
  }
  endCurrentLineOfTLA();
  if (line.length() == 0) {
    mappingVector.addElement(new Vector(2));
    tlacode.addElement("");
    return;
  }
  addOneTokenToTLA(line);
  endCurrentLineOfTLA();
}

private void addOneLineOfTLA ( String line ) { if ( tlacode . size ( ) != mappingVector . size ( ) ) { PcalDebug . ReportBug ( "tlacode and mappingVector have different lengths" ) ; } endCurrentLineOfTLA ( ) ; if ( line . length ( ) == 0 ) { mappingVector . addElement ( new Vector ( 2 ) ) ; tlacode . addElement ( "" ) ; return ; } addOneTokenToTLA ( line ) ; endCurrentLineOfTLA ( ) ; }
adds a complete line of tla " code " that does not correspond to any pluscal code . adds begin / endtlatoken objects to the mapping iff the line does not equal " " .
