# HG changeset patch
# User wenzelm
# Date 1310229300 -7200
# Node ID ba1b2c918c322771550cd9ac7a2cbe9e28f62147
# Parent  4a4ca9e4a14b4a97ca70583dfc8956237056ffa7
tuned signature;

diff -r 4a4ca9e4a14b -r ba1b2c918c32 src/Pure/Concurrent/volatile.scala
--- a/src/Pure/Concurrent/volatile.scala	Sat Jul 09 18:15:23 2011 +0200
+++ b/src/Pure/Concurrent/volatile.scala	Sat Jul 09 18:35:00 2011 +0200
@@ -10,7 +10,7 @@
 class Volatile[A](init: A)
 {
   @volatile private var state: A = init
-  def peek(): A = state
+  def apply(): A = state
   def change(f: A => A) { state = f(state) }
   def change_yield[B](f: A => (B, A)): B =
   {
diff -r 4a4ca9e4a14b -r ba1b2c918c32 src/Pure/System/session.scala
--- a/src/Pure/System/session.scala	Sat Jul 09 18:15:23 2011 +0200
+++ b/src/Pure/System/session.scala	Sat Jul 09 18:35:00 2011 +0200
@@ -133,10 +133,10 @@
   def is_ready: Boolean = phase == Session.Ready
 
   private val global_state = new Volatile(Document.State.init)
-  def current_state(): Document.State = global_state.peek()
+  def current_state(): Document.State = global_state()
 
   def snapshot(name: String, pending_edits: List[Text.Edit]): Document.Snapshot =
-    current_state().snapshot(name, pending_edits)
+    global_state().snapshot(name, pending_edits)
 
 
   /* theory files */
@@ -180,13 +180,13 @@
     //{{{
     {
       val syntax = current_syntax()
-      val previous = current_state().history.tip.version
+      val previous = global_state().history.tip.version
       val doc_edits = edits.map(edit => (name, edit))
       val result = Future.fork { Thy_Syntax.text_edits(syntax, previous.join, doc_edits) }
       val change = global_state.change_yield(_.extend_history(previous, doc_edits, result))
 
       change.version.map(_ => {
-        assignments.await { current_state().is_assigned(previous.get_finished) }
+        assignments.await { global_state().is_assigned(previous.get_finished) }
         this_actor ! Change_Node(name, header, change) })
     }
     //}}}
@@ -200,7 +200,7 @@
       val previous = change.previous.get_finished
       val (node_edits, version) = change.result.get_finished
 
-      var former_assignment = current_state().the_assignment(previous).get_finished
+      var former_assignment = global_state().the_assignment(previous).get_finished
       for {
         (name, Some(cmd_edits)) <- node_edits
         (prev, None) <- cmd_edits
@@ -219,7 +219,7 @@
                     c2 match {
                       case None => None
                       case Some(command) =>
-                        if (current_state().lookup_command(command.id).isEmpty) {
+                        if (global_state().lookup_command(command.id).isEmpty) {
                           global_state.change(_.define_command(command))
                           prover.get.define_command(command.id, Symbol.encode(command.source))
                         }