# HG changeset patch
# User wenzelm
# Date 1310155253 -7200
# Node ID 1ba5331b462384d38771d7fe964bcc5fd56c7f06
# Parent  3c2c912af2ef7dd6014c5df11aa356b6050e02c2
moved global state to structure Document (again);

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;
 
diff -r 3c2c912af2ef -r 1ba5331b4623 src/Pure/PIDE/isar_document.ML
--- a/src/Pure/PIDE/isar_document.ML	Fri Jul 08 21:44:47 2011 +0200
+++ b/src/Pure/PIDE/isar_document.ML	Fri Jul 08 22:00:53 2011 +0200
@@ -4,26 +4,16 @@
 Protocol message formats for interactive Isar documents.
 *)
 
-signature ISAR_DOCUMENT =
-sig
-  val state: unit -> Document.state
-end
-
-structure Isar_Document: ISAR_DOCUMENT =
+structure Isar_Document: sig end =
 struct
 
-val global_state = Synchronized.var "Isar_Document" Document.init_state;
-val change_state = Synchronized.change global_state;
-
-fun state () = Synchronized.value global_state;
-
 val _ =
   Isabelle_Process.add_command "Isar_Document.define_command"
-    (fn [id, text] => change_state (Document.define_command (Document.parse_id id) text));
+    (fn [id, text] => Document.change_state (Document.define_command (Document.parse_id id) text));
 
 val _ =
   Isabelle_Process.add_command "Isar_Document.edit_version"
-    (fn [old_id_string, new_id_string, edits_yxml] => change_state (fn state =>
+    (fn [old_id_string, new_id_string, edits_yxml] => Document.change_state (fn state =>
       let
         val old_id = Document.parse_id old_id_string;
         val new_id = Document.parse_id new_id_string;