changeset 31330 | 7bfbd0e07a40 |
parent 30672 | beaadd5af500 |
child 31473 | fd341ca4b8de |
--- a/src/Pure/General/secure.ML Mon Jun 01 23:28:02 2009 +0200 +++ b/src/Pure/General/secure.ML Mon Jun 01 23:28:04 2009 +0200 @@ -9,6 +9,7 @@ val set_secure: unit -> unit val is_secure: unit -> bool val deny_secure: string -> unit + val secure_mltext: unit -> unit val use_text: use_context -> int * string -> bool -> string -> unit val use_file: use_context -> bool -> string -> unit val toplevel_pp: string list -> string -> unit