src/Pure/General/secure.ML
changeset 25753 99c9fc5e11f2
parent 25703 832073e402ae
child 26080 d920e4c8ba82
equal deleted inserted replaced
25752:374446e93558 25753:99c9fc5e11f2
    26 
    26 
    27 fun set_secure () = secure := true;
    27 fun set_secure () = secure := true;
    28 fun is_secure () = ! secure;
    28 fun is_secure () = ! secure;
    29 
    29 
    30 fun deny_secure msg = if is_secure () then error msg else ();
    30 fun deny_secure msg = if is_secure () then error msg else ();
       
    31 
    31 
    32 
    32 
    33 
    33 (** critical operations **)
    34 (** critical operations **)
    34 
    35 
    35 (* ML evaluation *)
    36 (* ML evaluation *)