# HG changeset patch
# User wenzelm
# Date 1333054344 -7200
# Node ID fbcb7024fc938468d5b7f65a09b152646dd3c7d6
# Parent  cfd8ff62eab1b2ca7fe90c5b08313dc5db2ec5e0# Parent  15ede9f1da3f6e71195fcae5135bd38aa2fb69be
merged

diff -r cfd8ff62eab1 -r fbcb7024fc93 src/Pure/PIDE/xml.ML
--- 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;