--- 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
--- 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 =
--- 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 =
--- 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;