src/Pure/PIDE/document.scala

--- a/src/Pure/PIDE/document.scala	Thu Jan 05 10:10:51 2017 +0100
+++ b/src/Pure/PIDE/document.scala	Thu Jan 05 10:49:47 2017 +0100
@@ -432,18 +432,18 @@
 
   abstract class Snapshot
   {
-    val state: State
-    val version: Version
-    val is_outdated: Boolean
+    def state: State
+    def version: Version
+    def is_outdated: Boolean
 
     def convert(i: Text.Offset): Text.Offset
     def revert(i: Text.Offset): Text.Offset
     def convert(range: Text.Range): Text.Range
     def revert(range: Text.Range): Text.Range
 
-    val node_name: Node.Name
-    val node: Node
-    val load_commands: List[Command]
+    def node_name: Node.Name
+    def node: Node
+    def load_commands: List[Command]
     def is_loaded: Boolean
 
     def find_command(id: Document_ID.Generic): Option[(Node, Command)]
@@ -755,9 +755,9 @@
       {
         /* global information */
 
-        val state = State.this
-        val version = stable.version.get_finished
-        val is_outdated = pending_edits.nonEmpty || latest != stable
+        val state: State = State.this
+        val version: Version = stable.version.get_finished
+        val is_outdated: Boolean = pending_edits.nonEmpty || latest != stable
 
 
         /* local node content */
@@ -770,14 +770,14 @@
         def convert(range: Text.Range) = range.map(convert(_))
         def revert(range: Text.Range) = range.map(revert(_))
 
-        val node_name = name
-        val node = version.nodes(name)
+        val node_name: Node.Name = name
+        def node: Node = version.nodes(name)
 
         val load_commands: List[Command] =
           if (node_name.is_theory) Nil
           else version.nodes.load_commands(node_name)
 
-        val is_loaded: Boolean = node_name.is_theory || load_commands.nonEmpty
+        def is_loaded: Boolean = node_name.is_theory || load_commands.nonEmpty
 
 
         /* find command */