src/Pure/General/markup.ML
changeset 29488 8fc3aeece219
parent 29482 fe044b49e34f
child 29522 793766d4c1b5
equal deleted inserted replaced
29487:06f4bb9fdb85 29488:8fc3aeece219
    89   val unprocessedN: string val unprocessed: T
    89   val unprocessedN: string val unprocessed: T
    90   val runningN: string val running: string -> T
    90   val runningN: string val running: string -> T
    91   val failedN: string val failed: T
    91   val failedN: string val failed: T
    92   val finishedN: string val finished: T
    92   val finishedN: string val finished: T
    93   val disposedN: string val disposed: T
    93   val disposedN: string val disposed: T
    94   val command_stateN: string val command_state: string -> string -> T
    94   val editsN: string val edits: string -> T
       
    95   val editN: string val edit: string -> string -> T
    95   val pidN: string
    96   val pidN: string
    96   val sessionN: string
    97   val sessionN: string
    97   val classN: string
    98   val classN: string
    98   val messageN: string val message: string -> T
    99   val messageN: string val message: string -> T
    99   val promptN: string val prompt: T
   100   val promptN: string val prompt: T
   267 val (runningN, running) = markup_string "running" taskN;
   268 val (runningN, running) = markup_string "running" taskN;
   268 val (failedN, failed) = markup_elem "failed";
   269 val (failedN, failed) = markup_elem "failed";
   269 val (finishedN, finished) = markup_elem "finished";
   270 val (finishedN, finished) = markup_elem "finished";
   270 val (disposedN, disposed) = markup_elem "disposed";
   271 val (disposedN, disposed) = markup_elem "disposed";
   271 
   272 
   272 val command_stateN = "command_state";
   273 
   273 fun command_state id state_id : T = (command_stateN, [(idN, id), (stateN, state_id)]);
   274 (* interactive documents *)
       
   275 
       
   276 val (editsN, edits) = markup_string "edits" idN;
       
   277 
       
   278 val editN = "edit";
       
   279 fun edit id state_id : T = (editN, [(idN, id), (stateN, state_id)]);
   274 
   280 
   275 
   281 
   276 (* messages *)
   282 (* messages *)
   277 
   283 
   278 val pidN = "pid";
   284 val pidN = "pid";