# HG changeset patch
# User wenzelm
# Date 1456587467 -3600
# Node ID 2436a02f28c40d325d908fdd5f9480b29593875b
# Parent  183c319b26dc19fd3aab83c820971118332d6545
more operations (like Markup.parse_bool in ML);

diff -r 183c319b26dc -r 2436a02f28c4 src/Pure/General/properties.scala
--- a/src/Pure/General/properties.scala	Sat Feb 27 16:37:06 2016 +0100
+++ b/src/Pure/General/properties.scala	Sat Feb 27 16:37:47 2016 +0100
@@ -23,6 +23,8 @@
           case "false" => Some(false)
           case _ => None
         }
+      def parse(s: java.lang.String): scala.Boolean =
+        unapply(s) getOrElse error("Bad boolean: " + quote(s))
     }
 
     object Int
@@ -31,6 +33,8 @@
       def unapply(s: java.lang.String): Option[scala.Int] =
         try { Some(Integer.parseInt(s)) }
         catch { case _: NumberFormatException => None }
+      def parse(s: java.lang.String): scala.Int =
+        unapply(s) getOrElse error("Bad integer: " + quote(s))
     }
 
     object Long
@@ -39,6 +43,8 @@
       def unapply(s: java.lang.String): Option[scala.Long] =
         try { Some(java.lang.Long.parseLong(s)) }
         catch { case _: NumberFormatException => None }
+      def parse(s: java.lang.String): scala.Long =
+        unapply(s) getOrElse error("Bad integer: " + quote(s))
     }
 
     object Double
@@ -47,6 +53,8 @@
       def unapply(s: java.lang.String): Option[scala.Double] =
         try { Some(java.lang.Double.parseDouble(s)) }
         catch { case _: NumberFormatException => None }
+      def parse(s: java.lang.String): scala.Double =
+        unapply(s) getOrElse error("Bad real: " + quote(s))
     }
   }