# HG changeset patch
# User wenzelm
# Date 1216157786 -7200
# Node ID 0dcdf992711464d2b0d67fa6b4637e989f15a1c2
# Parent  f38c25d106a7d36ddb0bf080517eebdc3420814a
tuned;

diff -r f38c25d106a7 -r 0dcdf9927114 src/Pure/General/markup.ML
--- a/src/Pure/General/markup.ML	Tue Jul 15 22:37:58 2008 +0200
+++ b/src/Pure/General/markup.ML	Tue Jul 15 23:36:26 2008 +0200
@@ -69,8 +69,8 @@
   val hiliteN: string val hilite: T
   val unprocessedN: string val unprocessed: T
   val runningN: string val running: T
+  val failedN: string val failed: T
   val finishedN: string val finished: T
-  val failedN: string val failed: T
   val disposedN: string val disposed: T
   val default_output: T -> output * output
   val add_mode: string -> (T -> output * output) -> unit
@@ -203,8 +203,8 @@
 
 val (unprocessedN, unprocessed) = markup_elem "unprocessed";
 val (runningN, running) = markup_elem "running";
+val (failedN, failed) = markup_elem "failed";
 val (finishedN, finished) = markup_elem "finished";
-val (failedN, failed) = markup_elem "failed";
 val (disposedN, disposed) = markup_elem "disposed";