#371 Uneditable Text

[Mathias Ricken]

It could be useful to have regions of text that cannot be edited and that display in a slightly different way in DrJava, perhaps with a different background color. That way, an instructor could provide more structure and help in files handed out to students.

I'm not entirely sure what the best way to encode this in the .java files would be. Some special form of comment perhaps.