src/Pure/PIDE/document.scala
changeset 56314 9a513737a0b2
parent 56309 5003ea266aef
child 56335 8953d4cc060a
     1.1 --- a/src/Pure/PIDE/document.scala	Sat Mar 29 09:24:39 2014 +0100
     1.2 +++ b/src/Pure/PIDE/document.scala	Sat Mar 29 09:34:51 2014 +0100
     1.3 @@ -189,7 +189,7 @@
     1.4  
     1.5      final class Commands private(val commands: Linear_Set[Command])
     1.6      {
     1.7 -      lazy val thy_load_commands: List[Command] =
     1.8 +      lazy val load_commands: List[Command] =
     1.9          commands.iterator.filter(cmd => !cmd.blobs.isEmpty).toList
    1.10  
    1.11        private lazy val full_index: (Array[(Command, Text.Offset)], Text.Range) =
    1.12 @@ -244,7 +244,7 @@
    1.13        perspective.overlays == other_perspective.overlays
    1.14  
    1.15      def commands: Linear_Set[Command] = _commands.commands
    1.16 -    def thy_load_commands: List[Command] = _commands.thy_load_commands
    1.17 +    def load_commands: List[Command] = _commands.load_commands
    1.18  
    1.19      def update_commands(new_commands: Linear_Set[Command]): Node =
    1.20        if (new_commands eq _commands.commands) this
    1.21 @@ -290,10 +290,10 @@
    1.22      def entries: Iterator[(Node.Name, Node)] =
    1.23        graph.entries.map({ case (name, (node, _)) => (name, node) })
    1.24  
    1.25 -    def thy_load_commands(file_name: Node.Name): List[Command] =
    1.26 +    def load_commands(file_name: Node.Name): List[Command] =
    1.27        (for {
    1.28          (_, node) <- entries
    1.29 -        cmd <- node.thy_load_commands.iterator
    1.30 +        cmd <- node.load_commands.iterator
    1.31          name <- cmd.blobs_names.iterator
    1.32          if name == file_name
    1.33        } yield cmd).toList
    1.34 @@ -421,7 +421,7 @@
    1.35  
    1.36      val node_name: Node.Name
    1.37      val node: Node
    1.38 -    val thy_load_commands: List[Command]
    1.39 +    val load_commands: List[Command]
    1.40      def is_loaded: Boolean
    1.41      def eq_content(other: Snapshot): Boolean
    1.42  
    1.43 @@ -694,11 +694,11 @@
    1.44          val node_name = name
    1.45          val node = version.nodes(name)
    1.46  
    1.47 -        val thy_load_commands: List[Command] =
    1.48 +        val load_commands: List[Command] =
    1.49            if (node_name.is_theory) Nil
    1.50 -          else version.nodes.thy_load_commands(node_name)
    1.51 +          else version.nodes.load_commands(node_name)
    1.52  
    1.53 -        val is_loaded: Boolean = node_name.is_theory || !thy_load_commands.isEmpty
    1.54 +        val is_loaded: Boolean = node_name.is_theory || !load_commands.isEmpty
    1.55  
    1.56          def eq_content(other: Snapshot): Boolean =
    1.57          {
    1.58 @@ -713,8 +713,8 @@
    1.59            !is_outdated && !other.is_outdated &&
    1.60            node.commands.size == other.node.commands.size &&
    1.61            (node.commands.iterator zip other.node.commands.iterator).forall(eq_commands) &&
    1.62 -          thy_load_commands.length == other.thy_load_commands.length &&
    1.63 -          (thy_load_commands zip other.thy_load_commands).forall(eq_commands)
    1.64 +          load_commands.length == other.load_commands.length &&
    1.65 +          (load_commands zip other.load_commands).forall(eq_commands)
    1.66          }
    1.67  
    1.68  
    1.69 @@ -729,7 +729,7 @@
    1.70          {
    1.71            val former_range = revert(range)
    1.72            val (file_name, command_range_iterator) =
    1.73 -            thy_load_commands match {
    1.74 +            load_commands match {
    1.75                case command :: _ => (node_name.node, Iterator((command, 0)))
    1.76                case _ => ("", node.command_range(former_range))
    1.77              }