--- a/etc/settings Fri May 28 19:36:48 2010 +0100
+++ b/etc/settings Fri May 28 22:34:21 2010 +0200
@@ -56,14 +56,6 @@
###
ISABELLE_JAVA="java"
-ISABELLE_SCALA="scala"
-
-[ -z "$SCALA_HOME" ] && SCALA_HOME=$(choosefrom \
- "$ISABELLE_HOME/contrib/scala" \
- "$ISABELLE_HOME/../scala" \
- "")
-
-[ -n "$SCALA_HOME" ] && ISABELLE_SCALA="$SCALA_HOME/bin/scala"
classpath "$ISABELLE_HOME/lib/classes/Pure.jar"
--- a/lib/Tools/scala Fri May 28 19:36:48 2010 +0100
+++ b/lib/Tools/scala Fri May 28 22:34:21 2010 +0200
@@ -4,7 +4,9 @@
#
# DESCRIPTION: invoke Scala within the Isabelle environment
+[ -z "$SCALA_HOME" ] && { echo "Unknown SCALA_HOME -- Scala unavailable"; exit 2; }
+
[ -e "$ISABELLE_HOME/Admin/build" ] && { "$ISABELLE_HOME/Admin/build" jars || exit $?; }
CLASSPATH="$(jvmpath "$CLASSPATH")"
-exec "$ISABELLE_SCALA" "$@"
+exec "$SCALA_HOME/bin/scala" "$@"
--- a/src/Pure/PIDE/command.scala Fri May 28 19:36:48 2010 +0100
+++ b/src/Pure/PIDE/command.scala Fri May 28 22:34:21 2010 +0200
@@ -73,7 +73,7 @@
react {
case Consume(message, forward) if !assigned =>
val old_state = state
- state = old_state + message
+ state = old_state.accumulate(message)
if (!(state eq old_state)) forward(static_parent getOrElse this)
case Assign =>
--- a/src/Pure/PIDE/state.scala Fri May 28 19:36:48 2010 +0100
+++ b/src/Pure/PIDE/state.scala Fri May 28 22:34:21 2010 +0200
@@ -70,7 +70,7 @@
/* message dispatch */
- def + (message: XML.Tree): State =
+ def accumulate(message: XML.Tree): State =
message match {
case XML.Elem(Markup.STATUS, _, elems) =>
(this /: elems)((state, elem) =>
@@ -78,7 +78,7 @@
case XML.Elem(Markup.UNPROCESSED, _, _) => state.set_status(Command.Status.UNPROCESSED)
case XML.Elem(Markup.FINISHED, _, _) => state.set_status(Command.Status.FINISHED)
case XML.Elem(Markup.FAILED, _, _) => state.set_status(Command.Status.FAILED)
- case XML.Elem(kind, atts, body) =>
+ case XML.Elem(kind, atts, body) if Position.get_id(atts) == Some(command.id) =>
atts match {
case Position.Range(begin, end) =>
if (kind == Markup.ML_TYPING) {
@@ -99,11 +99,6 @@
case _ => state
}
}
- else if (kind == Markup.FACT_DECL || kind == Markup.LOCAL_FACT_DECL ||
- kind == Markup.ATTRIBUTE || kind == Markup.FIXED_DECL) {
- // FIXME usually displaced due to lack of full history support
- state
- }
else {
state.add_markup(
command.markup_node(begin - 1, end - 1, Command.HighlightInfo(kind)))
--- a/src/Pure/System/cygwin.scala Fri May 28 19:36:48 2010 +0100
+++ b/src/Pure/System/cygwin.scala Fri May 28 22:34:21 2010 +0200
@@ -116,7 +116,7 @@
val (_, rc) = Standard_System.raw_exec(root, null, true,
setup_exe.toString, "-R", root.toString, "-l", download.toString,
- "-P", "make,perl,python", "-q", "-n")
+ "-P", "make,perl,python", "-q", "-n")
if (rc != 0) error("Cygwin setup failed!")
sanity_check(root)
--- a/src/Pure/build-jars Fri May 28 19:36:48 2010 +0100
+++ b/src/Pure/build-jars Fri May 28 22:34:21 2010 +0200
@@ -16,7 +16,7 @@
}
[ -n "$ISABELLE_HOME" ] || fail "Missing Isabelle settings environment"
-[ -z "$SCALA_HOME" ] && fail "Scala unavailable: unknown SCALA_HOME"
+[ -z "$SCALA_HOME" ] && fail "Unknown SCALA_HOME -- Scala unavailable"
## dependencies
--- a/src/Tools/jEdit/nbproject/project.properties Fri May 28 19:36:48 2010 +0100
+++ b/src/Tools/jEdit/nbproject/project.properties Fri May 28 22:34:21 2010 +0200
@@ -76,6 +76,6 @@
source.encoding=UTF-8
src.dir=${file.reference.isabelle-jedit-src}
scalac.compilerargs=
-scalac.deprecation=no
-scalac.unchecked=no
+scalac.deprecation=yes
+scalac.unchecked=yes
--- a/src/Tools/jEdit/src/jedit/isabelle_encoding.scala Fri May 28 19:36:48 2010 +0100
+++ b/src/Tools/jEdit/src/jedit/isabelle_encoding.scala Fri May 28 22:34:21 2010 +0200
@@ -38,16 +38,16 @@
new CharArrayReader(Isabelle.system.symbols.decode(source.mkString).toArray)
}
- override def getTextReader(in: InputStream): Reader =
+ override def getTextReader(in: InputStream): Reader =
text_reader(in, Standard_System.codec())
- override def getPermissiveTextReader(in: InputStream): Reader =
- {
- val codec = Standard_System.codec()
- codec.onMalformedInput(CodingErrorAction.REPLACE)
- codec.onUnmappableCharacter(CodingErrorAction.REPLACE)
- text_reader(in, codec)
- }
+ override def getPermissiveTextReader(in: InputStream): Reader =
+ {
+ val codec = Standard_System.codec()
+ codec.onMalformedInput(CodingErrorAction.REPLACE)
+ codec.onUnmappableCharacter(CodingErrorAction.REPLACE)
+ text_reader(in, codec)
+ }
override def getTextWriter(out: OutputStream): Writer =
{
@@ -60,6 +60,6 @@
}
override def close() { out.close() }
}
- new OutputStreamWriter(buffer, charset.newEncoder())
+ new OutputStreamWriter(buffer, charset.newEncoder())
}
}
--- a/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala Fri May 28 19:36:48 2010 +0100
+++ b/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala Fri May 28 22:34:21 2010 +0200
@@ -38,8 +38,8 @@
class Isabelle_Hyperlinks extends HyperlinkSource
{
- def getHyperlink(buffer: Buffer, original_offset: Int): Hyperlink =
- {
+ def getHyperlink(buffer: Buffer, original_offset: Int): Hyperlink =
+ {
Document_Model(buffer) match {
case Some(model) =>
val document = model.recent_document()
--- a/src/Tools/jEdit/src/jedit/plugin.scala Fri May 28 19:36:48 2010 +0100
+++ b/src/Tools/jEdit/src/jedit/plugin.scala Fri May 28 22:34:21 2010 +0200
@@ -104,12 +104,12 @@
/* main jEdit components */ // FIXME ownership!?
- def jedit_buffers(): Iterator[Buffer] = Iterator.fromArray(jEdit.getBuffers())
+ def jedit_buffers(): Iterator[Buffer] = jEdit.getBuffers().iterator
- def jedit_views(): Iterator[View] = Iterator.fromArray(jEdit.getViews())
+ def jedit_views(): Iterator[View] = jEdit.getViews().iterator
def jedit_text_areas(view: View): Iterator[JEditTextArea] =
- Iterator.fromArray(view.getEditPanes).map(_.getTextArea)
+ view.getEditPanes().iterator.map(_.getTextArea)
def jedit_text_areas(): Iterator[JEditTextArea] =
jedit_views().flatMap(jedit_text_areas(_))
--- a/src/Tools/jEdit/src/jedit/scala_console.scala Fri May 28 19:36:48 2010 +0100
+++ b/src/Tools/jEdit/src/jedit/scala_console.scala Fri May 28 22:34:21 2010 +0200
@@ -130,17 +130,17 @@
}
override def printPrompt(console: Console, out: Output)
- {
+ {
out.writeAttrs(ConsolePane.colorAttributes(console.getInfoColor), "scala>")
- out.writeAttrs(ConsolePane.colorAttributes(console.getPlainColor), " ")
- }
+ out.writeAttrs(ConsolePane.colorAttributes(console.getPlainColor), " ")
+ }
override def execute(console: Console, input: String, out: Output, err: Output, command: String)
{
val interp = interpreters(console)
with_console(console, out, err) { interp.interpret(command) }
if (err != null) err.commandDone()
- out.commandDone()
+ out.commandDone()
}
override def stop(console: Console)