merged

--- a/src/Pure/PIDE/xml.ML	Thu Mar 29 21:13:48 2012 +0200
+++ b/src/Pure/PIDE/xml.ML	Thu Mar 29 22:52:24 2012 +0200
@@ -327,7 +327,8 @@
 fun option _ NONE = []
   | option f (SOME x) = [node (f x)];
 
-fun variant fs x = [tagged (the (get_index (fn f => try f x) fs))];
+fun variant fs x =
+  [tagged (the (get_index (fn f => SOME (f x) handle General.Match => NONE) fs))];
 
 end;