--- 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 *)