src/Pure/General/secure.ML
changeset 31330 7bfbd0e07a40
parent 30672 beaadd5af500
child 31473 fd341ca4b8de
equal deleted inserted replaced
31329:c8821a6297f9 31330:7bfbd0e07a40
     7 signature SECURE =
     7 signature SECURE =
     8 sig
     8 sig
     9   val set_secure: unit -> unit
     9   val set_secure: unit -> unit
    10   val is_secure: unit -> bool
    10   val is_secure: unit -> bool
    11   val deny_secure: string -> unit
    11   val deny_secure: string -> unit
       
    12   val secure_mltext: unit -> unit
    12   val use_text: use_context -> int * string -> bool -> string -> unit
    13   val use_text: use_context -> int * string -> bool -> string -> unit
    13   val use_file: use_context -> bool -> string -> unit
    14   val use_file: use_context -> bool -> string -> unit
    14   val toplevel_pp: string list -> string -> unit
    15   val toplevel_pp: string list -> string -> unit
    15   val commit: unit -> unit
    16   val commit: unit -> unit
    16   val system_out: string -> string * int
    17   val system_out: string -> string * int