# HG changeset patch
# User wenzelm
# Date 1269946059 -7200
# Node ID 8b25e3b217bce5f235def59a1e96e301b765ba97
# Parent  fcd7bea01a93fc9c741e7c98ecf86ed4747b8168# Parent  4f5c7a19ebe04f17e08d954a26663122baaab723
merged

diff -r fcd7bea01a93 -r 8b25e3b217bc src/Pure/General/linear_set.scala
--- a/src/Pure/General/linear_set.scala	Mon Mar 29 17:30:56 2010 +0200
+++ b/src/Pure/General/linear_set.scala	Tue Mar 30 12:47:39 2010 +0200
@@ -7,27 +7,36 @@
 
 package isabelle
 
+import scala.collection.SetLike
+import scala.collection.generic.{SetFactory, CanBuildFrom, GenericSetTemplate, GenericCompanion}
 
-object Linear_Set
+
+object Linear_Set extends SetFactory[Linear_Set]
 {
   private case class Rep[A](
-    val first: Option[A], val last: Option[A], val nexts: Map[A, A], prevs: Map[A, A])
+    val start: Option[A], val end: Option[A], val nexts: Map[A, A], prevs: Map[A, A])
 
   private def empty_rep[A] = Rep[A](None, None, Map(), Map())
 
-  private def make[A](first: Option[A], last: Option[A], nexts: Map[A, A], prevs: Map[A, A])
-    : Linear_Set[A] = new Linear_Set[A] { override val rep = Rep(first, last, nexts, prevs) }
+  private def make[A](start: Option[A], end: Option[A], nexts: Map[A, A], prevs: Map[A, A])
+    : Linear_Set[A] = new Linear_Set[A] { override val rep = Rep(start, end, nexts, prevs) }
 
-  def empty[A]: Linear_Set[A] = new Linear_Set
-  def apply[A](elems: A*): Linear_Set[A] = empty[A] ++ elems
+  implicit def canBuildFrom[A]: CanBuildFrom[Coll, A, Linear_Set[A]] = setCanBuildFrom[A]
+  override def empty[A] = new Linear_Set[A]
 
   class Duplicate(s: String) extends Exception(s)
   class Undefined(s: String) extends Exception(s)
 }
 
 
-class Linear_Set[A] extends scala.collection.immutable.Set[A]
+class Linear_Set[A]
+  extends scala.collection.immutable.Set[A]
+  with GenericSetTemplate[A, Linear_Set]
+  with SetLike[A, Linear_Set[A]]
 {
+  override def companion: GenericCompanion[Linear_Set] = Linear_Set
+
+
   /* representation */
 
   protected val rep = Linear_Set.empty_rep[A]
@@ -43,10 +52,10 @@
     else
       hook match {
         case None =>
-          rep.first match {
+          rep.start match {
             case None => Linear_Set.make(Some(elem), Some(elem), Map(), Map())
             case Some(elem1) =>
-              Linear_Set.make(Some(elem), rep.last,
+              Linear_Set.make(Some(elem), rep.end,
                 rep.nexts + (elem -> elem1), rep.prevs + (elem1 -> elem))
           }
         case Some(elem1) =>
@@ -54,10 +63,10 @@
           else
             rep.nexts.get(elem1) match {
               case None =>
-                Linear_Set.make(rep.first, Some(elem),
+                Linear_Set.make(rep.start, Some(elem),
                   rep.nexts + (elem1 -> elem), rep.prevs + (elem -> elem1))
               case Some(elem2) =>
-                Linear_Set.make(rep.first, rep.last,
+                Linear_Set.make(rep.start, rep.end,
                   rep.nexts + (elem1 -> elem) + (elem -> elem2),
                   rep.prevs + (elem2 -> elem) + (elem -> elem1))
             }
@@ -66,13 +75,13 @@
   def delete_after(hook: Option[A]): Linear_Set[A] =
     hook match {
       case None =>
-        rep.first match {
+        rep.start match {
           case None => throw new Linear_Set.Undefined("")
           case Some(elem1) =>
             rep.nexts.get(elem1) match {
               case None => empty
               case Some(elem2) =>
-                Linear_Set.make(Some(elem2), rep.last, rep.nexts - elem1, rep.prevs - elem2)
+                Linear_Set.make(Some(elem2), rep.end, rep.nexts - elem1, rep.prevs - elem2)
             }
         }
       case Some(elem1) =>
@@ -83,9 +92,9 @@
             case Some(elem2) =>
               rep.nexts.get(elem2) match {
                 case None =>
-                  Linear_Set.make(rep.first, Some(elem1), rep.nexts - elem1, rep.prevs - elem2)
+                  Linear_Set.make(rep.start, Some(elem1), rep.nexts - elem1, rep.prevs - elem2)
                 case Some(elem3) =>
-                  Linear_Set.make(rep.first, rep.last,
+                  Linear_Set.make(rep.start, rep.end,
                     rep.nexts - elem2 + (elem1 -> elem3),
                     rep.prevs - elem2 + (elem3 -> elem1))
               }
@@ -100,8 +109,8 @@
     if (isEmpty) this
     else {
       val next =
-        if (from == rep.last) None
-        else if (from == None) rep.first
+        if (from == rep.end) None
+        else if (from == None) rep.start
         else from.map(rep.nexts(_))
       if (next == to) this
       else delete_after(from).delete_between(from, to)
@@ -113,15 +122,13 @@
 
   override def stringPrefix = "Linear_Set"
 
-  def empty[B]: Linear_Set[B] = Linear_Set.empty
-
-  override def isEmpty: Boolean = !rep.first.isDefined
-  def size: Int = if (isEmpty) 0 else rep.nexts.size + 1
+  override def isEmpty: Boolean = !rep.start.isDefined
+  override def size: Int = if (isEmpty) 0 else rep.nexts.size + 1
 
   def contains(elem: A): Boolean =
-    !isEmpty && (rep.last.get == elem || rep.nexts.isDefinedAt(elem))
+    !isEmpty && (rep.end.get == elem || rep.nexts.isDefinedAt(elem))
 
-  private def elements_from(start: Option[A]): Iterator[A] = new Iterator[A] {
+  private def iterator_from(start: Option[A]): Iterator[A] = new Iterator[A] {
     private var next_elem = start
     def hasNext = next_elem.isDefined
     def next =
@@ -133,18 +140,13 @@
       }
   }
 
-  def elements: Iterator[A] = elements_from(rep.first)
+  override def iterator: Iterator[A] = iterator_from(rep.start)
 
-  def elements(elem: A): Iterator[A] =
-    if (contains(elem)) elements_from(Some(elem))
+  def iterator(elem: A): Iterator[A] =
+    if (contains(elem)) iterator_from(Some(elem))
     else throw new Linear_Set.Undefined(elem.toString)
 
-  def + (elem: A): Linear_Set[A] = insert_after(rep.last, elem)
-
-  override def + (elem1: A, elem2: A, elems: A*): Linear_Set[A] =
-    this + elem1 + elem2 ++ elems
-  override def ++ (elems: Iterable[A]): Linear_Set[A] = (this /: elems) ((s, elem) => s + elem)
-  override def ++ (elems: Iterator[A]): Linear_Set[A] = (this /: elems) ((s, elem) => s + elem)
+  def + (elem: A): Linear_Set[A] = insert_after(rep.end, elem)
 
   def - (elem: A): Linear_Set[A] =
     if (!contains(elem)) throw new Linear_Set.Undefined(elem.toString)
diff -r fcd7bea01a93 -r 8b25e3b217bc src/Pure/General/scan.scala
--- a/src/Pure/General/scan.scala	Mon Mar 29 17:30:56 2010 +0200
+++ b/src/Pure/General/scan.scala	Tue Mar 30 12:47:39 2010 +0200
@@ -7,6 +7,7 @@
 package isabelle
 
 
+import scala.collection.generic.Addable
 import scala.collection.immutable.PagedSeq
 import scala.util.parsing.input.{OffsetPosition, Position => InputPosition, Reader}
 import scala.util.parsing.combinator.RegexParsers
@@ -27,7 +28,7 @@
     def apply(elems: String*): Lexicon = empty ++ elems
   }
 
-  class Lexicon extends scala.collection.Set[String] with RegexParsers
+  class Lexicon extends Addable[String, Lexicon] with RegexParsers
   {
     /* representation */
 
@@ -65,14 +66,14 @@
       }
 
 
-    /* Set methods */
+    /* pseudo Set methods */
 
-    override def stringPrefix = "Lexicon"
+    def iterator: Iterator[String] = content(main_tree, Nil).sortWith(_ <= _).iterator
 
-    override def isEmpty: Boolean = { main_tree.branches.isEmpty }
+    override def toString: String = iterator.mkString("Lexicon(", ", ", ")")
 
-    def size: Int = content(main_tree, Nil).length
-    def elements: Iterator[String] = content(main_tree, Nil).sort(_ <= _).elements
+    def empty: Lexicon = Lexicon.empty
+    def isEmpty: Boolean = main_tree.branches.isEmpty
 
     def contains(elem: String): Boolean =
       lookup(elem) match {
@@ -80,6 +81,11 @@
         case _ => false
       }
 
+
+    /* Addable methods */
+
+    def repr = this
+
     def + (elem: String): Lexicon =
       if (contains(elem)) this
       else {
@@ -102,11 +108,6 @@
         new Lexicon { override val main_tree = extend(old.main_tree, 0) }
       }
 
-    def + (elem1: String, elem2: String, elems: String*): Lexicon =
-      this + elem1 + elem2 ++ elems
-    def ++ (elems: Iterable[String]): Lexicon = (this /: elems) ((s, elem) => s + elem)
-    def ++ (elems: Iterator[String]): Lexicon = (this /: elems) ((s, elem) => s + elem)
-
 
 
     /** RegexParsers methods **/
diff -r fcd7bea01a93 -r 8b25e3b217bc src/Pure/General/symbol.scala
--- a/src/Pure/General/symbol.scala	Mon Mar 29 17:30:56 2010 +0200
+++ b/src/Pure/General/symbol.scala	Tue Mar 30 12:47:39 2010 +0200
@@ -7,7 +7,7 @@
 package isabelle
 
 import scala.io.Source
-import scala.collection.{jcl, mutable}
+import scala.collection.mutable
 import scala.util.matching.Regex
 
 
@@ -54,9 +54,9 @@
   }
 
 
-  /* elements */
+  /* iterator */
 
-  def elements(text: CharSequence) = new Iterator[CharSequence]
+  def iterator(text: CharSequence) = new Iterator[CharSequence]
   {
     private val matcher = new Matcher(text)
     private var i = 0
@@ -124,12 +124,7 @@
       }
       (min, max)
     }
-    private val table =
-    {
-      val table = new jcl.HashMap[String, String]   // reasonably efficient?
-      for ((x, y) <- list) table + (x -> y)
-      table
-    }
+    private val table = Map[String, String]() ++ list
     def recode(text: String): String =
     {
       val len = text.length
diff -r fcd7bea01a93 -r 8b25e3b217bc src/Pure/General/xml.scala
--- a/src/Pure/General/xml.scala	Mon Mar 29 17:30:56 2010 +0200
+++ b/src/Pure/General/xml.scala	Tue Mar 30 12:47:39 2010 +0200
@@ -34,34 +34,34 @@
   /* string representation */
 
   private def append_text(text: String, s: StringBuilder) {
-    if (text == null) s ++ text
+    if (text == null) s ++= text
     else {
-      for (c <- text.elements) c match {
-        case '<' => s ++ "&lt;"
-        case '>' => s ++ "&gt;"
-        case '&' => s ++ "&amp;"
-        case '"' => s ++ "&quot;"
-        case '\'' => s ++ "&apos;"
-        case _ => s + c
+      for (c <- text.iterator) c match {
+        case '<' => s ++= "&lt;"
+        case '>' => s ++= "&gt;"
+        case '&' => s ++= "&amp;"
+        case '"' => s ++= "&quot;"
+        case '\'' => s ++= "&apos;"
+        case _ => s += c
       }
     }
   }
 
   private def append_elem(name: String, atts: Attributes, s: StringBuilder) {
-    s ++ name
+    s ++= name
     for ((a, x) <- atts) {
-      s ++ " "; s ++ a; s ++ "=\""; append_text(x, s); s ++ "\""
+      s ++= " "; s ++= a; s ++= "=\""; append_text(x, s); s ++= "\""
     }
   }
 
   private def append_tree(tree: Tree, s: StringBuilder) {
     tree match {
       case Elem(name, atts, Nil) =>
-        s ++ "<"; append_elem(name, atts, s); s ++ "/>"
+        s ++= "<"; append_elem(name, atts, s); s ++= "/>"
       case Elem(name, atts, ts) =>
-        s ++ "<"; append_elem(name, atts, s); s ++ ">"
+        s ++= "<"; append_elem(name, atts, s); s ++= ">"
         for (t <- ts) append_tree(t, s)
-        s ++ "</"; s ++ name; s ++ ">"
+        s ++= "</"; s ++= name; s ++= ">"
       case Text(text) => append_text(text, s)
     }
   }
diff -r fcd7bea01a93 -r 8b25e3b217bc src/Pure/System/isabelle_syntax.scala
--- a/src/Pure/System/isabelle_syntax.scala	Mon Mar 29 17:30:56 2010 +0200
+++ b/src/Pure/System/isabelle_syntax.scala	Tue Mar 30 12:47:39 2010 +0200
@@ -40,7 +40,7 @@
     result: StringBuilder)
   {
     result.append("(")
-    val elems = body.elements
+    val elems = body.iterator
     if (elems.hasNext) append_elem(elems.next, result)
     while (elems.hasNext) {
       result.append(", ")
diff -r fcd7bea01a93 -r 8b25e3b217bc src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala	Mon Mar 29 17:30:56 2010 +0200
+++ b/src/Pure/System/isabelle_system.scala	Tue Mar 30 12:47:39 2010 +0200
@@ -24,7 +24,7 @@
 
   private val environment: Map[String, String] =
   {
-    import scala.collection.jcl.Conversions._
+    import scala.collection.JavaConversions._
 
     val env0 = Map(java.lang.System.getenv.toList: _*)
 
@@ -288,7 +288,7 @@
         for (file <- files if file.isFile) logics += file.getName
       }
     }
-    logics.toList.sort(_ < _)
+    logics.toList.sortWith(_ < _)
   }
 
 
@@ -297,7 +297,7 @@
   private def read_symbols(path: String): List[String] =
   {
     val file = platform_file(path)
-    if (file.isFile) Source.fromFile(file).getLines.toList
+    if (file.isFile) Source.fromFile(file).getLines().toList
     else Nil
   }
   val symbols = new Symbol.Interpretation(
diff -r fcd7bea01a93 -r 8b25e3b217bc src/Pure/System/standard_system.scala
--- a/src/Pure/System/standard_system.scala	Mon Mar 29 17:30:56 2010 +0200
+++ b/src/Pure/System/standard_system.scala	Tue Mar 30 12:47:39 2010 +0200
@@ -12,7 +12,7 @@
   BufferedInputStream, FileInputStream, BufferedReader, InputStreamReader,
   File, FileFilter, IOException}
 
-import scala.io.Source
+import scala.io.{Source, Codec}
 import scala.util.matching.Regex
 import scala.collection.mutable
 
@@ -20,6 +20,7 @@
 object Standard_System
 {
   val charset = "UTF-8"
+  def codec(): Codec = Codec(charset)
 
 
   /* permissive UTF-8 decoding */
@@ -135,7 +136,7 @@
   def process_output(proc: Process): (String, Int) =
   {
     proc.getOutputStream.close
-    val output = Source.fromInputStream(proc.getInputStream, charset).mkString  // FIXME
+    val output = Source.fromInputStream(proc.getInputStream)(codec()).mkString  // FIXME
     val rc =
       try { proc.waitFor }
       finally {
diff -r fcd7bea01a93 -r 8b25e3b217bc src/Pure/Thy/command.scala
--- a/src/Pure/Thy/command.scala	Mon Mar 29 17:30:56 2010 +0200
+++ b/src/Pure/Thy/command.scala	Tue Mar 30 12:47:39 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 fcd7bea01a93 -r 8b25e3b217bc src/Pure/Thy/completion.scala
--- a/src/Pure/Thy/completion.scala	Mon Mar 29 17:30:56 2010 +0200
+++ b/src/Pure/Thy/completion.scala	Tue Mar 30 12:47:39 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 fcd7bea01a93 -r 8b25e3b217bc src/Pure/Thy/document.scala
--- a/src/Pure/Thy/document.scala	Mon Mar 29 17:30:56 2010 +0200
+++ b/src/Pure/Thy/document.scala	Tue Mar 30 12:47:39 2010 +0200
@@ -14,7 +14,7 @@
   def command_starts(commands: Linear_Set[Command]): Iterator[(Command, Int)] =
   {
     var offset = 0
-    for (cmd <- commands.elements) yield {
+    for (cmd <- commands.iterator) yield {
       val start = offset
       offset += cmd.length
       (cmd, start)
@@ -92,17 +92,17 @@
     def parse_spans(commands: Linear_Set[Command]): Linear_Set[Command] =
     {
       // FIXME relative search!
-      commands.elements.find(is_unparsed) match {
+      commands.iterator.find(is_unparsed) match {
         case Some(first_unparsed) =>
           val prefix = commands.prev(first_unparsed)
-          val body = commands.elements(first_unparsed).takeWhile(is_unparsed).toList
+          val body = commands.iterator(first_unparsed).takeWhile(is_unparsed).toList
           val suffix = commands.next(body.last)
 
           val sources = (prefix.toList ::: body ::: suffix.toList).flatMap(_.span.map(_.source))
           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)
 
@@ -128,8 +128,8 @@
       val commands1 = Library.timeit("edit_text") { edit_text(edits, commands0) }
       val commands2 = Library.timeit("parse_spans") { parse_spans(commands1) }
 
-      val removed_commands = commands0.elements.filter(!commands2.contains(_)).toList
-      val inserted_commands = commands2.elements.filter(!commands0.contains(_)).toList
+      val removed_commands = commands0.iterator.filter(!commands2.contains(_)).toList
+      val inserted_commands = commands2.iterator.filter(!commands0.contains(_)).toList
 
       val doc_edits =
         removed_commands.reverse.map(cmd => (commands0.prev(cmd), None)) :::
diff -r fcd7bea01a93 -r 8b25e3b217bc src/Pure/Thy/html.scala
--- a/src/Pure/Thy/html.scala	Mon Mar 29 17:30:56 2010 +0200
+++ b/src/Pure/Thy/html.scala	Tue Mar 30 12:47:39 2010 +0200
@@ -41,29 +41,29 @@
         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.elements(txt).map(_.toString)
+        val syms = Symbol.iterator(txt).map(_.toString)
         while (syms.hasNext) {
           val s1 = syms.next
           def s2() = if (syms.hasNext) syms.next else ""
           s1 match {
             case "\n" => add(XML.elem(BR))
-            case "\\<^bsub>" => t ++ s1  // FIXME
-            case "\\<^esub>" => t ++ s1  // FIXME
-            case "\\<^bsup>" => t ++ s1  // FIXME
-            case "\\<^esup>" => t ++ s1  // FIXME
+            case "\\<^bsub>" => t ++= s1  // FIXME
+            case "\\<^esub>" => t ++= s1  // FIXME
+            case "\\<^bsup>" => t ++= s1  // FIXME
+            case "\\<^esup>" => t ++= s1  // FIXME
             case "\\<^sub>" | "\\<^isub>" => add(hidden(s1)); add(sub(s2()))
             case "\\<^sup>" | "\\<^isup>" => add(hidden(s1)); add(sup(s2()))
             case "\\<^bold>" => add(hidden(s1)); add(span("bold", List(XML.Text(s2()))))
             case "\\<^loc>" => add(hidden(s1)); add(span("loc", List(XML.Text(s2()))))
-            case _ => t ++ s1
+            case _ => t ++= s1
           }
         }
         flush()
diff -r fcd7bea01a93 -r 8b25e3b217bc src/Pure/Thy/markup_node.scala
--- a/src/Pure/Thy/markup_node.scala	Mon Mar 29 17:30:56 2010 +0200
+++ b/src/Pure/Thy/markup_node.scala	Tue Mar 30 12:47:39 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)
 
@@ -70,7 +70,7 @@
           markup <- markups
         } yield markup
       if (next_x < node.stop)
-        filled_gaps + new Markup_Node(next_x, node.stop, node.info)
+        filled_gaps ::: List(new Markup_Node(next_x, node.stop, node.info))
       else filled_gaps
     }
   }
diff -r fcd7bea01a93 -r 8b25e3b217bc src/Pure/Thy/state.scala
--- a/src/Pure/Thy/state.scala	Mon Mar 29 17:30:56 2010 +0200
+++ b/src/Pure/Thy/state.scala	Tue Mar 30 12:47:39 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)))
                 }
diff -r fcd7bea01a93 -r 8b25e3b217bc src/Pure/build-jars
--- a/src/Pure/build-jars	Mon Mar 29 17:30:56 2010 +0200
+++ b/src/Pure/build-jars	Tue Mar 30 12:47:39 2010 +0200
@@ -88,7 +88,7 @@
   echo "###"
 
   rm -rf classes && mkdir classes
-  "$SCALA_HOME/bin/scalac" -unchecked -deprecation -d classes -target jvm-1.5 "${SOURCES[@]}" || \
+  "$SCALA_HOME/bin/scalac" -unchecked -deprecation -d classes -target:jvm-1.5 "${SOURCES[@]}" || \
     fail "Failed to compile sources"
   mkdir -p "$TARGET_DIR" || fail "Failed to create directory $TARGET_DIR"
   (
diff -r fcd7bea01a93 -r 8b25e3b217bc src/Tools/jEdit/README_BUILD
--- a/src/Tools/jEdit/README_BUILD	Mon Mar 29 17:30:56 2010 +0200
+++ b/src/Tools/jEdit/README_BUILD	Tue Mar 30 12:47:39 2010 +0200
@@ -5,10 +5,10 @@
 * Proper Java JRE/JDK from Sun, e.g. 1.6.0_18
   http://java.sun.com/javase/downloads/index.jsp
 
-* Netbeans 6.7.1
+* Netbeans 6.8
   http://www.netbeans.org/downloads/index.html
 
-* Scala for Netbeans: version 6.7v1 for NB 6.7
+* Scala for Netbeans: version 6.8v1.1
   http://sourceforge.net/project/showfiles.php?group_id=192439&package_id=256544
   http://blogtrader.net/dcaoyuan/category/NetBeans
   http://wiki.netbeans.org/Scala
@@ -19,6 +19,7 @@
   Netbeans Project "jEdit": install official sources as ./contrib/jEdit/.
 
 * jEdit plugins:
+  Netbeans Library "Console" = $HOME/.jedit/jars/Console.jar
   Netbeans Library "SideKick" = $HOME/.jedit/jars/SideKick.jar
   Netbeans Library "ErrorList" = $HOME/.jedit/jars/ErrorList.jar
   Netbeans Library "Hyperlinks" = $HOME/.jedit/jars/Hyperlinks.jar
diff -r fcd7bea01a93 -r 8b25e3b217bc src/Tools/jEdit/nbproject/build-impl.xml
--- a/src/Tools/jEdit/nbproject/build-impl.xml	Mon Mar 29 17:30:56 2010 +0200
+++ b/src/Tools/jEdit/nbproject/build-impl.xml	Tue Mar 30 12:47:39 2010 +0200
@@ -24,7 +24,7 @@
     <target depends="test,jar,javadoc" description="Build and test whole project." name="default"/>
     <!--
                 ======================
-                INITIALIZATION SECTION 
+                INITIALIZATION SECTION
                 ======================
             -->
     <target name="-pre-init">
@@ -40,9 +40,9 @@
             <isset property="env.SCALA_HOME"/>
         </condition>
         <fail unless="scala.home">
-You must set SCALA_HOME or environment property and append "-J-Dscala.home=scalahomepath"
-property to the end of "netbeans_default_options" in NetBeansInstallationPath/etc/netbeans.conf to point to
-Scala installation directory.
+                    You must set SCALA_HOME or environment property and append "-J-Dscala.home=scalahomepath"
+                    property to the end of "netbeans_default_options" in NetBeansInstallationPath/etc/netbeans.conf to point to
+                    Scala installation directory.
                 </fail>
         <property name="scala.compiler" value="${scala.home}/lib/scala-compiler.jar"/>
         <property name="scala.library" value="${scala.home}/lib/scala-library.jar"/>
@@ -53,14 +53,13 @@
                 <pathelement location="${scala.library}"/>
             </classpath>
         </taskdef>
-        <chmod dir="${scala.home}/bin" includes="**/*" perm="u+rx"/>
     </target>
     <target depends="-pre-init,-init-private" name="-init-user">
         <property file="${user.properties.file}"/>
         <!-- The two properties below are usually overridden -->
         <!-- by the active platform. Just a fallback. -->
-        <property name="default.javac.source" value="1.4"/>
-        <property name="default.javac.target" value="1.4"/>
+        <property name="default.javac.source" value="1.5"/>
+        <property name="default.javac.target" value="1.5"/>
     </target>
     <target depends="-pre-init,-init-private,-init-user" name="-init-project">
         <property file="nbproject/configs/${config}.properties"/>
@@ -126,6 +125,7 @@
         <property name="javadoc.encoding.used" value="${source.encoding}"/>
         <property name="includes" value="**"/>
         <property name="excludes" value=""/>
+        <property name="extdirs" value=" "/>
         <property name="do.depend" value="false"/>
         <condition property="do.depend.true">
             <istrue value="${do.depend}"/>
@@ -191,7 +191,13 @@
             <sequential>
                 <depend cache="${build.dir}/depcache" destdir="@{destdir}" excludes="${excludes}" includes="${includes}" srcdir="@{srcdir}">
                     <classpath>
-                        <path path="@{classpath}"/>
+                        <path>
+                            <pathelement path="@{classpath}"/>
+                            <fileset dir="${scala.lib}">
+                                <include name="**/*.jar"/>
+                            </fileset>
+                            <pathelement location="${build.classes.dir}"/>
+                        </path>
                     </classpath>
                 </depend>
             </sequential>
@@ -217,33 +223,25 @@
             <attribute default="${src.dir}" name="srcdir"/>
             <attribute default="${build.classes.dir}" name="destdir"/>
             <attribute default="${javac.classpath}" name="classpath"/>
+            <attribute default="${extdirs}" name="extdirs"/>
             <attribute default="${includes}" name="includes"/>
             <attribute default="${excludes}" name="excludes"/>
-            <attribute default="${javac.compilerargs}" name="addparams"/>
+            <attribute default="${scalac.compilerargs}" name="addparams"/>
             <attribute default="" name="sourcepath"/>
             <element name="customize" optional="true"/>
             <sequential>
-                <fsc addparams="@{addparams}" destdir="@{destdir}" encoding="${source.encoding}" excludes="@{excludes}" includes="@{includes}" sourcepath="@{sourcepath}" srcdir="@{srcdir}" target="jvm-${javac.target}">
+                <scalac addparams="-make:transitive -dependencyfile ${basedir}/${build.dir}/.scala_dependencies @{addparams}" deprecation="${scalac.deprecation}" destdir="@{destdir}" encoding="${source.encoding}" excludes="@{excludes}" extdirs="@{extdirs}" force="yes" fork="true" includes="@{includes}" sourcepath="@{sourcepath}" srcdir="@{srcdir}" target="jvm-${javac.target}" unchecked="${scalac.unchecked}">
                     <classpath>
-                        <path path="@{classpath}"/>
-                        <fileset dir="${scala.lib}">
-                            <include name="**/*.jar"/>
-                        </fileset>
+                        <path>
+                            <pathelement path="@{classpath}"/>
+                            <fileset dir="${scala.lib}">
+                                <include name="**/*.jar"/>
+                            </fileset>
+                            <pathelement location="${build.classes.dir}"/>
+                        </path>
                     </classpath>
                     <customize/>
-                </fsc>
-            </sequential>
-        </macrodef>
-        <macrodef name="depend" uri="http://www.netbeans.org/ns/scala-project/1">
-            <attribute default="${src.dir}" name="srcdir"/>
-            <attribute default="${build.classes.dir}" name="destdir"/>
-            <attribute default="${javac.classpath}" name="classpath"/>
-            <sequential>
-                <depend cache="${build.dir}/depcache" destdir="@{destdir}" excludes="${excludes}" includes="${includes}" srcdir="@{srcdir}">
-                    <classpath>
-                        <path path="@{classpath}"/>
-                    </classpath>
-                </depend>
+                </scalac>
             </sequential>
         </macrodef>
         <macrodef name="force-recompile" uri="http://www.netbeans.org/ns/scala-project/1">
@@ -551,14 +549,14 @@
             -->
     <target depends="init" name="-javadoc-build">
         <mkdir dir="${dist.javadoc.dir}"/>
-        <javadoc additionalparam="${javadoc.additionalparam}" author="${javadoc.author}" charset="UTF-8" destdir="${dist.javadoc.dir}" docencoding="UTF-8" encoding="${javadoc.encoding.used}" failonerror="true" noindex="${javadoc.noindex}" nonavbar="${javadoc.nonavbar}" notree="${javadoc.notree}" private="${javadoc.private}" source="${javac.source}" splitindex="${javadoc.splitindex}" use="${javadoc.use}" useexternalfile="true" version="${javadoc.version}" windowtitle="${javadoc.windowtitle}">
+        <scaladoc addparams="${javadoc.additionalparam}" deprecation="yes" destdir="${dist.javadoc.dir}" doctitle="${javadoc.windowtitle}" encoding="${javadoc.encoding.used}" srcdir="${src.dir}" unchecked="yes" windowtitle="${javadoc.windowtitle}">
             <classpath>
                 <path path="${javac.classpath}"/>
+                <fileset dir="${scala.lib}">
+                    <include name="**/*.jar"/>
+                </fileset>
             </classpath>
-            <fileset dir="${src.dir}" excludes="${excludes}" includes="${includes}">
-                <filename name="**/*.java"/>
-            </fileset>
-        </javadoc>
+        </scaladoc>
     </target>
     <target depends="init,-javadoc-build" if="netbeans.home" name="-javadoc-browse" unless="no.javadoc.preview">
         <nbbrowse file="${dist.javadoc.dir}/index.html"/>
@@ -580,7 +578,7 @@
         <scalaProject1:depend classpath="${javac.test.classpath}" destdir="${build.test.classes.dir}" srcdir=""/>
     </target>
     <target depends="init,compile,-pre-pre-compile-test,-pre-compile-test,-compile-test-depend" if="have.tests" name="-do-compile-test">
-        <scalaProject1:scalac classpath="${javac.test.classpath}" debug="true" destdir="${build.test.classes.dir}" srcdir=""/>
+        <scalaProject1:scalac classpath="${javac.test.classpath}" destdir="${build.test.classes.dir}" srcdir=""/>
         <copy todir="${build.test.classes.dir}"/>
     </target>
     <target name="-post-compile-test">
@@ -595,7 +593,7 @@
     <target depends="init,compile,-pre-pre-compile-test,-pre-compile-test-single" if="have.tests" name="-do-compile-test-single">
         <fail unless="javac.includes">Must select some files in the IDE or set javac.includes</fail>
         <scalaProject1:force-recompile destdir="${build.test.classes.dir}"/>
-        <scalaProject1:scalac classpath="${javac.test.classpath}" debug="true" destdir="${build.test.classes.dir}" excludes="" includes="${javac.includes}" sourcepath="" srcdir=""/>
+        <scalaProject1:scalac classpath="${javac.test.classpath}" destdir="${build.test.classes.dir}" excludes="" includes="${javac.includes}" sourcepath="" srcdir=""/>
         <copy todir="${build.test.classes.dir}"/>
     </target>
     <target name="-post-compile-test-single">
diff -r fcd7bea01a93 -r 8b25e3b217bc src/Tools/jEdit/nbproject/genfiles.properties
--- a/src/Tools/jEdit/nbproject/genfiles.properties	Mon Mar 29 17:30:56 2010 +0200
+++ b/src/Tools/jEdit/nbproject/genfiles.properties	Tue Mar 30 12:47:39 2010 +0200
@@ -4,5 +4,5 @@
 # This file is used by a NetBeans-based IDE to track changes in generated files such as build-impl.xml.
 # Do not edit this file. You may delete it but then the IDE will never regenerate such files for you.
 nbproject/build-impl.xml.data.CRC32=8f41dcce
-nbproject/build-impl.xml.script.CRC32=69f2059c
-nbproject/build-impl.xml.stylesheet.CRC32=bc42a706@1.3.0
+nbproject/build-impl.xml.script.CRC32=1c29c971
+nbproject/build-impl.xml.stylesheet.CRC32=8c3c03dd@1.3.4
diff -r fcd7bea01a93 -r 8b25e3b217bc src/Tools/jEdit/nbproject/project.properties
--- a/src/Tools/jEdit/nbproject/project.properties	Mon Mar 29 17:30:56 2010 +0200
+++ b/src/Tools/jEdit/nbproject/project.properties	Tue Mar 30 12:47:39 2010 +0200
@@ -75,3 +75,7 @@
     ${build.test.classes.dir}
 source.encoding=UTF-8
 src.dir=${file.reference.isabelle-jedit-src}
+scalac.compilerargs=
+scalac.deprecation=no
+scalac.unchecked=no
+
diff -r fcd7bea01a93 -r 8b25e3b217bc src/Tools/jEdit/src/jedit/document_model.scala
--- a/src/Tools/jEdit/src/jedit/document_model.scala	Mon Mar 29 17:30:56 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/document_model.scala	Tue Mar 30 12:47:39 2010 +0200
@@ -8,6 +8,8 @@
 package isabelle.jedit
 
 
+import isabelle._
+
 import scala.actors.Actor, Actor._
 import scala.collection.mutable
 
diff -r fcd7bea01a93 -r 8b25e3b217bc src/Tools/jEdit/src/jedit/document_view.scala
--- a/src/Tools/jEdit/src/jedit/document_view.scala	Mon Mar 29 17:30:56 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/document_view.scala	Tue Mar 30 12:47:39 2010 +0200
@@ -8,6 +8,8 @@
 package isabelle.jedit
 
 
+import isabelle._
+
 import scala.actors.Actor._
 
 import java.awt.event.{MouseAdapter, MouseEvent}
diff -r fcd7bea01a93 -r 8b25e3b217bc src/Tools/jEdit/src/jedit/html_panel.scala
--- a/src/Tools/jEdit/src/jedit/html_panel.scala	Mon Mar 29 17:30:56 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/html_panel.scala	Tue Mar 30 12:47:39 2010 +0200
@@ -7,6 +7,8 @@
 package isabelle.jedit
 
 
+import isabelle._
+
 import java.io.StringReader
 import java.awt.{BorderLayout, Dimension}
 import java.awt.event.MouseEvent
diff -r fcd7bea01a93 -r 8b25e3b217bc src/Tools/jEdit/src/jedit/isabelle_encoding.scala
--- a/src/Tools/jEdit/src/jedit/isabelle_encoding.scala	Mon Mar 29 17:30:56 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/isabelle_encoding.scala	Tue Mar 30 12:47:39 2010 +0200
@@ -7,14 +7,16 @@
 package isabelle.jedit
 
 
+import isabelle._
+
 import org.gjt.sp.jedit.io.Encoding
 import org.gjt.sp.jedit.buffer.JEditBuffer
 
-import java.nio.charset.{Charset, CharsetDecoder, CodingErrorAction}
+import java.nio.charset.{Charset, CodingErrorAction}
 import java.io.{InputStream, OutputStream, Reader, Writer, InputStreamReader, OutputStreamWriter,
   CharArrayReader, ByteArrayOutputStream}
 
-import scala.io.{Source, BufferedSource}
+import scala.io.{Codec, Source, BufferedSource}
 
 
 object Isabelle_Encoding
@@ -28,24 +30,23 @@
 class Isabelle_Encoding extends Encoding
 {
   private val charset = Charset.forName(Standard_System.charset)
-  private val BUFSIZE = 32768
+  val BUFSIZE = 32768
 
-  private def text_reader(in: InputStream, decoder: CharsetDecoder): Reader =
+  private def text_reader(in: InputStream, codec: Codec): Reader =
   {
-    def source(): Source =
-      BufferedSource.fromInputStream(in, decoder, BUFSIZE, { () => source() })
+    val source = new BufferedSource(in)(codec)
     new CharArrayReader(Isabelle.system.symbols.decode(source.mkString).toArray)
   }
 
 	override def getTextReader(in: InputStream): Reader =
-    text_reader(in, charset.newDecoder())
+    text_reader(in, Standard_System.codec())
 
 	override def getPermissiveTextReader(in: InputStream): Reader =
 	{
-		val decoder = charset.newDecoder()
-		decoder.onMalformedInput(CodingErrorAction.REPLACE)
-		decoder.onUnmappableCharacter(CodingErrorAction.REPLACE)
-		text_reader(in, decoder)
+		val codec = Standard_System.codec()
+		codec.onMalformedInput(CodingErrorAction.REPLACE)
+		codec.onUnmappableCharacter(CodingErrorAction.REPLACE)
+		text_reader(in, codec)
 	}
 
   override def getTextWriter(out: OutputStream): Writer =
diff -r fcd7bea01a93 -r 8b25e3b217bc src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala
--- a/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala	Mon Mar 29 17:30:56 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala	Tue Mar 30 12:47:39 2010 +0200
@@ -7,6 +7,8 @@
 package isabelle.jedit
 
 
+import isabelle._
+
 import java.io.File
 
 import gatchan.jedit.hyperlinks.{Hyperlink, HyperlinkSource, AbstractHyperlink}
diff -r fcd7bea01a93 -r 8b25e3b217bc src/Tools/jEdit/src/jedit/isabelle_sidekick.scala
--- a/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala	Mon Mar 29 17:30:56 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala	Tue Mar 30 12:47:39 2010 +0200
@@ -8,6 +8,8 @@
 package isabelle.jedit
 
 
+import isabelle._
+
 import scala.collection.Set
 import scala.collection.immutable.TreeSet
 
diff -r fcd7bea01a93 -r 8b25e3b217bc src/Tools/jEdit/src/jedit/output_dockable.scala
--- a/src/Tools/jEdit/src/jedit/output_dockable.scala	Mon Mar 29 17:30:56 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/output_dockable.scala	Tue Mar 30 12:47:39 2010 +0200
@@ -7,6 +7,8 @@
 package isabelle.jedit
 
 
+import isabelle._
+
 import scala.actors.Actor._
 
 import javax.swing.JPanel
diff -r fcd7bea01a93 -r 8b25e3b217bc src/Tools/jEdit/src/jedit/plugin.scala
--- a/src/Tools/jEdit/src/jedit/plugin.scala	Mon Mar 29 17:30:56 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/plugin.scala	Tue Mar 30 12:47:39 2010 +0200
@@ -9,6 +9,8 @@
 package isabelle.jedit
 
 
+import isabelle._
+
 import java.io.{FileInputStream, IOException}
 import java.awt.Font
 import javax.swing.JTextArea
diff -r fcd7bea01a93 -r 8b25e3b217bc src/Tools/jEdit/src/jedit/protocol_dockable.scala
--- a/src/Tools/jEdit/src/jedit/protocol_dockable.scala	Mon Mar 29 17:30:56 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/protocol_dockable.scala	Tue Mar 30 12:47:39 2010 +0200
@@ -7,6 +7,8 @@
 package isabelle.jedit
 
 
+import isabelle._
+
 import scala.actors.Actor._
 
 import java.awt.{Dimension, Graphics, BorderLayout}
diff -r fcd7bea01a93 -r 8b25e3b217bc src/Tools/jEdit/src/jedit/scala_console.scala
--- a/src/Tools/jEdit/src/jedit/scala_console.scala	Mon Mar 29 17:30:56 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/scala_console.scala	Tue Mar 30 12:47:39 2010 +0200
@@ -7,6 +7,8 @@
 package isabelle.jedit
 
 
+import isabelle._
+
 import console.{Console, ConsolePane, Shell, Output}
 
 import org.gjt.sp.jedit.{jEdit, JARClassLoader}
@@ -63,7 +65,7 @@
 
     def write(cbuf: Array[Char], off: Int, len: Int)
     {
-      if (len > 0) write(new String(cbuf.subArray(off, off + len)))
+      if (len > 0) write(new String(cbuf.slice(off, off + len)))
     }
 
     override def write(str: String)