# HG changeset patch
# User wenzelm
# Date 1254229164 -7200
# Node ID 31e75ad9ae17c7b17db321757635802942c051cc
# Parent  15bb09ca0378b6f9bd23f69f8c8a7835786655fc
open_unsynchronized for interactive Isar loop;

diff -r 15bb09ca0378 -r 31e75ad9ae17 src/Pure/General/secure.ML
--- a/src/Pure/General/secure.ML	Tue Sep 29 11:49:22 2009 +0200
+++ b/src/Pure/General/secure.ML	Tue Sep 29 14:59:24 2009 +0200
@@ -13,6 +13,7 @@
   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
+  val open_unsynchronized: unit -> unit
   val commit: unit -> unit
   val system_out: string -> string * int
   val system: string -> int
@@ -47,8 +48,13 @@
 
 fun toplevel_pp path pp = (secure_mltext (); raw_toplevel_pp ML_Parse.global_context path pp);
 
-(*commit is dynamically bound!*)
-fun commit () = raw_use_text ML_Parse.global_context (0, "") false "commit();";
+
+(* global evaluation *)
+
+val use_global = raw_use_text ML_Parse.global_context (0, "") false;
+
+fun commit () = use_global "commit();";   (*commit is dynamically bound!*)
+fun open_unsynchronized () = use_global "open Unsynchronized";
 
 
 (* shell commands *)
diff -r 15bb09ca0378 -r 31e75ad9ae17 src/Pure/System/isar.ML
--- a/src/Pure/System/isar.ML	Tue Sep 29 11:49:22 2009 +0200
+++ b/src/Pure/System/isar.ML	Tue Sep 29 14:59:24 2009 +0200
@@ -139,6 +139,7 @@
 
 fun toplevel_loop {init = do_init, welcome, sync, secure} =
  (Context.set_thread_data NONE;
+  Secure.open_unsynchronized ();
   if do_init then init () else ();
   if welcome then writeln (Session.welcome ()) else ();
   uninterruptible (fn _ => fn () => raw_loop secure (OuterSyntax.isar sync)) ());