tuned;
authorwenzelm
Tue, 15 Jul 2008 23:36:26 +0200
changeset 27615 0dcdf9927114
parent 27614 f38c25d106a7
child 27616 a811269b577c
tuned;
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";