# HG changeset patch # User wenzelm # Date 1232016829 -3600 # Node ID 8fc3aeece219be5bfe75d3a33c8c5bb21e6acec3 # Parent 06f4bb9fdb859fbf8aeeebb0fd08540122c67e33 replaced command_state by edits/edit; diff -r 06f4bb9fdb85 -r 8fc3aeece219 src/Pure/General/markup.ML --- a/src/Pure/General/markup.ML Thu Jan 15 00:48:45 2009 +0100 +++ b/src/Pure/General/markup.ML Thu Jan 15 11:53:49 2009 +0100 @@ -91,7 +91,8 @@ val failedN: string val failed: T val finishedN: string val finished: T val disposedN: string val disposed: T - val command_stateN: string val command_state: string -> string -> T + val editsN: string val edits: string -> T + val editN: string val edit: string -> string -> T val pidN: string val sessionN: string val classN: string @@ -269,8 +270,13 @@ val (finishedN, finished) = markup_elem "finished"; val (disposedN, disposed) = markup_elem "disposed"; -val command_stateN = "command_state"; -fun command_state id state_id : T = (command_stateN, [(idN, id), (stateN, state_id)]); + +(* interactive documents *) + +val (editsN, edits) = markup_string "edits" idN; + +val editN = "edit"; +fun edit id state_id : T = (editN, [(idN, id), (stateN, state_id)]); (* messages *) diff -r 06f4bb9fdb85 -r 8fc3aeece219 src/Pure/General/markup.scala --- 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 */