merged
authorwenzelm
Tue Mar 30 12:47:39 2010 +0200 (2010-03-30)
changeset 360418b25e3b217bc
parent 36040 fcd7bea01a93
parent 36016 4f5c7a19ebe0
child 36042 85efdadee8ae
merged
     1.1 --- a/src/Pure/General/linear_set.scala	Mon Mar 29 17:30:56 2010 +0200
     1.2 +++ b/src/Pure/General/linear_set.scala	Tue Mar 30 12:47:39 2010 +0200
     1.3 @@ -7,27 +7,36 @@
     1.4  
     1.5  package isabelle
     1.6  
     1.7 +import scala.collection.SetLike
     1.8 +import scala.collection.generic.{SetFactory, CanBuildFrom, GenericSetTemplate, GenericCompanion}
     1.9  
    1.10 -object Linear_Set
    1.11 +
    1.12 +object Linear_Set extends SetFactory[Linear_Set]
    1.13  {
    1.14    private case class Rep[A](
    1.15 -    val first: Option[A], val last: Option[A], val nexts: Map[A, A], prevs: Map[A, A])
    1.16 +    val start: Option[A], val end: Option[A], val nexts: Map[A, A], prevs: Map[A, A])
    1.17  
    1.18    private def empty_rep[A] = Rep[A](None, None, Map(), Map())
    1.19  
    1.20 -  private def make[A](first: Option[A], last: Option[A], nexts: Map[A, A], prevs: Map[A, A])
    1.21 -    : Linear_Set[A] = new Linear_Set[A] { override val rep = Rep(first, last, nexts, prevs) }
    1.22 +  private def make[A](start: Option[A], end: Option[A], nexts: Map[A, A], prevs: Map[A, A])
    1.23 +    : Linear_Set[A] = new Linear_Set[A] { override val rep = Rep(start, end, nexts, prevs) }
    1.24  
    1.25 -  def empty[A]: Linear_Set[A] = new Linear_Set
    1.26 -  def apply[A](elems: A*): Linear_Set[A] = empty[A] ++ elems
    1.27 +  implicit def canBuildFrom[A]: CanBuildFrom[Coll, A, Linear_Set[A]] = setCanBuildFrom[A]
    1.28 +  override def empty[A] = new Linear_Set[A]
    1.29  
    1.30    class Duplicate(s: String) extends Exception(s)
    1.31    class Undefined(s: String) extends Exception(s)
    1.32  }
    1.33  
    1.34  
    1.35 -class Linear_Set[A] extends scala.collection.immutable.Set[A]
    1.36 +class Linear_Set[A]
    1.37 +  extends scala.collection.immutable.Set[A]
    1.38 +  with GenericSetTemplate[A, Linear_Set]
    1.39 +  with SetLike[A, Linear_Set[A]]
    1.40  {
    1.41 +  override def companion: GenericCompanion[Linear_Set] = Linear_Set
    1.42 +
    1.43 +
    1.44    /* representation */
    1.45  
    1.46    protected val rep = Linear_Set.empty_rep[A]
    1.47 @@ -43,10 +52,10 @@
    1.48      else
    1.49        hook match {
    1.50          case None =>
    1.51 -          rep.first match {
    1.52 +          rep.start match {
    1.53              case None => Linear_Set.make(Some(elem), Some(elem), Map(), Map())
    1.54              case Some(elem1) =>
    1.55 -              Linear_Set.make(Some(elem), rep.last,
    1.56 +              Linear_Set.make(Some(elem), rep.end,
    1.57                  rep.nexts + (elem -> elem1), rep.prevs + (elem1 -> elem))
    1.58            }
    1.59          case Some(elem1) =>
    1.60 @@ -54,10 +63,10 @@
    1.61            else
    1.62              rep.nexts.get(elem1) match {
    1.63                case None =>
    1.64 -                Linear_Set.make(rep.first, Some(elem),
    1.65 +                Linear_Set.make(rep.start, Some(elem),
    1.66                    rep.nexts + (elem1 -> elem), rep.prevs + (elem -> elem1))
    1.67                case Some(elem2) =>
    1.68 -                Linear_Set.make(rep.first, rep.last,
    1.69 +                Linear_Set.make(rep.start, rep.end,
    1.70                    rep.nexts + (elem1 -> elem) + (elem -> elem2),
    1.71                    rep.prevs + (elem2 -> elem) + (elem -> elem1))
    1.72              }
    1.73 @@ -66,13 +75,13 @@
    1.74    def delete_after(hook: Option[A]): Linear_Set[A] =
    1.75      hook match {
    1.76        case None =>
    1.77 -        rep.first match {
    1.78 +        rep.start match {
    1.79            case None => throw new Linear_Set.Undefined("")
    1.80            case Some(elem1) =>
    1.81              rep.nexts.get(elem1) match {
    1.82                case None => empty
    1.83                case Some(elem2) =>
    1.84 -                Linear_Set.make(Some(elem2), rep.last, rep.nexts - elem1, rep.prevs - elem2)
    1.85 +                Linear_Set.make(Some(elem2), rep.end, rep.nexts - elem1, rep.prevs - elem2)
    1.86              }
    1.87          }
    1.88        case Some(elem1) =>
    1.89 @@ -83,9 +92,9 @@
    1.90              case Some(elem2) =>
    1.91                rep.nexts.get(elem2) match {
    1.92                  case None =>
    1.93 -                  Linear_Set.make(rep.first, Some(elem1), rep.nexts - elem1, rep.prevs - elem2)
    1.94 +                  Linear_Set.make(rep.start, Some(elem1), rep.nexts - elem1, rep.prevs - elem2)
    1.95                  case Some(elem3) =>
    1.96 -                  Linear_Set.make(rep.first, rep.last,
    1.97 +                  Linear_Set.make(rep.start, rep.end,
    1.98                      rep.nexts - elem2 + (elem1 -> elem3),
    1.99                      rep.prevs - elem2 + (elem3 -> elem1))
   1.100                }
   1.101 @@ -100,8 +109,8 @@
   1.102      if (isEmpty) this
   1.103      else {
   1.104        val next =
   1.105 -        if (from == rep.last) None
   1.106 -        else if (from == None) rep.first
   1.107 +        if (from == rep.end) None
   1.108 +        else if (from == None) rep.start
   1.109          else from.map(rep.nexts(_))
   1.110        if (next == to) this
   1.111        else delete_after(from).delete_between(from, to)
   1.112 @@ -113,15 +122,13 @@
   1.113  
   1.114    override def stringPrefix = "Linear_Set"
   1.115  
   1.116 -  def empty[B]: Linear_Set[B] = Linear_Set.empty
   1.117 -
   1.118 -  override def isEmpty: Boolean = !rep.first.isDefined
   1.119 -  def size: Int = if (isEmpty) 0 else rep.nexts.size + 1
   1.120 +  override def isEmpty: Boolean = !rep.start.isDefined
   1.121 +  override def size: Int = if (isEmpty) 0 else rep.nexts.size + 1
   1.122  
   1.123    def contains(elem: A): Boolean =
   1.124 -    !isEmpty && (rep.last.get == elem || rep.nexts.isDefinedAt(elem))
   1.125 +    !isEmpty && (rep.end.get == elem || rep.nexts.isDefinedAt(elem))
   1.126  
   1.127 -  private def elements_from(start: Option[A]): Iterator[A] = new Iterator[A] {
   1.128 +  private def iterator_from(start: Option[A]): Iterator[A] = new Iterator[A] {
   1.129      private var next_elem = start
   1.130      def hasNext = next_elem.isDefined
   1.131      def next =
   1.132 @@ -133,18 +140,13 @@
   1.133        }
   1.134    }
   1.135  
   1.136 -  def elements: Iterator[A] = elements_from(rep.first)
   1.137 +  override def iterator: Iterator[A] = iterator_from(rep.start)
   1.138  
   1.139 -  def elements(elem: A): Iterator[A] =
   1.140 -    if (contains(elem)) elements_from(Some(elem))
   1.141 +  def iterator(elem: A): Iterator[A] =
   1.142 +    if (contains(elem)) iterator_from(Some(elem))
   1.143      else throw new Linear_Set.Undefined(elem.toString)
   1.144  
   1.145 -  def + (elem: A): Linear_Set[A] = insert_after(rep.last, elem)
   1.146 -
   1.147 -  override def + (elem1: A, elem2: A, elems: A*): Linear_Set[A] =
   1.148 -    this + elem1 + elem2 ++ elems
   1.149 -  override def ++ (elems: Iterable[A]): Linear_Set[A] = (this /: elems) ((s, elem) => s + elem)
   1.150 -  override def ++ (elems: Iterator[A]): Linear_Set[A] = (this /: elems) ((s, elem) => s + elem)
   1.151 +  def + (elem: A): Linear_Set[A] = insert_after(rep.end, elem)
   1.152  
   1.153    def - (elem: A): Linear_Set[A] =
   1.154      if (!contains(elem)) throw new Linear_Set.Undefined(elem.toString)
     2.1 --- a/src/Pure/General/scan.scala	Mon Mar 29 17:30:56 2010 +0200
     2.2 +++ b/src/Pure/General/scan.scala	Tue Mar 30 12:47:39 2010 +0200
     2.3 @@ -7,6 +7,7 @@
     2.4  package isabelle
     2.5  
     2.6  
     2.7 +import scala.collection.generic.Addable
     2.8  import scala.collection.immutable.PagedSeq
     2.9  import scala.util.parsing.input.{OffsetPosition, Position => InputPosition, Reader}
    2.10  import scala.util.parsing.combinator.RegexParsers
    2.11 @@ -27,7 +28,7 @@
    2.12      def apply(elems: String*): Lexicon = empty ++ elems
    2.13    }
    2.14  
    2.15 -  class Lexicon extends scala.collection.Set[String] with RegexParsers
    2.16 +  class Lexicon extends Addable[String, Lexicon] with RegexParsers
    2.17    {
    2.18      /* representation */
    2.19  
    2.20 @@ -65,14 +66,14 @@
    2.21        }
    2.22  
    2.23  
    2.24 -    /* Set methods */
    2.25 +    /* pseudo Set methods */
    2.26  
    2.27 -    override def stringPrefix = "Lexicon"
    2.28 +    def iterator: Iterator[String] = content(main_tree, Nil).sortWith(_ <= _).iterator
    2.29  
    2.30 -    override def isEmpty: Boolean = { main_tree.branches.isEmpty }
    2.31 +    override def toString: String = iterator.mkString("Lexicon(", ", ", ")")
    2.32  
    2.33 -    def size: Int = content(main_tree, Nil).length
    2.34 -    def elements: Iterator[String] = content(main_tree, Nil).sort(_ <= _).elements
    2.35 +    def empty: Lexicon = Lexicon.empty
    2.36 +    def isEmpty: Boolean = main_tree.branches.isEmpty
    2.37  
    2.38      def contains(elem: String): Boolean =
    2.39        lookup(elem) match {
    2.40 @@ -80,6 +81,11 @@
    2.41          case _ => false
    2.42        }
    2.43  
    2.44 +
    2.45 +    /* Addable methods */
    2.46 +
    2.47 +    def repr = this
    2.48 +
    2.49      def + (elem: String): Lexicon =
    2.50        if (contains(elem)) this
    2.51        else {
    2.52 @@ -102,11 +108,6 @@
    2.53          new Lexicon { override val main_tree = extend(old.main_tree, 0) }
    2.54        }
    2.55  
    2.56 -    def + (elem1: String, elem2: String, elems: String*): Lexicon =
    2.57 -      this + elem1 + elem2 ++ elems
    2.58 -    def ++ (elems: Iterable[String]): Lexicon = (this /: elems) ((s, elem) => s + elem)
    2.59 -    def ++ (elems: Iterator[String]): Lexicon = (this /: elems) ((s, elem) => s + elem)
    2.60 -
    2.61  
    2.62  
    2.63      /** RegexParsers methods **/
     3.1 --- a/src/Pure/General/symbol.scala	Mon Mar 29 17:30:56 2010 +0200
     3.2 +++ b/src/Pure/General/symbol.scala	Tue Mar 30 12:47:39 2010 +0200
     3.3 @@ -7,7 +7,7 @@
     3.4  package isabelle
     3.5  
     3.6  import scala.io.Source
     3.7 -import scala.collection.{jcl, mutable}
     3.8 +import scala.collection.mutable
     3.9  import scala.util.matching.Regex
    3.10  
    3.11  
    3.12 @@ -54,9 +54,9 @@
    3.13    }
    3.14  
    3.15  
    3.16 -  /* elements */
    3.17 +  /* iterator */
    3.18  
    3.19 -  def elements(text: CharSequence) = new Iterator[CharSequence]
    3.20 +  def iterator(text: CharSequence) = new Iterator[CharSequence]
    3.21    {
    3.22      private val matcher = new Matcher(text)
    3.23      private var i = 0
    3.24 @@ -124,12 +124,7 @@
    3.25        }
    3.26        (min, max)
    3.27      }
    3.28 -    private val table =
    3.29 -    {
    3.30 -      val table = new jcl.HashMap[String, String]   // reasonably efficient?
    3.31 -      for ((x, y) <- list) table + (x -> y)
    3.32 -      table
    3.33 -    }
    3.34 +    private val table = Map[String, String]() ++ list
    3.35      def recode(text: String): String =
    3.36      {
    3.37        val len = text.length
     4.1 --- a/src/Pure/General/xml.scala	Mon Mar 29 17:30:56 2010 +0200
     4.2 +++ b/src/Pure/General/xml.scala	Tue Mar 30 12:47:39 2010 +0200
     4.3 @@ -34,34 +34,34 @@
     4.4    /* string representation */
     4.5  
     4.6    private def append_text(text: String, s: StringBuilder) {
     4.7 -    if (text == null) s ++ text
     4.8 +    if (text == null) s ++= text
     4.9      else {
    4.10 -      for (c <- text.elements) c match {
    4.11 -        case '<' => s ++ "&lt;"
    4.12 -        case '>' => s ++ "&gt;"
    4.13 -        case '&' => s ++ "&amp;"
    4.14 -        case '"' => s ++ "&quot;"
    4.15 -        case '\'' => s ++ "&apos;"
    4.16 -        case _ => s + c
    4.17 +      for (c <- text.iterator) c match {
    4.18 +        case '<' => s ++= "&lt;"
    4.19 +        case '>' => s ++= "&gt;"
    4.20 +        case '&' => s ++= "&amp;"
    4.21 +        case '"' => s ++= "&quot;"
    4.22 +        case '\'' => s ++= "&apos;"
    4.23 +        case _ => s += c
    4.24        }
    4.25      }
    4.26    }
    4.27  
    4.28    private def append_elem(name: String, atts: Attributes, s: StringBuilder) {
    4.29 -    s ++ name
    4.30 +    s ++= name
    4.31      for ((a, x) <- atts) {
    4.32 -      s ++ " "; s ++ a; s ++ "=\""; append_text(x, s); s ++ "\""
    4.33 +      s ++= " "; s ++= a; s ++= "=\""; append_text(x, s); s ++= "\""
    4.34      }
    4.35    }
    4.36  
    4.37    private def append_tree(tree: Tree, s: StringBuilder) {
    4.38      tree match {
    4.39        case Elem(name, atts, Nil) =>
    4.40 -        s ++ "<"; append_elem(name, atts, s); s ++ "/>"
    4.41 +        s ++= "<"; append_elem(name, atts, s); s ++= "/>"
    4.42        case Elem(name, atts, ts) =>
    4.43 -        s ++ "<"; append_elem(name, atts, s); s ++ ">"
    4.44 +        s ++= "<"; append_elem(name, atts, s); s ++= ">"
    4.45          for (t <- ts) append_tree(t, s)
    4.46 -        s ++ "</"; s ++ name; s ++ ">"
    4.47 +        s ++= "</"; s ++= name; s ++= ">"
    4.48        case Text(text) => append_text(text, s)
    4.49      }
    4.50    }
     5.1 --- a/src/Pure/System/isabelle_syntax.scala	Mon Mar 29 17:30:56 2010 +0200
     5.2 +++ b/src/Pure/System/isabelle_syntax.scala	Tue Mar 30 12:47:39 2010 +0200
     5.3 @@ -40,7 +40,7 @@
     5.4      result: StringBuilder)
     5.5    {
     5.6      result.append("(")
     5.7 -    val elems = body.elements
     5.8 +    val elems = body.iterator
     5.9      if (elems.hasNext) append_elem(elems.next, result)
    5.10      while (elems.hasNext) {
    5.11        result.append(", ")
     6.1 --- a/src/Pure/System/isabelle_system.scala	Mon Mar 29 17:30:56 2010 +0200
     6.2 +++ b/src/Pure/System/isabelle_system.scala	Tue Mar 30 12:47:39 2010 +0200
     6.3 @@ -24,7 +24,7 @@
     6.4  
     6.5    private val environment: Map[String, String] =
     6.6    {
     6.7 -    import scala.collection.jcl.Conversions._
     6.8 +    import scala.collection.JavaConversions._
     6.9  
    6.10      val env0 = Map(java.lang.System.getenv.toList: _*)
    6.11  
    6.12 @@ -288,7 +288,7 @@
    6.13          for (file <- files if file.isFile) logics += file.getName
    6.14        }
    6.15      }
    6.16 -    logics.toList.sort(_ < _)
    6.17 +    logics.toList.sortWith(_ < _)
    6.18    }
    6.19  
    6.20  
    6.21 @@ -297,7 +297,7 @@
    6.22    private def read_symbols(path: String): List[String] =
    6.23    {
    6.24      val file = platform_file(path)
    6.25 -    if (file.isFile) Source.fromFile(file).getLines.toList
    6.26 +    if (file.isFile) Source.fromFile(file).getLines().toList
    6.27      else Nil
    6.28    }
    6.29    val symbols = new Symbol.Interpretation(
     7.1 --- a/src/Pure/System/standard_system.scala	Mon Mar 29 17:30:56 2010 +0200
     7.2 +++ b/src/Pure/System/standard_system.scala	Tue Mar 30 12:47:39 2010 +0200
     7.3 @@ -12,7 +12,7 @@
     7.4    BufferedInputStream, FileInputStream, BufferedReader, InputStreamReader,
     7.5    File, FileFilter, IOException}
     7.6  
     7.7 -import scala.io.Source
     7.8 +import scala.io.{Source, Codec}
     7.9  import scala.util.matching.Regex
    7.10  import scala.collection.mutable
    7.11  
    7.12 @@ -20,6 +20,7 @@
    7.13  object Standard_System
    7.14  {
    7.15    val charset = "UTF-8"
    7.16 +  def codec(): Codec = Codec(charset)
    7.17  
    7.18  
    7.19    /* permissive UTF-8 decoding */
    7.20 @@ -135,7 +136,7 @@
    7.21    def process_output(proc: Process): (String, Int) =
    7.22    {
    7.23      proc.getOutputStream.close
    7.24 -    val output = Source.fromInputStream(proc.getInputStream, charset).mkString  // FIXME
    7.25 +    val output = Source.fromInputStream(proc.getInputStream)(codec()).mkString  // FIXME
    7.26      val rc =
    7.27        try { proc.waitFor }
    7.28        finally {
     8.1 --- a/src/Pure/Thy/command.scala	Mon Mar 29 17:30:56 2010 +0200
     8.2 +++ b/src/Pure/Thy/command.scala	Tue Mar 30 12:47:39 2010 +0200
     8.3 @@ -35,11 +35,11 @@
     8.4  {
     8.5    /* classification */
     8.6  
     8.7 -  def is_command: Boolean = !span.isEmpty && span.first.is_command
     8.8 +  def is_command: Boolean = !span.isEmpty && span.head.is_command
     8.9    def is_ignored: Boolean = span.forall(_.is_ignored)
    8.10    def is_malformed: Boolean = !is_command && !is_ignored
    8.11  
    8.12 -  def name: String = if (is_command) span.first.content else ""
    8.13 +  def name: String = if (is_command) span.head.content else ""
    8.14    override def toString = if (is_command) name else if (is_ignored) "<ignored>" else "<malformed>"
    8.15  
    8.16  
     9.1 --- a/src/Pure/Thy/completion.scala	Mon Mar 29 17:30:56 2010 +0200
     9.2 +++ b/src/Pure/Thy/completion.scala	Tue Mar 30 12:47:39 2010 +0200
     9.3 @@ -94,7 +94,7 @@
     9.4            case Some(word) =>
     9.5              words_lex.completions(word).map(words_map(_)) match {
     9.6                case Nil => None
     9.7 -              case cs => Some(word, cs.sort(_ < _))
     9.8 +              case cs => Some(word, cs.sortWith(_ < _))
     9.9              }
    9.10            case None => None
    9.11          }
    10.1 --- a/src/Pure/Thy/document.scala	Mon Mar 29 17:30:56 2010 +0200
    10.2 +++ b/src/Pure/Thy/document.scala	Tue Mar 30 12:47:39 2010 +0200
    10.3 @@ -14,7 +14,7 @@
    10.4    def command_starts(commands: Linear_Set[Command]): Iterator[(Command, Int)] =
    10.5    {
    10.6      var offset = 0
    10.7 -    for (cmd <- commands.elements) yield {
    10.8 +    for (cmd <- commands.iterator) yield {
    10.9        val start = offset
   10.10        offset += cmd.length
   10.11        (cmd, start)
   10.12 @@ -92,17 +92,17 @@
   10.13      def parse_spans(commands: Linear_Set[Command]): Linear_Set[Command] =
   10.14      {
   10.15        // FIXME relative search!
   10.16 -      commands.elements.find(is_unparsed) match {
   10.17 +      commands.iterator.find(is_unparsed) match {
   10.18          case Some(first_unparsed) =>
   10.19            val prefix = commands.prev(first_unparsed)
   10.20 -          val body = commands.elements(first_unparsed).takeWhile(is_unparsed).toList
   10.21 +          val body = commands.iterator(first_unparsed).takeWhile(is_unparsed).toList
   10.22            val suffix = commands.next(body.last)
   10.23  
   10.24            val sources = (prefix.toList ::: body ::: suffix.toList).flatMap(_.span.map(_.source))
   10.25            val spans0 = Thy_Syntax.parse_spans(session.current_syntax.scan(sources.mkString))
   10.26  
   10.27            val (before_edit, spans1) =
   10.28 -            if (!spans0.isEmpty && Some(spans0.first) == prefix.map(_.span))
   10.29 +            if (!spans0.isEmpty && Some(spans0.head) == prefix.map(_.span))
   10.30                (prefix, spans0.tail)
   10.31              else (if (prefix.isDefined) commands.prev(prefix.get) else None, spans0)
   10.32  
   10.33 @@ -128,8 +128,8 @@
   10.34        val commands1 = Library.timeit("edit_text") { edit_text(edits, commands0) }
   10.35        val commands2 = Library.timeit("parse_spans") { parse_spans(commands1) }
   10.36  
   10.37 -      val removed_commands = commands0.elements.filter(!commands2.contains(_)).toList
   10.38 -      val inserted_commands = commands2.elements.filter(!commands0.contains(_)).toList
   10.39 +      val removed_commands = commands0.iterator.filter(!commands2.contains(_)).toList
   10.40 +      val inserted_commands = commands2.iterator.filter(!commands0.contains(_)).toList
   10.41  
   10.42        val doc_edits =
   10.43          removed_commands.reverse.map(cmd => (commands0.prev(cmd), None)) :::
    11.1 --- a/src/Pure/Thy/html.scala	Mon Mar 29 17:30:56 2010 +0200
    11.2 +++ b/src/Pure/Thy/html.scala	Tue Mar 30 12:47:39 2010 +0200
    11.3 @@ -41,29 +41,29 @@
    11.4          val t = new StringBuilder
    11.5          def flush() {
    11.6            if (!t.isEmpty) {
    11.7 -            ts + XML.Text(t.toString)
    11.8 +            ts += XML.Text(t.toString)
    11.9              t.clear
   11.10            }
   11.11          }
   11.12          def add(elem: XML.Tree) {
   11.13            flush()
   11.14 -          ts + elem
   11.15 +          ts += elem
   11.16          }
   11.17 -        val syms = Symbol.elements(txt).map(_.toString)
   11.18 +        val syms = Symbol.iterator(txt).map(_.toString)
   11.19          while (syms.hasNext) {
   11.20            val s1 = syms.next
   11.21            def s2() = if (syms.hasNext) syms.next else ""
   11.22            s1 match {
   11.23              case "\n" => add(XML.elem(BR))
   11.24 -            case "\\<^bsub>" => t ++ s1  // FIXME
   11.25 -            case "\\<^esub>" => t ++ s1  // FIXME
   11.26 -            case "\\<^bsup>" => t ++ s1  // FIXME
   11.27 -            case "\\<^esup>" => t ++ s1  // FIXME
   11.28 +            case "\\<^bsub>" => t ++= s1  // FIXME
   11.29 +            case "\\<^esub>" => t ++= s1  // FIXME
   11.30 +            case "\\<^bsup>" => t ++= s1  // FIXME
   11.31 +            case "\\<^esup>" => t ++= s1  // FIXME
   11.32              case "\\<^sub>" | "\\<^isub>" => add(hidden(s1)); add(sub(s2()))
   11.33              case "\\<^sup>" | "\\<^isup>" => add(hidden(s1)); add(sup(s2()))
   11.34              case "\\<^bold>" => add(hidden(s1)); add(span("bold", List(XML.Text(s2()))))
   11.35              case "\\<^loc>" => add(hidden(s1)); add(span("loc", List(XML.Text(s2()))))
   11.36 -            case _ => t ++ s1
   11.37 +            case _ => t ++= s1
   11.38            }
   11.39          }
   11.40          flush()
    12.1 --- a/src/Pure/Thy/markup_node.scala	Mon Mar 29 17:30:56 2010 +0200
    12.2 +++ b/src/Pure/Thy/markup_node.scala	Tue Mar 30 12:47:39 2010 +0200
    12.3 @@ -24,7 +24,7 @@
    12.4    def set_branches(bs: List[Markup_Tree]): Markup_Tree = new Markup_Tree(node, bs)
    12.5  
    12.6    private def add(branch: Markup_Tree) =   // FIXME avoid sort
    12.7 -    set_branches((branch :: branches) sort ((a, b) => a.node.start < b.node.start))
    12.8 +    set_branches((branch :: branches).sortWith((a, b) => a.node.start < b.node.start))
    12.9  
   12.10    private def remove(bs: List[Markup_Tree]) = set_branches(branches -- bs)
   12.11  
   12.12 @@ -70,7 +70,7 @@
   12.13            markup <- markups
   12.14          } yield markup
   12.15        if (next_x < node.stop)
   12.16 -        filled_gaps + new Markup_Node(next_x, node.stop, node.info)
   12.17 +        filled_gaps ::: List(new Markup_Node(next_x, node.stop, node.info))
   12.18        else filled_gaps
   12.19      }
   12.20    }
    13.1 --- a/src/Pure/Thy/state.scala	Mon Mar 29 17:30:56 2010 +0200
    13.2 +++ b/src/Pure/Thy/state.scala	Tue Mar 30 12:47:39 2010 +0200
    13.3 @@ -84,7 +84,7 @@
    13.4                  val (begin, end) = Position.get_offsets(atts)
    13.5                  if (begin.isEmpty || end.isEmpty) state
    13.6                  else if (kind == Markup.ML_TYPING) {
    13.7 -                  val info = body.first.asInstanceOf[XML.Text].content   // FIXME proper match!?
    13.8 +                  val info = body.head.asInstanceOf[XML.Text].content   // FIXME proper match!?
    13.9                    state.add_markup(
   13.10                      command.markup_node(begin.get - 1, end.get - 1, Command.TypeInfo(info)))
   13.11                  }
    14.1 --- a/src/Pure/build-jars	Mon Mar 29 17:30:56 2010 +0200
    14.2 +++ b/src/Pure/build-jars	Tue Mar 30 12:47:39 2010 +0200
    14.3 @@ -88,7 +88,7 @@
    14.4    echo "###"
    14.5  
    14.6    rm -rf classes && mkdir classes
    14.7 -  "$SCALA_HOME/bin/scalac" -unchecked -deprecation -d classes -target jvm-1.5 "${SOURCES[@]}" || \
    14.8 +  "$SCALA_HOME/bin/scalac" -unchecked -deprecation -d classes -target:jvm-1.5 "${SOURCES[@]}" || \
    14.9      fail "Failed to compile sources"
   14.10    mkdir -p "$TARGET_DIR" || fail "Failed to create directory $TARGET_DIR"
   14.11    (
    15.1 --- a/src/Tools/jEdit/README_BUILD	Mon Mar 29 17:30:56 2010 +0200
    15.2 +++ b/src/Tools/jEdit/README_BUILD	Tue Mar 30 12:47:39 2010 +0200
    15.3 @@ -5,10 +5,10 @@
    15.4  * Proper Java JRE/JDK from Sun, e.g. 1.6.0_18
    15.5    http://java.sun.com/javase/downloads/index.jsp
    15.6  
    15.7 -* Netbeans 6.7.1
    15.8 +* Netbeans 6.8
    15.9    http://www.netbeans.org/downloads/index.html
   15.10  
   15.11 -* Scala for Netbeans: version 6.7v1 for NB 6.7
   15.12 +* Scala for Netbeans: version 6.8v1.1
   15.13    http://sourceforge.net/project/showfiles.php?group_id=192439&package_id=256544
   15.14    http://blogtrader.net/dcaoyuan/category/NetBeans
   15.15    http://wiki.netbeans.org/Scala
   15.16 @@ -19,6 +19,7 @@
   15.17    Netbeans Project "jEdit": install official sources as ./contrib/jEdit/.
   15.18  
   15.19  * jEdit plugins:
   15.20 +  Netbeans Library "Console" = $HOME/.jedit/jars/Console.jar
   15.21    Netbeans Library "SideKick" = $HOME/.jedit/jars/SideKick.jar
   15.22    Netbeans Library "ErrorList" = $HOME/.jedit/jars/ErrorList.jar
   15.23    Netbeans Library "Hyperlinks" = $HOME/.jedit/jars/Hyperlinks.jar
    16.1 --- a/src/Tools/jEdit/nbproject/build-impl.xml	Mon Mar 29 17:30:56 2010 +0200
    16.2 +++ b/src/Tools/jEdit/nbproject/build-impl.xml	Tue Mar 30 12:47:39 2010 +0200
    16.3 @@ -24,7 +24,7 @@
    16.4      <target depends="test,jar,javadoc" description="Build and test whole project." name="default"/>
    16.5      <!--
    16.6                  ======================
    16.7 -                INITIALIZATION SECTION 
    16.8 +                INITIALIZATION SECTION
    16.9                  ======================
   16.10              -->
   16.11      <target name="-pre-init">
   16.12 @@ -40,9 +40,9 @@
   16.13              <isset property="env.SCALA_HOME"/>
   16.14          </condition>
   16.15          <fail unless="scala.home">
   16.16 -You must set SCALA_HOME or environment property and append "-J-Dscala.home=scalahomepath"
   16.17 -property to the end of "netbeans_default_options" in NetBeansInstallationPath/etc/netbeans.conf to point to
   16.18 -Scala installation directory.
   16.19 +                    You must set SCALA_HOME or environment property and append "-J-Dscala.home=scalahomepath"
   16.20 +                    property to the end of "netbeans_default_options" in NetBeansInstallationPath/etc/netbeans.conf to point to
   16.21 +                    Scala installation directory.
   16.22                  </fail>
   16.23          <property name="scala.compiler" value="${scala.home}/lib/scala-compiler.jar"/>
   16.24          <property name="scala.library" value="${scala.home}/lib/scala-library.jar"/>
   16.25 @@ -53,14 +53,13 @@
   16.26                  <pathelement location="${scala.library}"/>
   16.27              </classpath>
   16.28          </taskdef>
   16.29 -        <chmod dir="${scala.home}/bin" includes="**/*" perm="u+rx"/>
   16.30      </target>
   16.31      <target depends="-pre-init,-init-private" name="-init-user">
   16.32          <property file="${user.properties.file}"/>
   16.33          <!-- The two properties below are usually overridden -->
   16.34          <!-- by the active platform. Just a fallback. -->
   16.35 -        <property name="default.javac.source" value="1.4"/>
   16.36 -        <property name="default.javac.target" value="1.4"/>
   16.37 +        <property name="default.javac.source" value="1.5"/>
   16.38 +        <property name="default.javac.target" value="1.5"/>
   16.39      </target>
   16.40      <target depends="-pre-init,-init-private,-init-user" name="-init-project">
   16.41          <property file="nbproject/configs/${config}.properties"/>
   16.42 @@ -126,6 +125,7 @@
   16.43          <property name="javadoc.encoding.used" value="${source.encoding}"/>
   16.44          <property name="includes" value="**"/>
   16.45          <property name="excludes" value=""/>
   16.46 +        <property name="extdirs" value=" "/>
   16.47          <property name="do.depend" value="false"/>
   16.48          <condition property="do.depend.true">
   16.49              <istrue value="${do.depend}"/>
   16.50 @@ -191,7 +191,13 @@
   16.51              <sequential>
   16.52                  <depend cache="${build.dir}/depcache" destdir="@{destdir}" excludes="${excludes}" includes="${includes}" srcdir="@{srcdir}">
   16.53                      <classpath>
   16.54 -                        <path path="@{classpath}"/>
   16.55 +                        <path>
   16.56 +                            <pathelement path="@{classpath}"/>
   16.57 +                            <fileset dir="${scala.lib}">
   16.58 +                                <include name="**/*.jar"/>
   16.59 +                            </fileset>
   16.60 +                            <pathelement location="${build.classes.dir}"/>
   16.61 +                        </path>
   16.62                      </classpath>
   16.63                  </depend>
   16.64              </sequential>
   16.65 @@ -217,33 +223,25 @@
   16.66              <attribute default="${src.dir}" name="srcdir"/>
   16.67              <attribute default="${build.classes.dir}" name="destdir"/>
   16.68              <attribute default="${javac.classpath}" name="classpath"/>
   16.69 +            <attribute default="${extdirs}" name="extdirs"/>
   16.70              <attribute default="${includes}" name="includes"/>
   16.71              <attribute default="${excludes}" name="excludes"/>
   16.72 -            <attribute default="${javac.compilerargs}" name="addparams"/>
   16.73 +            <attribute default="${scalac.compilerargs}" name="addparams"/>
   16.74              <attribute default="" name="sourcepath"/>
   16.75              <element name="customize" optional="true"/>
   16.76              <sequential>
   16.77 -                <fsc addparams="@{addparams}" destdir="@{destdir}" encoding="${source.encoding}" excludes="@{excludes}" includes="@{includes}" sourcepath="@{sourcepath}" srcdir="@{srcdir}" target="jvm-${javac.target}">
   16.78 +                <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}">
   16.79                      <classpath>
   16.80 -                        <path path="@{classpath}"/>
   16.81 -                        <fileset dir="${scala.lib}">
   16.82 -                            <include name="**/*.jar"/>
   16.83 -                        </fileset>
   16.84 +                        <path>
   16.85 +                            <pathelement path="@{classpath}"/>
   16.86 +                            <fileset dir="${scala.lib}">
   16.87 +                                <include name="**/*.jar"/>
   16.88 +                            </fileset>
   16.89 +                            <pathelement location="${build.classes.dir}"/>
   16.90 +                        </path>
   16.91                      </classpath>
   16.92                      <customize/>
   16.93 -                </fsc>
   16.94 -            </sequential>
   16.95 -        </macrodef>
   16.96 -        <macrodef name="depend" uri="http://www.netbeans.org/ns/scala-project/1">
   16.97 -            <attribute default="${src.dir}" name="srcdir"/>
   16.98 -            <attribute default="${build.classes.dir}" name="destdir"/>
   16.99 -            <attribute default="${javac.classpath}" name="classpath"/>
  16.100 -            <sequential>
  16.101 -                <depend cache="${build.dir}/depcache" destdir="@{destdir}" excludes="${excludes}" includes="${includes}" srcdir="@{srcdir}">
  16.102 -                    <classpath>
  16.103 -                        <path path="@{classpath}"/>
  16.104 -                    </classpath>
  16.105 -                </depend>
  16.106 +                </scalac>
  16.107              </sequential>
  16.108          </macrodef>
  16.109          <macrodef name="force-recompile" uri="http://www.netbeans.org/ns/scala-project/1">
  16.110 @@ -551,14 +549,14 @@
  16.111              -->
  16.112      <target depends="init" name="-javadoc-build">
  16.113          <mkdir dir="${dist.javadoc.dir}"/>
  16.114 -        <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}">
  16.115 +        <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}">
  16.116              <classpath>
  16.117                  <path path="${javac.classpath}"/>
  16.118 +                <fileset dir="${scala.lib}">
  16.119 +                    <include name="**/*.jar"/>
  16.120 +                </fileset>
  16.121              </classpath>
  16.122 -            <fileset dir="${src.dir}" excludes="${excludes}" includes="${includes}">
  16.123 -                <filename name="**/*.java"/>
  16.124 -            </fileset>
  16.125 -        </javadoc>
  16.126 +        </scaladoc>
  16.127      </target>
  16.128      <target depends="init,-javadoc-build" if="netbeans.home" name="-javadoc-browse" unless="no.javadoc.preview">
  16.129          <nbbrowse file="${dist.javadoc.dir}/index.html"/>
  16.130 @@ -580,7 +578,7 @@
  16.131          <scalaProject1:depend classpath="${javac.test.classpath}" destdir="${build.test.classes.dir}" srcdir=""/>
  16.132      </target>
  16.133      <target depends="init,compile,-pre-pre-compile-test,-pre-compile-test,-compile-test-depend" if="have.tests" name="-do-compile-test">
  16.134 -        <scalaProject1:scalac classpath="${javac.test.classpath}" debug="true" destdir="${build.test.classes.dir}" srcdir=""/>
  16.135 +        <scalaProject1:scalac classpath="${javac.test.classpath}" destdir="${build.test.classes.dir}" srcdir=""/>
  16.136          <copy todir="${build.test.classes.dir}"/>
  16.137      </target>
  16.138      <target name="-post-compile-test">
  16.139 @@ -595,7 +593,7 @@
  16.140      <target depends="init,compile,-pre-pre-compile-test,-pre-compile-test-single" if="have.tests" name="-do-compile-test-single">
  16.141          <fail unless="javac.includes">Must select some files in the IDE or set javac.includes</fail>
  16.142          <scalaProject1:force-recompile destdir="${build.test.classes.dir}"/>
  16.143 -        <scalaProject1:scalac classpath="${javac.test.classpath}" debug="true" destdir="${build.test.classes.dir}" excludes="" includes="${javac.includes}" sourcepath="" srcdir=""/>
  16.144 +        <scalaProject1:scalac classpath="${javac.test.classpath}" destdir="${build.test.classes.dir}" excludes="" includes="${javac.includes}" sourcepath="" srcdir=""/>
  16.145          <copy todir="${build.test.classes.dir}"/>
  16.146      </target>
  16.147      <target name="-post-compile-test-single">
    17.1 --- a/src/Tools/jEdit/nbproject/genfiles.properties	Mon Mar 29 17:30:56 2010 +0200
    17.2 +++ b/src/Tools/jEdit/nbproject/genfiles.properties	Tue Mar 30 12:47:39 2010 +0200
    17.3 @@ -4,5 +4,5 @@
    17.4  # This file is used by a NetBeans-based IDE to track changes in generated files such as build-impl.xml.
    17.5  # Do not edit this file. You may delete it but then the IDE will never regenerate such files for you.
    17.6  nbproject/build-impl.xml.data.CRC32=8f41dcce
    17.7 -nbproject/build-impl.xml.script.CRC32=69f2059c
    17.8 -nbproject/build-impl.xml.stylesheet.CRC32=bc42a706@1.3.0
    17.9 +nbproject/build-impl.xml.script.CRC32=1c29c971
   17.10 +nbproject/build-impl.xml.stylesheet.CRC32=8c3c03dd@1.3.4
    18.1 --- a/src/Tools/jEdit/nbproject/project.properties	Mon Mar 29 17:30:56 2010 +0200
    18.2 +++ b/src/Tools/jEdit/nbproject/project.properties	Tue Mar 30 12:47:39 2010 +0200
    18.3 @@ -75,3 +75,7 @@
    18.4      ${build.test.classes.dir}
    18.5  source.encoding=UTF-8
    18.6  src.dir=${file.reference.isabelle-jedit-src}
    18.7 +scalac.compilerargs=
    18.8 +scalac.deprecation=no
    18.9 +scalac.unchecked=no
   18.10 +
    19.1 --- a/src/Tools/jEdit/src/jedit/document_model.scala	Mon Mar 29 17:30:56 2010 +0200
    19.2 +++ b/src/Tools/jEdit/src/jedit/document_model.scala	Tue Mar 30 12:47:39 2010 +0200
    19.3 @@ -8,6 +8,8 @@
    19.4  package isabelle.jedit
    19.5  
    19.6  
    19.7 +import isabelle._
    19.8 +
    19.9  import scala.actors.Actor, Actor._
   19.10  import scala.collection.mutable
   19.11  
    20.1 --- a/src/Tools/jEdit/src/jedit/document_view.scala	Mon Mar 29 17:30:56 2010 +0200
    20.2 +++ b/src/Tools/jEdit/src/jedit/document_view.scala	Tue Mar 30 12:47:39 2010 +0200
    20.3 @@ -8,6 +8,8 @@
    20.4  package isabelle.jedit
    20.5  
    20.6  
    20.7 +import isabelle._
    20.8 +
    20.9  import scala.actors.Actor._
   20.10  
   20.11  import java.awt.event.{MouseAdapter, MouseEvent}
    21.1 --- a/src/Tools/jEdit/src/jedit/html_panel.scala	Mon Mar 29 17:30:56 2010 +0200
    21.2 +++ b/src/Tools/jEdit/src/jedit/html_panel.scala	Tue Mar 30 12:47:39 2010 +0200
    21.3 @@ -7,6 +7,8 @@
    21.4  package isabelle.jedit
    21.5  
    21.6  
    21.7 +import isabelle._
    21.8 +
    21.9  import java.io.StringReader
   21.10  import java.awt.{BorderLayout, Dimension}
   21.11  import java.awt.event.MouseEvent
    22.1 --- a/src/Tools/jEdit/src/jedit/isabelle_encoding.scala	Mon Mar 29 17:30:56 2010 +0200
    22.2 +++ b/src/Tools/jEdit/src/jedit/isabelle_encoding.scala	Tue Mar 30 12:47:39 2010 +0200
    22.3 @@ -7,14 +7,16 @@
    22.4  package isabelle.jedit
    22.5  
    22.6  
    22.7 +import isabelle._
    22.8 +
    22.9  import org.gjt.sp.jedit.io.Encoding
   22.10  import org.gjt.sp.jedit.buffer.JEditBuffer
   22.11  
   22.12 -import java.nio.charset.{Charset, CharsetDecoder, CodingErrorAction}
   22.13 +import java.nio.charset.{Charset, CodingErrorAction}
   22.14  import java.io.{InputStream, OutputStream, Reader, Writer, InputStreamReader, OutputStreamWriter,
   22.15    CharArrayReader, ByteArrayOutputStream}
   22.16  
   22.17 -import scala.io.{Source, BufferedSource}
   22.18 +import scala.io.{Codec, Source, BufferedSource}
   22.19  
   22.20  
   22.21  object Isabelle_Encoding
   22.22 @@ -28,24 +30,23 @@
   22.23  class Isabelle_Encoding extends Encoding
   22.24  {
   22.25    private val charset = Charset.forName(Standard_System.charset)
   22.26 -  private val BUFSIZE = 32768
   22.27 +  val BUFSIZE = 32768
   22.28  
   22.29 -  private def text_reader(in: InputStream, decoder: CharsetDecoder): Reader =
   22.30 +  private def text_reader(in: InputStream, codec: Codec): Reader =
   22.31    {
   22.32 -    def source(): Source =
   22.33 -      BufferedSource.fromInputStream(in, decoder, BUFSIZE, { () => source() })
   22.34 +    val source = new BufferedSource(in)(codec)
   22.35      new CharArrayReader(Isabelle.system.symbols.decode(source.mkString).toArray)
   22.36    }
   22.37  
   22.38  	override def getTextReader(in: InputStream): Reader =
   22.39 -    text_reader(in, charset.newDecoder())
   22.40 +    text_reader(in, Standard_System.codec())
   22.41  
   22.42  	override def getPermissiveTextReader(in: InputStream): Reader =
   22.43  	{
   22.44 -		val decoder = charset.newDecoder()
   22.45 -		decoder.onMalformedInput(CodingErrorAction.REPLACE)
   22.46 -		decoder.onUnmappableCharacter(CodingErrorAction.REPLACE)
   22.47 -		text_reader(in, decoder)
   22.48 +		val codec = Standard_System.codec()
   22.49 +		codec.onMalformedInput(CodingErrorAction.REPLACE)
   22.50 +		codec.onUnmappableCharacter(CodingErrorAction.REPLACE)
   22.51 +		text_reader(in, codec)
   22.52  	}
   22.53  
   22.54    override def getTextWriter(out: OutputStream): Writer =
    23.1 --- a/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala	Mon Mar 29 17:30:56 2010 +0200
    23.2 +++ b/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala	Tue Mar 30 12:47:39 2010 +0200
    23.3 @@ -7,6 +7,8 @@
    23.4  package isabelle.jedit
    23.5  
    23.6  
    23.7 +import isabelle._
    23.8 +
    23.9  import java.io.File
   23.10  
   23.11  import gatchan.jedit.hyperlinks.{Hyperlink, HyperlinkSource, AbstractHyperlink}
    24.1 --- a/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala	Mon Mar 29 17:30:56 2010 +0200
    24.2 +++ b/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala	Tue Mar 30 12:47:39 2010 +0200
    24.3 @@ -8,6 +8,8 @@
    24.4  package isabelle.jedit
    24.5  
    24.6  
    24.7 +import isabelle._
    24.8 +
    24.9  import scala.collection.Set
   24.10  import scala.collection.immutable.TreeSet
   24.11  
    25.1 --- a/src/Tools/jEdit/src/jedit/output_dockable.scala	Mon Mar 29 17:30:56 2010 +0200
    25.2 +++ b/src/Tools/jEdit/src/jedit/output_dockable.scala	Tue Mar 30 12:47:39 2010 +0200
    25.3 @@ -7,6 +7,8 @@
    25.4  package isabelle.jedit
    25.5  
    25.6  
    25.7 +import isabelle._
    25.8 +
    25.9  import scala.actors.Actor._
   25.10  
   25.11  import javax.swing.JPanel
    26.1 --- a/src/Tools/jEdit/src/jedit/plugin.scala	Mon Mar 29 17:30:56 2010 +0200
    26.2 +++ b/src/Tools/jEdit/src/jedit/plugin.scala	Tue Mar 30 12:47:39 2010 +0200
    26.3 @@ -9,6 +9,8 @@
    26.4  package isabelle.jedit
    26.5  
    26.6  
    26.7 +import isabelle._
    26.8 +
    26.9  import java.io.{FileInputStream, IOException}
   26.10  import java.awt.Font
   26.11  import javax.swing.JTextArea
    27.1 --- a/src/Tools/jEdit/src/jedit/protocol_dockable.scala	Mon Mar 29 17:30:56 2010 +0200
    27.2 +++ b/src/Tools/jEdit/src/jedit/protocol_dockable.scala	Tue Mar 30 12:47:39 2010 +0200
    27.3 @@ -7,6 +7,8 @@
    27.4  package isabelle.jedit
    27.5  
    27.6  
    27.7 +import isabelle._
    27.8 +
    27.9  import scala.actors.Actor._
   27.10  
   27.11  import java.awt.{Dimension, Graphics, BorderLayout}
    28.1 --- a/src/Tools/jEdit/src/jedit/scala_console.scala	Mon Mar 29 17:30:56 2010 +0200
    28.2 +++ b/src/Tools/jEdit/src/jedit/scala_console.scala	Tue Mar 30 12:47:39 2010 +0200
    28.3 @@ -7,6 +7,8 @@
    28.4  package isabelle.jedit
    28.5  
    28.6  
    28.7 +import isabelle._
    28.8 +
    28.9  import console.{Console, ConsolePane, Shell, Output}
   28.10  
   28.11  import org.gjt.sp.jedit.{jEdit, JARClassLoader}
   28.12 @@ -63,7 +65,7 @@
   28.13  
   28.14      def write(cbuf: Array[Char], off: Int, len: Int)
   28.15      {
   28.16 -      if (len > 0) write(new String(cbuf.subArray(off, off + len)))
   28.17 +      if (len > 0) write(new String(cbuf.slice(off, off + len)))
   28.18      }
   28.19  
   28.20      override def write(str: String)