open_unsynchronized for interactive Isar loop;
authorwenzelm
Tue Sep 29 14:59:24 2009 +0200 (2009-09-29)
changeset 3273931e75ad9ae17
parent 32738 15bb09ca0378
child 32740 9dd0a2f83429
open_unsynchronized for interactive Isar loop;
src/Pure/General/secure.ML
src/Pure/System/isar.ML
     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 *)
     2.1 --- a/src/Pure/System/isar.ML	Tue Sep 29 11:49:22 2009 +0200
     2.2 +++ b/src/Pure/System/isar.ML	Tue Sep 29 14:59:24 2009 +0200
     2.3 @@ -139,6 +139,7 @@
     2.4  
     2.5  fun toplevel_loop {init = do_init, welcome, sync, secure} =
     2.6   (Context.set_thread_data NONE;
     2.7 +  Secure.open_unsynchronized ();
     2.8    if do_init then init () else ();
     2.9    if welcome then writeln (Session.welcome ()) else ();
    2.10    uninterruptible (fn _ => fn () => raw_loop secure (OuterSyntax.isar sync)) ());