# HG changeset patch
# User wenzelm
# Date 1314110476 -7200
# Node ID 5f9ad3583e0acc25662948f0dd0fc5dd953b45a0
# Parent  0f0ba362ce50378ed475977ab550ce0274d451b8
tuned signature;

diff -r 0f0ba362ce50 -r 5f9ad3583e0a src/Pure/Thy/thy_syntax.scala
--- a/src/Pure/Thy/thy_syntax.scala	Tue Aug 23 16:39:21 2011 +0200
+++ b/src/Pure/Thy/thy_syntax.scala	Tue Aug 23 16:41:16 2011 +0200
@@ -97,6 +97,37 @@
 
 
 
+  /** command perspective **/
+
+  def command_perspective(node: Document.Node, perspective: Text.Perspective): Command.Perspective =
+  {
+    if (perspective.isEmpty) Nil
+    else {
+      val result = new mutable.ListBuffer[Command]
+      @tailrec
+      def check_ranges(ranges: List[Text.Range], commands: Stream[(Command, Text.Offset)])
+      {
+        (ranges, commands) match {
+          case (range :: more_ranges, (command, offset) #:: more_commands) =>
+            val command_range = command.range + offset
+            range compare command_range match {
+              case -1 => check_ranges(more_ranges, commands)
+              case 0 =>
+                result += command
+                check_ranges(ranges, more_commands)
+              case 1 => check_ranges(ranges, more_commands)
+            }
+          case _ =>
+        }
+      }
+      val perspective_range = Text.Range(perspective.head.start, perspective.last.stop)
+      check_ranges(perspective, node.command_range(perspective_range).toStream)
+      result.toList
+    }
+  }
+
+
+
   /** text edits **/
 
   def text_edits(
@@ -172,37 +203,6 @@
     }
 
 
-    /* command perspective */
-
-    def command_perspective(node: Document.Node, perspective: Text.Perspective)
-        : Command.Perspective =
-    {
-      if (perspective.isEmpty) Nil
-      else {
-        val result = new mutable.ListBuffer[Command]
-        @tailrec
-        def check_ranges(ranges: List[Text.Range], commands: Stream[(Command, Text.Offset)])
-        {
-          (ranges, commands) match {
-            case (range :: more_ranges, (command, offset) #:: more_commands) =>
-              val command_range = command.range + offset
-              range compare command_range match {
-                case -1 => check_ranges(more_ranges, commands)
-                case 0 =>
-                  result += command
-                  check_ranges(ranges, more_commands)
-                case 1 => check_ranges(ranges, more_commands)
-              }
-            case _ =>
-          }
-        }
-        val perspective_range = Text.Range(perspective.head.start, perspective.last.stop)
-        check_ranges(perspective, node.command_range(perspective_range).toStream)
-        result.toList
-      }
-    }
-
-
     /* resulting document edits */
 
     {