changeset 29488 | 8fc3aeece219 |
parent 29482 | fe044b49e34f |
child 29522 | 793766d4c1b5 |
--- a/src/Pure/General/markup.scala Thu Jan 15 00:48:45 2009 +0100 +++ b/src/Pure/General/markup.scala Thu Jan 15 11:53:49 2009 +0100 @@ -117,7 +117,12 @@ val FAILED = "failed" val FINISHED = "finished" val DISPOSED = "disposed" - val COMMAND_STATE = "command_state" + + + /* interactive documents */ + + val EDITS = "edits" + val EDIT = "edit" /* messages */