src/Pure/library.ML
changeset 22567 1565d476a9e2
parent 22369 a7263f330494
child 22582 f315da9400fb
equal deleted inserted replaced
22566:535ae9dd4c45 22567:1565d476a9e2
    44   exception SYS_ERROR of string
    44   exception SYS_ERROR of string
    45   val sys_error: string -> 'a
    45   val sys_error: string -> 'a
    46   exception ERROR of string
    46   exception ERROR of string
    47   val error: string -> 'a
    47   val error: string -> 'a
    48   val cat_error: string -> string -> 'a
    48   val cat_error: string -> string -> 'a
    49   val assert: bool -> string -> unit
       
    50   val deny: bool -> string -> unit
       
    51   val assert_all: ('a -> bool) -> 'a list -> ('a -> string) -> unit
    49   val assert_all: ('a -> bool) -> 'a list -> ('a -> string) -> unit
    52 
    50 
    53   (*pairs*)
    51   (*pairs*)
    54   val pair: 'a -> 'b -> 'a * 'b
    52   val pair: 'a -> 'b -> 'a * 'b
    55   val rpair: 'a -> 'b -> 'b * 'a
    53   val rpair: 'a -> 'b -> 'b * 'a
   325 fun error msg = raise ERROR msg;
   323 fun error msg = raise ERROR msg;
   326 
   324 
   327 fun cat_error "" msg = error msg
   325 fun cat_error "" msg = error msg
   328   | cat_error msg1 msg2 = error (msg1 ^ "\n" ^ msg2);
   326   | cat_error msg1 msg2 = error (msg1 ^ "\n" ^ msg2);
   329 
   327 
   330 fun assert p msg = if p then () else error msg;
       
   331 fun deny p msg = if p then error msg else ();
       
   332 
       
   333 fun assert_all pred list msg =
   328 fun assert_all pred list msg =
   334   let
   329   let
   335     fun ass [] = ()
   330     fun ass [] = ()
   336       | ass (x :: xs) = if pred x then ass xs else error (msg x);
   331       | ass (x :: xs) = if pred x then ass xs else error (msg x);
   337   in ass list end;
   332   in ass list end;