Interface Interner

public interface Interner

A placeholder type that translates into the type of the C++ class that implements an interning service for local names (@Local in Java).

Version:

$Id$