named "group_detected" and "user_detected" and show if Dev-Editor could
successfully convert a group or user ID into the corresponding name.
- Cleaned exec_beginedit() and exec_endedit()
- More proper encoding of HTML entities at some points (still needs work)