- if (device_type != NULL)
- {
- struct string token = DS_INITIALIZER;
- size_t save_idx = 0;
-
- while (ds_tokenize (device_type, &token, " \t\r\v", &save_idx))
- {
- const char *type = ds_c_str (&token);
- if (!strcmp (type, "listing"))
- device |= OUTP_DEV_LISTING;
- else if (!strcmp (type, "screen"))
- device |= OUTP_DEV_SCREEN;
- else if (!strcmp (type, "printer"))
- device |= OUTP_DEV_PRINTER;
- else
- msg (IS, _("Unknown device type `%s'."), type);
- }
- ds_destroy (&token);
- }
+ while (ss_tokenize (device_type, ss_cstr (CC_SPACES), &save_idx, &token))
+ if (!ss_compare (token, ss_cstr ("listing")))
+ device |= OUTP_DEV_LISTING;
+ else if (!ss_compare (token, ss_cstr ("screen")))
+ device |= OUTP_DEV_SCREEN;
+ else if (!ss_compare (token, ss_cstr ("printer")))
+ device |= OUTP_DEV_PRINTER;
+ else
+ error (0, 0, _("unknown device type `%.*s'"),
+ (int) ss_length (token), ss_data (token));