structure Unsynchronized is never opened and set/reset/toggle have been discontinued;
retain Unsynchronized.change alias for Proof General;
--- 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 ***
--- 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 *)
--- 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;
--- 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)) ());