diff -r 3c2c912af2ef -r 1ba5331b4623 src/Pure/PIDE/document.ML --- a/src/Pure/PIDE/document.ML Fri Jul 08 21:44:47 2011 +0200 +++ b/src/Pure/PIDE/document.ML Fri Jul 08 22:00:53 2011 +0200 @@ -23,6 +23,8 @@ val define_command: command_id -> string -> state -> state val edit: version_id -> version_id -> edit list -> state -> (command_id * exec_id) list * state val execute: version_id -> state -> state + val state: unit -> state + val change_state: (state -> state) -> unit end; structure Document: DOCUMENT = @@ -359,5 +361,14 @@ in (versions, commands, execs, execution') end); + + +(** global state **) + +val global_state = Synchronized.var "Document" init_state; + +fun state () = Synchronized.value global_state; +val change_state = Synchronized.change global_state; + end;