| changeset 47199 | 15ede9f1da3f |
| parent 46840 | 42e32c777581 |
| child 48769 | e3b7087bb923 |
--- 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;