--- 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)
--- 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 **/
--- 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
--- 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 ++ "<"
- case '>' => s ++ ">"
- case '&' => s ++ "&"
- case '"' => s ++ """
- case '\'' => s ++ "'"
- case _ => s + c
+ for (c <- text.iterator) c match {
+ case '<' => s ++= "<"
+ case '>' => s ++= ">"
+ case '&' => s ++= "&"
+ case '"' => s ++= """
+ case '\'' => s ++= "'"
+ 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)
}
}
--- 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(", ")
--- 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(
--- 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 {
--- 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>"
--- 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
}
--- 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)) :::
--- 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()
--- 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
}
}
--- 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)))
}
--- 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"
(
--- 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
--- 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">
--- 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
--- 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
+
--- 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
--- 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}
--- 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
--- 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 =
--- 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}
--- 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
--- 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
--- 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
--- 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}
--- 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)