# HG changeset patch
# User wenzelm
# Date 1456588296 -3600
# Node ID 4630b1748cb3362a8170959e86a89ee40e521b99
# Parent  2436a02f28c40d325d908fdd5f9480b29593875b
tuned messages;

diff -r 2436a02f28c4 -r 4630b1748cb3 src/Pure/System/getopts.scala
--- a/src/Pure/System/getopts.scala	Sat Feb 27 16:37:47 2016 +0100
+++ b/src/Pure/System/getopts.scala	Sat Feb 27 16:51:36 2016 +0100
@@ -36,8 +36,13 @@
   private def is_option(opt: Char): Boolean = options.isDefinedAt(opt)
   private def is_option0(opt: Char): Boolean = is_option(opt) && !options(opt)._1
   private def is_option1(opt: Char): Boolean = is_option(opt) && options(opt)._1
-  private def option(opt: Char, opt_arg: List[Char]): Unit = options(opt)._2.apply(opt_arg.mkString)
   private def print_option(opt: Char): String = quote("-" + opt.toString)
+  private def option(opt: Char, opt_arg: List[Char]): Unit =
+    try { options(opt)._2.apply(opt_arg.mkString) }
+    catch {
+      case ERROR(msg) =>
+        cat_error(msg, "The error(s) above occurred in command-line option " + print_option(opt))
+    }
 
   private def getopts(args: List[List[Char]]): List[List[Char]] =
     args match {