# HG changeset patch
# User wenzelm
# Date 1269896157 -7200
# Node ID 0614676f14d468b913cd1cfefe5812bbc43ae2f6
# Parent  3ff725ac13a48f20d08066c0ec80a4dcd06ca677
replaced some deprecated methods;

diff -r 3ff725ac13a4 -r 0614676f14d4 src/Pure/General/scan.scala
--- a/src/Pure/General/scan.scala	Mon Mar 29 22:43:56 2010 +0200
+++ b/src/Pure/General/scan.scala	Mon Mar 29 22:55:57 2010 +0200
@@ -68,7 +68,7 @@
 
     /* pseudo Set methods */
 
-    def iterator: Iterator[String] = content(main_tree, Nil).sort(_ <= _).iterator
+    def iterator: Iterator[String] = content(main_tree, Nil).sortWith(_ <= _).iterator
 
     override def toString: String = iterator.mkString("Lexicon(", ", ", ")")
 
diff -r 3ff725ac13a4 -r 0614676f14d4 src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala	Mon Mar 29 22:43:56 2010 +0200
+++ b/src/Pure/System/isabelle_system.scala	Mon Mar 29 22:55:57 2010 +0200
@@ -288,7 +288,7 @@
         for (file <- files if file.isFile) logics += file.getName
       }
     }
-    logics.toList.sort(_ < _)
+    logics.toList.sortWith(_ < _)
   }
 
 
diff -r 3ff725ac13a4 -r 0614676f14d4 src/Pure/Thy/command.scala
--- a/src/Pure/Thy/command.scala	Mon Mar 29 22:43:56 2010 +0200
+++ b/src/Pure/Thy/command.scala	Mon Mar 29 22:55:57 2010 +0200
@@ -35,11 +35,11 @@
 {
   /* classification */
 
-  def is_command: Boolean = !span.isEmpty && span.first.is_command
+  def is_command: Boolean = !span.isEmpty && span.head.is_command
   def is_ignored: Boolean = span.forall(_.is_ignored)
   def is_malformed: Boolean = !is_command && !is_ignored
 
-  def name: String = if (is_command) span.first.content else ""
+  def name: String = if (is_command) span.head.content else ""
   override def toString = if (is_command) name else if (is_ignored) "<ignored>" else "<malformed>"
 
 
diff -r 3ff725ac13a4 -r 0614676f14d4 src/Pure/Thy/completion.scala
--- a/src/Pure/Thy/completion.scala	Mon Mar 29 22:43:56 2010 +0200
+++ b/src/Pure/Thy/completion.scala	Mon Mar 29 22:55:57 2010 +0200
@@ -94,7 +94,7 @@
           case Some(word) =>
             words_lex.completions(word).map(words_map(_)) match {
               case Nil => None
-              case cs => Some(word, cs.sort(_ < _))
+              case cs => Some(word, cs.sortWith(_ < _))
             }
           case None => None
         }
diff -r 3ff725ac13a4 -r 0614676f14d4 src/Pure/Thy/document.scala
--- a/src/Pure/Thy/document.scala	Mon Mar 29 22:43:56 2010 +0200
+++ b/src/Pure/Thy/document.scala	Mon Mar 29 22:55:57 2010 +0200
@@ -102,7 +102,7 @@
           val spans0 = Thy_Syntax.parse_spans(session.current_syntax.scan(sources.mkString))
 
           val (before_edit, spans1) =
-            if (!spans0.isEmpty && Some(spans0.first) == prefix.map(_.span))
+            if (!spans0.isEmpty && Some(spans0.head) == prefix.map(_.span))
               (prefix, spans0.tail)
             else (if (prefix.isDefined) commands.prev(prefix.get) else None, spans0)
 
diff -r 3ff725ac13a4 -r 0614676f14d4 src/Pure/Thy/html.scala
--- a/src/Pure/Thy/html.scala	Mon Mar 29 22:43:56 2010 +0200
+++ b/src/Pure/Thy/html.scala	Mon Mar 29 22:55:57 2010 +0200
@@ -41,13 +41,13 @@
         val t = new StringBuilder
         def flush() {
           if (!t.isEmpty) {
-            ts + XML.Text(t.toString)
+            ts += XML.Text(t.toString)
             t.clear
           }
         }
         def add(elem: XML.Tree) {
           flush()
-          ts + elem
+          ts += elem
         }
         val syms = Symbol.iterator(txt).map(_.toString)
         while (syms.hasNext) {
diff -r 3ff725ac13a4 -r 0614676f14d4 src/Pure/Thy/markup_node.scala
--- a/src/Pure/Thy/markup_node.scala	Mon Mar 29 22:43:56 2010 +0200
+++ b/src/Pure/Thy/markup_node.scala	Mon Mar 29 22:55:57 2010 +0200
@@ -24,7 +24,7 @@
   def set_branches(bs: List[Markup_Tree]): Markup_Tree = new Markup_Tree(node, bs)
 
   private def add(branch: Markup_Tree) =   // FIXME avoid sort
-    set_branches((branch :: branches) sort ((a, b) => a.node.start < b.node.start))
+    set_branches((branch :: branches).sortWith((a, b) => a.node.start < b.node.start))
 
   private def remove(bs: List[Markup_Tree]) = set_branches(branches -- bs)
 
diff -r 3ff725ac13a4 -r 0614676f14d4 src/Pure/Thy/state.scala
--- a/src/Pure/Thy/state.scala	Mon Mar 29 22:43:56 2010 +0200
+++ b/src/Pure/Thy/state.scala	Mon Mar 29 22:55:57 2010 +0200
@@ -84,7 +84,7 @@
                 val (begin, end) = Position.get_offsets(atts)
                 if (begin.isEmpty || end.isEmpty) state
                 else if (kind == Markup.ML_TYPING) {
-                  val info = body.first.asInstanceOf[XML.Text].content   // FIXME proper match!?
+                  val info = body.head.asInstanceOf[XML.Text].content   // FIXME proper match!?
                   state.add_markup(
                     command.markup_node(begin.get - 1, end.get - 1, Command.TypeInfo(info)))
                 }