# HG changeset patch # User wenzelm # Date 1483609787 -3600 # Node ID 0e5ec80c352a116ba13d6b952eba7ebdf6b13128 # Parent 891a25a87ea1ef101accf5fc961db73c6dd6b3d6 tuned; diff -r 891a25a87ea1 -r 0e5ec80c352a 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 */