src/Pure/PIDE/markup.ML
changeset 66379 6392766f3c25
parent 66066 7ac97dea27d2
child 66873 9953ae603a23
equal deleted inserted replaced
66378:53a6c5d4d03e 66379:6392766f3c25
   157   val forkedN: string val forked: T
   157   val forkedN: string val forked: T
   158   val joinedN: string val joined: T
   158   val joinedN: string val joined: T
   159   val runningN: string val running: T
   159   val runningN: string val running: T
   160   val finishedN: string val finished: T
   160   val finishedN: string val finished: T
   161   val failedN: string val failed: T
   161   val failedN: string val failed: T
       
   162   val consolidatedN: string val consolidated: T
   162   val exec_idN: string
   163   val exec_idN: string
   163   val initN: string
   164   val initN: string
   164   val statusN: string val status: T
   165   val statusN: string val status: T
   165   val resultN: string val result: T
   166   val resultN: string val result: T
   166   val writelnN: string val writeln: T
   167   val writelnN: string val writeln: T
   553 val (forkedN, forked) = markup_elem "forked";
   554 val (forkedN, forked) = markup_elem "forked";
   554 val (joinedN, joined) = markup_elem "joined";
   555 val (joinedN, joined) = markup_elem "joined";
   555 val (runningN, running) = markup_elem "running";
   556 val (runningN, running) = markup_elem "running";
   556 val (finishedN, finished) = markup_elem "finished";
   557 val (finishedN, finished) = markup_elem "finished";
   557 val (failedN, failed) = markup_elem "failed";
   558 val (failedN, failed) = markup_elem "failed";
       
   559 val (consolidatedN, consolidated) = markup_elem "consolidated";
   558 
   560 
   559 
   561 
   560 (* messages *)
   562 (* messages *)
   561 
   563 
   562 val exec_idN = "exec_id";
   564 val exec_idN = "exec_id";