# HG changeset patch # User wenzelm # Date 1275078861 -7200 # Node ID d47fe9260c245c750e8f9a4eb1497ca5706b6dea # Parent 446cf1f997d19a6d89b9d57ec6c32ae8da0c6125# Parent d52f934f8ff6ef24f24fa53657a36bcb69b2cea7 merged diff -r 446cf1f997d1 -r d47fe9260c24 etc/settings --- 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" diff -r 446cf1f997d1 -r d47fe9260c24 lib/Tools/scala --- 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" "$@" diff -r 446cf1f997d1 -r d47fe9260c24 src/Pure/PIDE/command.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 => diff -r 446cf1f997d1 -r d47fe9260c24 src/Pure/PIDE/state.scala --- 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))) diff -r 446cf1f997d1 -r d47fe9260c24 src/Pure/System/cygwin.scala --- 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) diff -r 446cf1f997d1 -r d47fe9260c24 src/Pure/build-jars --- 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 diff -r 446cf1f997d1 -r d47fe9260c24 src/Tools/jEdit/nbproject/project.properties --- 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 diff -r 446cf1f997d1 -r d47fe9260c24 src/Tools/jEdit/src/jedit/isabelle_encoding.scala --- 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()) } } diff -r 446cf1f997d1 -r d47fe9260c24 src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala --- 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() diff -r 446cf1f997d1 -r d47fe9260c24 src/Tools/jEdit/src/jedit/plugin.scala --- 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(_)) diff -r 446cf1f997d1 -r d47fe9260c24 src/Tools/jEdit/src/jedit/scala_console.scala --- 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)