private static String generateOptionNameFromDocument(Type type, String document)
				throws SleighException {
			int startPos, endPos;
			String tagAttribute;
			switch (type) {
				case PROTOTYPE_MODEL:
				case MERGE_MODEL:
				case CALL_FIXUP:
					tagAttribute = "name=\"";
					break;
				case CALLOTHER_FIXUP:
					tagAttribute = "targetop=\"";
					break;
				default:
					throw new SleighException("Unsupported extension type");
			}
			startPos = document.indexOf(tagAttribute, 0);
			if (startPos < 0) {
				throw new SleighException("Could not find attribute: " + tagAttribute);
			}
			startPos += tagAttribute.length();
			endPos = document.indexOf('\"', startPos);
			if (endPos < 0) {
				throw new SleighException("Bad XML document");
			}
			String formalName = document.substring(startPos, endPos);
			if (!isValidFormalName(formalName)) {
				throw new SleighException("Name of extension uses invalid characters");
			}
			return type.getOptionName(formalName);
		}
Helper class for collecting information about an extension XML document
and constructing its option name for storage
Ghidra/Framework/SoftwareModeling/src/main/java/ghidra/program/database/SpecExtension.java