# HG changeset patch
# User wenzelm
# Date 1282911248 -7200
# Node ID 712cb964d1130b28723e5a7bafb10470d2d44410
# Parent  89f273ab1d4260c8ed15b35dbf0c696ae0f366c4
structure Unsynchronized is never opened and set/reset/toggle have been discontinued;
retain Unsynchronized.change alias for Proof General;

diff -r 89f273ab1d42 -r 712cb964d113 NEWS
--- a/NEWS	Fri Aug 27 14:07:09 2010 +0200
+++ b/NEWS	Fri Aug 27 14:14:08 2010 +0200
@@ -39,6 +39,12 @@
 Note that the corresponding "..._default" references may be only
 changed globally at the ROOT session setup, but *not* within a theory.
 
+* ML structure Unsynchronized never opened, not even in Isar
+interaction mode as before.  Old Unsynchronized.set etc. have been
+discontinued -- use plain := instead.  This should be *rare* anyway,
+since modern tools always work via official context data, notably
+configuration options.
+
 
 *** Pure ***
 
diff -r 89f273ab1d42 -r 712cb964d113 src/Pure/General/secure.ML
--- a/src/Pure/General/secure.ML	Fri Aug 27 14:07:09 2010 +0200
+++ b/src/Pure/General/secure.ML	Fri Aug 27 14:14:08 2010 +0200
@@ -13,7 +13,6 @@
   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 Isar_setup: unit -> unit
   val PG_setup: unit -> unit
   val commit: unit -> unit
   val bash_output: string -> string * int
@@ -56,8 +55,8 @@
 
 fun commit () = use_global "commit();";   (*commit is dynamically bound!*)
 
-fun Isar_setup () = use_global "open Unsynchronized;";
-fun PG_setup () = use_global "structure ThyLoad = ProofGeneral.ThyLoad;";
+fun PG_setup () =
+  use_global "val change = Unsynchronized.change; structure ThyLoad = ProofGeneral.ThyLoad;";
 
 
 (* shell commands *)
diff -r 89f273ab1d42 -r 712cb964d113 src/Pure/ML-Systems/unsynchronized.ML
--- a/src/Pure/ML-Systems/unsynchronized.ML	Fri Aug 27 14:07:09 2010 +0200
+++ b/src/Pure/ML-Systems/unsynchronized.ML	Fri Aug 27 14:14:08 2010 +0200
@@ -12,10 +12,6 @@
 val op := = op :=;
 val ! = !;
 
-fun set flag = (flag := true; true);
-fun reset flag = (flag := false; false);
-fun toggle flag = (flag := not (! flag); ! flag);
-
 fun change r f = r := f (! r);
 fun change_result r f = let val (x, y) = f (! r) in r := y; x end;
 
diff -r 89f273ab1d42 -r 712cb964d113 src/Pure/System/isar.ML
--- a/src/Pure/System/isar.ML	Fri Aug 27 14:07:09 2010 +0200
+++ b/src/Pure/System/isar.ML	Fri Aug 27 14:14:08 2010 +0200
@@ -134,7 +134,6 @@
 
 fun toplevel_loop in_stream {init = do_init, welcome, sync, secure} =
  (Context.set_thread_data NONE;
-  Secure.Isar_setup ();
   if do_init then init () else ();
   if welcome then writeln (Session.welcome ()) else ();
   uninterruptible (fn _ => fn () => raw_loop secure (Outer_Syntax.isar in_stream sync)) ());