moved global state to structure Document (again);
authorwenzelm
Fri Jul 08 22:00:53 2011 +0200 (2011-07-08)
changeset 437131ba5331b4623
parent 43712 3c2c912af2ef
child 43714 3749d1e6dde9
child 43732 6b2bdc57155b
moved global state to structure Document (again);
src/Pure/PIDE/document.ML
src/Pure/PIDE/isar_document.ML
     1.1 --- a/src/Pure/PIDE/document.ML	Fri Jul 08 21:44:47 2011 +0200
     1.2 +++ b/src/Pure/PIDE/document.ML	Fri Jul 08 22:00:53 2011 +0200
     1.3 @@ -23,6 +23,8 @@
     1.4    val define_command: command_id -> string -> state -> state
     1.5    val edit: version_id -> version_id -> edit list -> state -> (command_id * exec_id) list * state
     1.6    val execute: version_id -> state -> state
     1.7 +  val state: unit -> state
     1.8 +  val change_state: (state -> state) -> unit
     1.9  end;
    1.10  
    1.11  structure Document: DOCUMENT =
    1.12 @@ -359,5 +361,14 @@
    1.13  
    1.14      in (versions, commands, execs, execution') end);
    1.15  
    1.16 +
    1.17 +
    1.18 +(** global state **)
    1.19 +
    1.20 +val global_state = Synchronized.var "Document" init_state;
    1.21 +
    1.22 +fun state () = Synchronized.value global_state;
    1.23 +val change_state = Synchronized.change global_state;
    1.24 +
    1.25  end;
    1.26  
     2.1 --- a/src/Pure/PIDE/isar_document.ML	Fri Jul 08 21:44:47 2011 +0200
     2.2 +++ b/src/Pure/PIDE/isar_document.ML	Fri Jul 08 22:00:53 2011 +0200
     2.3 @@ -4,26 +4,16 @@
     2.4  Protocol message formats for interactive Isar documents.
     2.5  *)
     2.6  
     2.7 -signature ISAR_DOCUMENT =
     2.8 -sig
     2.9 -  val state: unit -> Document.state
    2.10 -end
    2.11 -
    2.12 -structure Isar_Document: ISAR_DOCUMENT =
    2.13 +structure Isar_Document: sig end =
    2.14  struct
    2.15  
    2.16 -val global_state = Synchronized.var "Isar_Document" Document.init_state;
    2.17 -val change_state = Synchronized.change global_state;
    2.18 -
    2.19 -fun state () = Synchronized.value global_state;
    2.20 -
    2.21  val _ =
    2.22    Isabelle_Process.add_command "Isar_Document.define_command"
    2.23 -    (fn [id, text] => change_state (Document.define_command (Document.parse_id id) text));
    2.24 +    (fn [id, text] => Document.change_state (Document.define_command (Document.parse_id id) text));
    2.25  
    2.26  val _ =
    2.27    Isabelle_Process.add_command "Isar_Document.edit_version"
    2.28 -    (fn [old_id_string, new_id_string, edits_yxml] => change_state (fn state =>
    2.29 +    (fn [old_id_string, new_id_string, edits_yxml] => Document.change_state (fn state =>
    2.30        let
    2.31          val old_id = Document.parse_id old_id_string;
    2.32          val new_id = Document.parse_id new_id_string;