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