src/Pure/PIDE/markup.ML

 Isabelle-specific implementation of quasi-abstract markup elements.
 *)
 
 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
   val empty: T
   val is_empty: T -> bool

 structure Markup: MARKUP =
 struct
 
 (** 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 =
   let val i = Int.fromString s in
     if is_none i orelse String.isPrefix "~" s