diff -r c272680df665 -r c54a53ef1873 src/Pure/General/value.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/value.ML	Mon Sep 05 23:11:00 2016 +0200
@@ -0,0 +1,57 @@
+(*  Title:      Pure/General/value.ML
+    Author:     Makarius
+
+Plain values, represented as string.
+*)
+
+signature VALUE =
+sig
+  val parse_bool: string -> bool
+  val print_bool: bool -> string
+  val parse_nat: string -> int
+  val parse_int: string -> int
+  val print_int: int -> string
+  val parse_real: string -> real
+  val print_real: real -> string
+end;
+
+structure Value: VALUE =
+struct
+
+fun parse_bool "true" = true
+  | parse_bool "false" = false
+  | parse_bool s = raise Fail ("Bad boolean " ^ quote s);
+
+val print_bool = Bool.toString;
+
+
+fun parse_nat s =
+  let val i = Int.fromString s in
+    if is_none i orelse the i < 0
+    then raise Fail ("Bad natural number " ^ quote s)
+    else the i
+  end;
+
+fun parse_int s =
+  let val i = Int.fromString s in
+    if is_none i orelse String.isPrefix "~" s
+    then raise Fail ("Bad integer " ^ quote s)
+    else the i
+  end;
+
+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));
+
+fun print_real x =
+  let val s = signed_string_of_real x in
+    (case space_explode "." s of
+      [a, b] => if forall_string (fn c => c = "0") b then a else s
+    | _ => s)
+  end;
+
+end;