# HG changeset patch
# User wenzelm
# Date 1368384377 -7200
# Node ID fab4ab92e8125b27104bd4ef9deb7e23b83fc953
# Parent  13fb5e4f2893ba8f7379ea36889337616e673638
more standard Isabelle/ML operations -- avoid inaccurate Bool.fromString;

diff -r 13fb5e4f2893 -r fab4ab92e812 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Sun May 12 20:30:34 2013 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Sun May 12 20:46:17 2013 +0200
@@ -733,7 +733,7 @@
           val metis_ft = AList.defined (op =) args metis_ftK
           val trivial =
             if AList.lookup (op =) args check_trivialK |> the_default trivial_default
-                            |> Bool.fromString |> the then
+                            |> Markup.parse_bool then
               Try0.try0 (SOME try_timeout) ([], [], [], []) pre
               handle TimeLimit.TimeOut => false
             else false
diff -r 13fb5e4f2893 -r fab4ab92e812 src/HOL/Tools/Metis/metis_reconstruct.ML
--- a/src/HOL/Tools/Metis/metis_reconstruct.ML	Sun May 12 20:30:34 2013 +0200
+++ b/src/HOL/Tools/Metis/metis_reconstruct.ML	Sun May 12 20:46:17 2013 +0200
@@ -324,7 +324,7 @@
       val m_tm = Metis_Term.Fn atom
       val [i_atom, i_tm] =
         hol_terms_from_metis ctxt type_enc concealed sym_tab [m_tm, fr]
-      val _ = trace_msg ctxt (fn () => "sign of the literal: " ^ Bool.toString pos)
+      val _ = trace_msg ctxt (fn () => "sign of the literal: " ^ Markup.print_bool pos)
       fun replace_item_list lx 0 (_::ls) = lx::ls
         | replace_item_list lx i (l::ls) = l :: replace_item_list lx (i-1) ls
       fun path_finder_fail tm ps t =
diff -r 13fb5e4f2893 -r fab4ab92e812 src/Pure/PIDE/markup.ML
--- a/src/Pure/PIDE/markup.ML	Sun May 12 20:30:34 2013 +0200
+++ b/src/Pure/PIDE/markup.ML	Sun May 12 20:46:17 2013 +0200
@@ -6,6 +6,8 @@
 
 signature MARKUP =
 sig
+  val parse_bool: string -> bool
+  val print_bool: bool -> string
   val parse_int: string -> int
   val print_int: int -> string
   type T = string * Properties.T
@@ -159,6 +161,15 @@
 
 (** markup elements **)
 
+(* booleans *)
+
+fun parse_bool "true" = true
+  | parse_bool "false" = false
+  | parse_bool s = raise Fail ("Bad boolean: " ^ quote s);
+
+val print_bool = Bool.toString;
+
+
 (* integers *)
 
 fun parse_int s =
diff -r 13fb5e4f2893 -r fab4ab92e812 src/Pure/System/options.ML
--- a/src/Pure/System/options.ML	Sun May 12 20:30:34 2013 +0200
+++ b/src/Pure/System/options.ML	Sun May 12 20:46:17 2013 +0200
@@ -96,13 +96,13 @@
 
 (* internal lookup and update *)
 
-val bool = get boolT Bool.fromString;
-val int = get intT Int.fromString;
+val bool = get boolT (try Markup.parse_bool);
+val int = get intT (try Markup.parse_int);
 val real = get realT Real.fromString;
 val string = get stringT SOME;
 
-val put_bool = put boolT Bool.toString;
-val put_int = put intT signed_string_of_int;
+val put_bool = put boolT Markup.print_bool;
+val put_int = put intT Markup.print_int;
 val put_real = put realT signed_string_of_real;
 val put_string = put stringT I;