"staff", STAFF,
"start", START_T,
"table", TABLE,
+ "symboltables", SYMBOLTABLES,
+ "texid", TEXID,
"chord", CHORD,
"multi", MULTI,
"unitspace", UNITSPACE,
"voices", VOICES,
"width", WIDTH,
"music", MUSIC,
+ "grouping", GROUPING,
0,0
};
void
delete_identifiers()
-{
-
+{
for (Assoc_iter<String,Identifier*> ai(the_id_tab); ai.ok(); ai++) {
mtor << "deleting: " << ai.key()<<'\n';
delete ai.val();