equal
deleted
inserted
replaced
315 } |
315 } |
316 |
316 |
317 protected Name.Table createTable(Options options) { |
317 protected Name.Table createTable(Options options) { |
318 boolean useUnsharedTable = options.isSet("useUnsharedTable"); |
318 boolean useUnsharedTable = options.isSet("useUnsharedTable"); |
319 if (useUnsharedTable) |
319 if (useUnsharedTable) |
320 return new UnsharedNameTable(this); |
320 return UnsharedNameTable.create(this); |
321 else |
321 else |
322 return new SharedNameTable(this); |
322 return SharedNameTable.create(this); |
323 } |
323 } |
324 |
324 |
325 public void dispose() { |
325 public void dispose() { |
326 table.dispose(); |
326 table.dispose(); |
327 } |
327 } |