# HG changeset patch
# User wenzelm
# Date 1333053830 -7200
# Node ID 15ede9f1da3f6e71195fcae5135bd38aa2fb69be
# Parent  6012241abe938be5d4403072346e9914e4b1b931
more specific notion of partiality (cf. Scala version);

diff -r 6012241abe93 -r 15ede9f1da3f src/Pure/PIDE/xml.ML
--- a/src/Pure/PIDE/xml.ML	Thu Mar 29 14:47:31 2012 +0200
+++ b/src/Pure/PIDE/xml.ML	Thu Mar 29 22:43:50 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;