tuned messages;
authorwenzelm
Sat, 27 Feb 2016 16:37:06 +0100
changeset 62432 183c319b26dc
parent 62431 fbccea37091d
child 62433 2436a02f28c4
tuned messages;
src/Pure/System/getopts.scala
--- a/src/Pure/System/getopts.scala	Sat Feb 27 16:19:02 2016 +0100
+++ b/src/Pure/System/getopts.scala	Sat Feb 27 16:37:06 2016 +0100
@@ -37,6 +37,7 @@
   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 getopts(args: List[List[Char]]): List[List[Char]] =
     args match {
@@ -50,10 +51,10 @@
       case List('-', opt) :: opt_arg :: rest_args if is_option1(opt) =>
         option(opt, opt_arg); getopts(rest_args)
       case List(List('-', opt)) if is_option1(opt) =>
-        Output.error_message("Command-line option " + quote(opt.toString) + " requires an argument")
+        Output.error_message("Command-line option " + print_option(opt) + " requires an argument")
         usage()
       case ('-' :: opt :: _) :: _ if !is_option(opt) =>
-        Output.error_message("Illegal command-line option " + quote(opt.toString))
+        if (opt != '?') Output.error_message("Illegal command-line option " + print_option(opt))
         usage()
       case _ => args
   }