# 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;