code: private Name makeOperatorName(String name) {
          Name opName = names.fromString(name);
          operatorNames.add(opName);
          return opName;
      }
docs: Create a new operator name from corresponding String representation
  and add the name to the set of known operator names.