src/Pure/General/secure.ML
changeset 32739 31e75ad9ae17
parent 32738 15bb09ca0378
child 35010 d6e492cea6e4
     1.1 --- a/src/Pure/General/secure.ML	Tue Sep 29 11:49:22 2009 +0200
     1.2 +++ b/src/Pure/General/secure.ML	Tue Sep 29 14:59:24 2009 +0200
     1.3 @@ -13,6 +13,7 @@
     1.4    val use_text: use_context -> int * string -> bool -> string -> unit
     1.5    val use_file: use_context -> bool -> string -> unit
     1.6    val toplevel_pp: string list -> string -> unit
     1.7 +  val open_unsynchronized: unit -> unit
     1.8    val commit: unit -> unit
     1.9    val system_out: string -> string * int
    1.10    val system: string -> int
    1.11 @@ -47,8 +48,13 @@
    1.12  
    1.13  fun toplevel_pp path pp = (secure_mltext (); raw_toplevel_pp ML_Parse.global_context path pp);
    1.14  
    1.15 -(*commit is dynamically bound!*)
    1.16 -fun commit () = raw_use_text ML_Parse.global_context (0, "") false "commit();";
    1.17 +
    1.18 +(* global evaluation *)
    1.19 +
    1.20 +val use_global = raw_use_text ML_Parse.global_context (0, "") false;
    1.21 +
    1.22 +fun commit () = use_global "commit();";   (*commit is dynamically bound!*)
    1.23 +fun open_unsynchronized () = use_global "open Unsynchronized";
    1.24  
    1.25  
    1.26  (* shell commands *)