# HG changeset patch
# User wenzelm
# Date 1274734911 -7200
# Node ID 9105c8237c7a41b8219b5022b551778560e69ebc
# Parent  dd3540a489f7ce4ce02e842365840a0819e2f024
renamed "rev" to "reverse" following usual Scala conventions;

diff -r dd3540a489f7 -r 9105c8237c7a src/Pure/General/linear_set.scala
--- a/src/Pure/General/linear_set.scala	Sat May 22 23:59:09 2010 +0200
+++ b/src/Pure/General/linear_set.scala	Mon May 24 23:01:51 2010 +0200
@@ -147,7 +147,7 @@
     if (contains(elem)) make_iterator(Some(elem), rep.nexts)
     else throw new Linear_Set.Undefined(elem.toString)
 
-  def rev_iterator(elem: A): Iterator[A] =
+  def reverse_iterator(elem: A): Iterator[A] =
     if (contains(elem)) make_iterator(Some(elem), rep.prevs)
     else throw new Linear_Set.Undefined(elem.toString)
 
diff -r dd3540a489f7 -r 9105c8237c7a src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Sat May 22 23:59:09 2010 +0200
+++ b/src/Pure/PIDE/document.scala	Mon May 24 23:01:51 2010 +0200
@@ -85,7 +85,7 @@
       commands.iterator.find(is_unparsed) match {
         case Some(first_unparsed) =>
           val first =
-            commands.rev_iterator(first_unparsed).find(_.is_command) getOrElse commands.head
+            commands.reverse_iterator(first_unparsed).find(_.is_command) getOrElse commands.head
           val last =
             commands.iterator(first_unparsed).find(_.is_command) getOrElse commands.last
           val range =
diff -r dd3540a489f7 -r 9105c8237c7a src/Pure/PIDE/state.scala
--- a/src/Pure/PIDE/state.scala	Sat May 22 23:59:09 2010 +0200
+++ b/src/Pure/PIDE/state.scala	Mon May 24 23:01:51 2010 +0200
@@ -11,7 +11,7 @@
 class State(
   val command: Command,
   val status: Command.Status.Value,
-  val rev_results: List[XML.Tree],
+  val reverse_results: List[XML.Tree],
   val markup_root: Markup_Text)
 {
   def this(command: Command) =
@@ -21,15 +21,15 @@
   /* content */
 
   private def set_status(st: Command.Status.Value): State =
-    new State(command, st, rev_results, markup_root)
+    new State(command, st, reverse_results, markup_root)
 
   private def add_result(res: XML.Tree): State =
-    new State(command, status, res :: rev_results, markup_root)
+    new State(command, status, res :: reverse_results, markup_root)
 
   private def add_markup(node: Markup_Tree): State =
-    new State(command, status, rev_results, markup_root + node)
+    new State(command, status, reverse_results, markup_root + node)
 
-  lazy val results = rev_results.reverse
+  lazy val results = reverse_results.reverse
 
 
   /* markup */
diff -r dd3540a489f7 -r 9105c8237c7a src/Pure/System/session_manager.scala
--- a/src/Pure/System/session_manager.scala	Sat May 22 23:59:09 2010 +0200
+++ b/src/Pure/System/session_manager.scala	Mon May 24 23:01:51 2010 +0200
@@ -22,21 +22,21 @@
 
 
   // FIXME handle (potentially cyclic) directory graph
-  private def find_sessions(rev_prefix: List[String], rev_sessions: List[List[String]],
+  private def find_sessions(reverse_prefix: List[String], reverse_sessions: List[List[String]],
     dir: File): List[List[String]] =
   {
-    val (rev_prefix1, rev_sessions1) =
+    val (reverse_prefix1, reverse_sessions1) =
       if (is_session_dir(dir)) {
         val name = dir.getName  // FIXME from root file
-        val rev_prefix1 = name :: rev_prefix
-        val rev_sessions1 = rev_prefix1.reverse :: rev_sessions
-        (rev_prefix1, rev_sessions1)
+        val reverse_prefix1 = name :: reverse_prefix
+        val reverse_sessions1 = reverse_prefix1.reverse :: reverse_sessions
+        (reverse_prefix1, reverse_sessions1)
       }
-      else (rev_prefix, rev_sessions)
+      else (reverse_prefix, reverse_sessions)
 
     val subdirs =
       dir.listFiles(new FileFilter { def accept(entry: File) = entry.isDirectory })
-    (rev_sessions1 /: subdirs)(find_sessions(rev_prefix1, _, _))
+    (reverse_sessions1 /: subdirs)(find_sessions(reverse_prefix1, _, _))
   }
 
   def component_sessions(): List[List[String]] =
diff -r dd3540a489f7 -r 9105c8237c7a src/Pure/Thy/completion.scala
--- a/src/Pure/Thy/completion.scala	Sat May 22 23:59:09 2010 +0200
+++ b/src/Pure/Thy/completion.scala	Mon May 24 23:01:51 2010 +0200
@@ -21,14 +21,14 @@
   {
     override val whiteSpace = "".r
 
-    def rev_symbol: Parser[String] = """>[A-Za-z0-9_']+<\\""".r
-    def rev_symb: Parser[String] = """[A-Za-z0-9_']{2,}<\\""".r
+    def reverse_symbol: Parser[String] = """>[A-Za-z0-9_']+<\\""".r
+    def reverse_symb: Parser[String] = """[A-Za-z0-9_']{2,}<\\""".r
     def word: Parser[String] = "[a-zA-Z0-9_']{3,}".r
 
     def read(in: CharSequence): Option[String] =
     {
-      val rev_in = new Library.Reverse(in)
-      parse((rev_symbol | rev_symb | word) ^^ (_.reverse), rev_in) match {
+      val reverse_in = new Library.Reverse(in)
+      parse((reverse_symbol | reverse_symb | word) ^^ (_.reverse), reverse_in) match {
         case Success(result, _) => Some(result)
         case _ => None
       }
@@ -86,8 +86,8 @@
   def complete(line: CharSequence): Option[(String, List[String])] =
   {
     abbrevs_lex.parse(abbrevs_lex.keyword, new Library.Reverse(line)) match {
-      case abbrevs_lex.Success(rev_a, _) =>
-        val (word, c) = abbrevs_map(rev_a)
+      case abbrevs_lex.Success(reverse_a, _) =>
+        val (word, c) = abbrevs_map(reverse_a)
         Some(word, List(c))
       case _ =>
         Completion.Parse.read(line) match {