# HG changeset patch
# User wenzelm
# Date 1368553711 -7200
# Node ID a9725750c53a733f063a8e0d88e2367d96644bd5
# Parent  7d8e0e3c553b308cf54fcefd3c8c98d0712bebdd
more uniform Markup.parse_real;

diff -r 7d8e0e3c553b -r a9725750c53a src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML	Tue May 14 19:30:21 2013 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML	Tue May 14 19:48:31 2013 +0200
@@ -7,7 +7,7 @@
 
 fun get args name default_value =
   case AList.lookup (op =) args name of
-    SOME value => the (Real.fromString value)
+    SOME value => Markup.parse_real value
   | NONE => default_value
 
 fun extract_relevance_fudge args
diff -r 7d8e0e3c553b -r a9725750c53a src/Pure/Isar/parse.ML
--- a/src/Pure/Isar/parse.ML	Tue May 14 19:30:21 2013 +0200
+++ b/src/Pure/Isar/parse.ML	Tue May 14 19:48:31 2013 +0200
@@ -212,7 +212,7 @@
 
 val nat = number >> (#1 o Library.read_int o Symbol.explode);
 val int = Scan.optional (minus >> K ~1) 1 -- nat >> op *;
-val real = float_number >> (the o Real.fromString) || int >> Real.fromInt;
+val real = float_number >> Markup.parse_real || int >> Real.fromInt;
 
 val tag_name = group (fn () => "tag name") (short_ident || string);
 val tags = Scan.repeat ($$$ "%" |-- !!! tag_name);
diff -r 7d8e0e3c553b -r a9725750c53a src/Pure/PIDE/markup.ML
--- a/src/Pure/PIDE/markup.ML	Tue May 14 19:30:21 2013 +0200
+++ b/src/Pure/PIDE/markup.ML	Tue May 14 19:48:31 2013 +0200
@@ -10,6 +10,8 @@
   val print_bool: bool -> string
   val parse_int: string -> int
   val print_int: int -> string
+  val parse_real: string -> real
+  val print_real: real -> string
   type T = string * Properties.T
   val empty: T
   val is_empty: T -> bool
@@ -161,7 +163,7 @@
 
 (** markup elements **)
 
-(* booleans *)
+(* misc values *)
 
 fun parse_bool "true" = true
   | parse_bool "false" = false
@@ -169,9 +171,6 @@
 
 val print_bool = Bool.toString;
 
-
-(* integers *)
-
 fun parse_int s =
   let val i = Int.fromString s in
     if is_none i orelse String.isPrefix "~" s
@@ -181,6 +180,13 @@
 
 val print_int = signed_string_of_int;
 
+fun parse_real s =
+  (case Real.fromString s of
+    SOME x => x
+  | NONE => raise Fail ("Bad real: " ^ quote s));
+
+val print_real = smart_string_of_real;
+
 
 (* basic markup *)
 
diff -r 7d8e0e3c553b -r a9725750c53a src/Pure/System/options.ML
--- a/src/Pure/System/options.ML	Tue May 14 19:30:21 2013 +0200
+++ b/src/Pure/System/options.ML	Tue May 14 19:48:31 2013 +0200
@@ -98,7 +98,7 @@
 
 val bool = get boolT (try Markup.parse_bool);
 val int = get intT (try Markup.parse_int);
-val real = get realT Real.fromString;
+val real = get realT (try Markup.parse_real);
 val string = get stringT SOME;
 
 val put_bool = put boolT Markup.print_bool;