--- a/Admin/build Thu Jun 23 10:07:16 2011 -0700
+++ b/Admin/build Thu Jun 23 10:08:35 2011 -0700
@@ -84,6 +84,7 @@
function build_jars ()
{
+ "$ISABELLE_HOME/lib/scripts/java_ext_dirs" >/dev/null
pushd "$ISABELLE_HOME/src/Pure" >/dev/null
"$ISABELLE_TOOL" env ./build-jars "$@" || exit $?
popd >/dev/null
--- a/Isabelle Thu Jun 23 10:07:16 2011 -0700
+++ b/Isabelle Thu Jun 23 10:08:35 2011 -0700
@@ -26,4 +26,4 @@
CLASSPATH="$(jvmpath "$CLASSPATH")"
exec "$ISABELLE_TOOL" java \
"-Disabelle.home=$(jvmpath "$ISABELLE_HOME")" \
- -jar "$(jvmpath "$ISABELLE_HOME/lib/classes/isabelle-scala.jar")" "$@"
+ isabelle.GUI_Setup "$@"
--- a/etc/settings Thu Jun 23 10:07:16 2011 -0700
+++ b/etc/settings Thu Jun 23 10:08:35 2011 -0700
@@ -62,8 +62,6 @@
ISABELLE_JAVA="java"
fi
-classpath "$ISABELLE_HOME/lib/classes/Pure.jar"
-
###
### Interactive sessions (cf. isabelle tty)
--- a/lib/Tools/java Thu Jun 23 10:07:16 2011 -0700
+++ b/lib/Tools/java Thu Jun 23 10:08:35 2011 -0700
@@ -7,10 +7,13 @@
CLASSPATH="$(jvmpath "$CLASSPATH")"
JAVA_EXE="${THIS_JAVA:-$ISABELLE_JAVA}"
-if "$JAVA_EXE" -server >/dev/null 2>/dev/null
-then
- exec "$JAVA_EXE" -Dfile.encoding=UTF-8 -server "$@"
+
+if "$JAVA_EXE" -server >/dev/null 2>/dev/null; then
+ SERVER="-server"
else
- exec "$JAVA_EXE" -Dfile.encoding=UTF-8 "$@"
+ SERVER=""
fi
+exec "$JAVA_EXE" -Dfile.encoding=UTF-8 $SERVER \
+ "-Djava.ext.dirs=$("$ISABELLE_HOME/lib/scripts/java_ext_dirs")" "$@"
+
--- a/lib/Tools/scala Thu Jun 23 10:07:16 2011 -0700
+++ b/lib/Tools/scala Thu Jun 23 10:08:35 2011 -0700
@@ -9,4 +9,5 @@
[ -e "$ISABELLE_HOME/Admin/build" ] && { "$ISABELLE_HOME/Admin/build" jars || exit $?; }
CLASSPATH="$(jvmpath "$CLASSPATH")"
-exec "$SCALA_HOME/bin/scala" -Dfile.encoding=UTF-8 "$@"
+exec "$SCALA_HOME/bin/scala" -Dfile.encoding=UTF-8 \
+ "-Djava.ext.dirs=$("$ISABELLE_HOME/lib/scripts/java_ext_dirs")" "$@"
--- a/lib/scripts/getsettings Thu Jun 23 10:07:16 2011 -0700
+++ b/lib/scripts/getsettings Thu Jun 23 10:08:35 2011 -0700
@@ -60,6 +60,7 @@
THIS_CYGWIN="$(jvmpath "/")"
else
function jvmpath() { echo "$@"; }
+ CLASSPATH="$CLASSPATH"
fi
HOME_JVM="$HOME"
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/lib/scripts/java_ext_dirs Thu Jun 23 10:08:35 2011 -0700
@@ -0,0 +1,41 @@
+#!/usr/bin/env bash
+#
+# Author: Makarius
+#
+# Augment Java extension directories.
+
+## diagnostics
+
+function fail()
+{
+ echo "$1" >&2
+ exit 2
+}
+
+
+## dependencies
+
+SOURCE="$ISABELLE_HOME/src/Pure/System/Java_Ext_Dirs.java"
+
+TARGET_DIR="$ISABELLE_HOME/lib/classes"
+TARGET="$TARGET_DIR/java_ext_dirs.jar"
+
+if [ ! -e "$TARGET" -o "$SOURCE" -nt "$TARGET" ]; then
+ mkdir -p "$TARGET_DIR" || fail "Bad directory: \"$TARGET_DIR\""
+ pushd "$TARGET_DIR" >/dev/null
+
+ rm -rf classes && mkdir classes
+ javac -d classes -source 1.5 "$(jvmpath "$SOURCE")" || fail "Failed to compile sources"
+ jar cf "$(jvmpath "$TARGET")" -C classes . || fail "Failed to produce $TARGET"
+ rm -rf classes
+
+ popd >/dev/null
+fi
+
+
+## main
+
+JAVA_EXE="${THIS_JAVA:-$ISABELLE_JAVA}"
+exec "$JAVA_EXE" -classpath "$(jvmpath "$TARGET")" isabelle.Java_Ext_Dirs \
+ "$(jvmpath "$ISABELLE_HOME/lib/classes/ext")"
+
--- a/src/Pure/General/xml.scala Thu Jun 23 10:07:16 2011 -0700
+++ b/src/Pure/General/xml.scala Thu Jun 23 10:08:35 2011 -0700
@@ -6,6 +6,7 @@
package isabelle
+import java.lang.System
import java.util.WeakHashMap
import java.lang.ref.WeakReference
import javax.xml.parsers.DocumentBuilderFactory
--- a/src/Pure/PIDE/command.scala Thu Jun 23 10:07:16 2011 -0700
+++ b/src/Pure/PIDE/command.scala Thu Jun 23 10:08:35 2011 -0700
@@ -7,6 +7,7 @@
package isabelle
+import java.lang.System
import scala.collection.immutable.SortedMap
--- a/src/Pure/PIDE/markup_tree.scala Thu Jun 23 10:07:16 2011 -0700
+++ b/src/Pure/PIDE/markup_tree.scala Thu Jun 23 10:08:35 2011 -0700
@@ -7,7 +7,7 @@
package isabelle
-
+import java.lang.System
import javax.swing.tree.DefaultMutableTreeNode
import scala.collection.immutable.SortedMap
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/System/Java_Ext_Dirs.java Thu Jun 23 10:08:35 2011 -0700
@@ -0,0 +1,22 @@
+/* Title: Pure/System/Java_Ext_Dirs.java
+ Author: Makarius
+
+Augment Java extension directories.
+*/
+
+package isabelle;
+
+public class Java_Ext_Dirs
+{
+ public static void main(String [] args) {
+ StringBuilder s = new StringBuilder();
+ s.append(System.getProperty("java.ext.dirs"));
+ int i;
+ for (i = 0; i < args.length; i++) {
+ s.append(System.getProperty("path.separator"));
+ s.append(args[i]);
+ }
+ System.out.println(s.toString());
+ }
+}
+
--- a/src/Pure/System/cygwin.scala Thu Jun 23 10:07:16 2011 -0700
+++ b/src/Pure/System/cygwin.scala Thu Jun 23 10:08:35 2011 -0700
@@ -6,6 +6,7 @@
package isabelle
+import java.lang.System
import java.lang.reflect.Method
import java.io.File
import java.net.URL
@@ -91,7 +92,7 @@
def check_root(): String =
{
- val this_cygwin = java.lang.System.getenv("THIS_CYGWIN")
+ val this_cygwin = System.getenv("THIS_CYGWIN")
val root =
if (this_cygwin != null && this_cygwin != "") this_cygwin
else
--- a/src/Pure/System/gui_setup.scala Thu Jun 23 10:07:16 2011 -0700
+++ b/src/Pure/System/gui_setup.scala Thu Jun 23 10:08:35 2011 -0700
@@ -6,6 +6,8 @@
package isabelle
+import java.lang.System
+
import scala.swing.{Button, FlowPanel, BorderPanel, MainFrame, TextArea, SwingApplication}
import scala.swing.event.ButtonClicked
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/System/isabelle_charset.scala Thu Jun 23 10:08:35 2011 -0700
@@ -0,0 +1,50 @@
+/* Title: Pure/System/isabelle_charset.scala
+ Author: Makarius
+
+Charset for Isabelle symbols.
+*/
+
+package isabelle
+
+import java.nio.Buffer
+import java.nio.{ByteBuffer, CharBuffer}
+import java.nio.charset.{Charset, CharsetDecoder, CharsetEncoder, CoderResult}
+import java.nio.charset.spi.CharsetProvider
+
+
+object Isabelle_Charset
+{
+ val name: String = "UTF-8-Isabelle-test" // FIXME
+ lazy val charset: Charset = new Isabelle_Charset
+}
+
+
+class Isabelle_Charset extends Charset(Isabelle_Charset.name, null)
+{
+ override def contains(cs: Charset): Boolean =
+ cs.name.equalsIgnoreCase(Standard_System.charset_name) ||
+ Standard_System.charset.contains(cs)
+
+ override def newDecoder(): CharsetDecoder =
+ Standard_System.charset.newDecoder
+
+ override def newEncoder(): CharsetEncoder =
+ Standard_System.charset.newEncoder
+}
+
+
+class Isabelle_Charset_Provider extends CharsetProvider
+{
+ override def charsetForName(name: String): Charset =
+ {
+ if (name.equalsIgnoreCase(Isabelle_Charset.name)) Isabelle_Charset.charset
+ else null
+ }
+
+ override def charsets(): java.util.Iterator[Charset] =
+ {
+ import scala.collection.JavaConversions._
+ Iterator(Isabelle_Charset.charset)
+ }
+}
+
--- a/src/Pure/System/isabelle_process.scala Thu Jun 23 10:07:16 2011 -0700
+++ b/src/Pure/System/isabelle_process.scala Thu Jun 23 10:08:35 2011 -0700
@@ -7,6 +7,7 @@
package isabelle
+import java.lang.System
import java.util.concurrent.LinkedBlockingQueue
import java.io.{BufferedReader, BufferedWriter, InputStreamReader, OutputStreamWriter,
InputStream, OutputStream, BufferedOutputStream, IOException}
--- a/src/Pure/System/isabelle_system.scala Thu Jun 23 10:07:16 2011 -0700
+++ b/src/Pure/System/isabelle_system.scala Thu Jun 23 10:08:35 2011 -0700
@@ -6,6 +6,7 @@
package isabelle
+import java.lang.System
import java.util.regex.Pattern
import java.util.Locale
import java.io.{InputStream, FileInputStream, OutputStream, FileOutputStream, File,
@@ -41,7 +42,7 @@
{
import scala.collection.JavaConversions._
- val env0 = Map(java.lang.System.getenv.toList: _*) +
+ val env0 = Map(System.getenv.toList: _*) +
("THIS_JAVA" -> this_java())
val isabelle_home =
@@ -49,7 +50,7 @@
else
env0.get("ISABELLE_HOME") match {
case None | Some("") =>
- val path = java.lang.System.getProperty("isabelle.home")
+ val path = System.getProperty("isabelle.home")
if (path == null || path == "") error("Unknown Isabelle home directory")
else path
case Some(path) => path
@@ -70,8 +71,8 @@
else (entry.substring(0, i) -> entry.substring(i + 1))
}
Map(entries: _*) +
- ("HOME" -> java.lang.System.getenv("HOME")) +
- ("PATH" -> java.lang.System.getenv("PATH"))
+ ("HOME" -> System.getenv("HOME")) +
+ ("PATH" -> System.getenv("PATH"))
}
}
--- a/src/Pure/System/platform.scala Thu Jun 23 10:07:16 2011 -0700
+++ b/src/Pure/System/platform.scala Thu Jun 23 10:08:35 2011 -0700
@@ -6,6 +6,7 @@
package isabelle
+import java.lang.System
import javax.swing.UIManager
import scala.util.matching.Regex
@@ -34,7 +35,7 @@
lazy val jvm_platform: String =
{
val arch =
- java.lang.System.getProperty("os.arch") match {
+ System.getProperty("os.arch") match {
case X86() => "x86"
case X86_64() => "x86_64"
case Sparc() => "sparc"
@@ -42,7 +43,7 @@
case _ => error("Failed to determine CPU architecture")
}
val os =
- java.lang.System.getProperty("os.name") match {
+ System.getProperty("os.name") match {
case Solaris() => "solaris"
case Linux() => "linux"
case Darwin() => "darwin"
@@ -55,7 +56,7 @@
/* JVM name */
- val jvm_name: String = java.lang.System.getProperty("java.vm.name")
+ val jvm_name: String = System.getProperty("java.vm.name")
val is_hotspot: Boolean = jvm_name.startsWith("Java HotSpot")
--- a/src/Pure/System/session.scala Thu Jun 23 10:07:16 2011 -0700
+++ b/src/Pure/System/session.scala Thu Jun 23 10:08:35 2011 -0700
@@ -7,6 +7,7 @@
package isabelle
+import java.lang.System
import scala.actors.TIMEOUT
import scala.actors.Actor
--- a/src/Pure/System/standard_system.scala Thu Jun 23 10:07:16 2011 -0700
+++ b/src/Pure/System/standard_system.scala Thu Jun 23 10:08:35 2011 -0700
@@ -6,6 +6,7 @@
package isabelle
+import java.lang.System
import java.util.zip.{ZipEntry, ZipInputStream}
import java.util.regex.Pattern
import java.util.Locale
@@ -13,6 +14,7 @@
import java.io.{BufferedWriter, OutputStreamWriter, FileOutputStream, BufferedOutputStream,
BufferedInputStream, InputStream, FileInputStream, BufferedReader, InputStreamReader,
File, FileFilter, IOException}
+import java.nio.charset.Charset
import scala.io.{Source, Codec}
import scala.util.matching.Regex
@@ -23,7 +25,8 @@
{
/* UTF-8 charset */
- val charset = "UTF-8"
+ val charset_name: String = "UTF-8"
+ val charset: Charset = Charset.forName(charset_name)
def codec(): Codec = Codec(charset)
def string_bytes(s: String): Array[Byte] = s.getBytes(charset)
@@ -95,7 +98,8 @@
def write_file(file: File, text: CharSequence)
{
- val writer = new BufferedWriter(new OutputStreamWriter(new FileOutputStream(file), charset))
+ val writer =
+ new BufferedWriter(new OutputStreamWriter(new FileOutputStream(file), charset))
try { writer.append(text) }
finally { writer.close }
}
--- a/src/Pure/build-jars Thu Jun 23 10:07:16 2011 -0700
+++ b/src/Pure/build-jars Thu Jun 23 10:08:35 2011 -0700
@@ -37,6 +37,7 @@
System/download.scala
System/event_bus.scala
System/gui_setup.scala
+ System/isabelle_charset.scala
System/isabelle_process.scala
System/isabelle_syntax.scala
System/isabelle_system.scala
@@ -106,16 +107,10 @@
-## dependencies
+# build
TARGET_DIR="$ISABELLE_HOME/lib/classes"
-PURE_JAR="$TARGET_DIR/Pure.jar"
-FULL_JAR="$TARGET_DIR/isabelle-scala.jar"
-
-declare -a TARGETS=("$PURE_JAR" "$FULL_JAR")
-
-
-## main
+TARGET="$TARGET_DIR/ext/Pure.jar"
declare -a UPDATED=()
@@ -123,23 +118,16 @@
OUTDATED=true
else
OUTDATED=false
- for TARGET in "${TARGETS[@]}"
- do
- [ ! -e "$TARGET" ] && OUTDATED=true
- done
- if [ "$OUTDATED" = false ]; then
+ if [ ! -e "$TARGET" ]; then
+ OUTDATED=true
+ else
for DEP in "${SOURCES[@]}"
do
[ ! -e "$DEP" ] && fail "Missing file: $DEP"
- UPDATE=""
- for TARGET in "${TARGETS[@]}"
- do
- [ "$DEP" -nt "$TARGET" ] && {
- OUTDATED=true
- UPDATE=true
- }
- done
- [ -n "$UPDATE" ] && UPDATED["${#UPDATED[@]}"]="$DEP"
+ [ "$DEP" -nt "$TARGET" ] && {
+ OUTDATED=true
+ UPDATED["${#UPDATED[@]}"]="$DEP"
+ }
done
fi
fi
@@ -161,19 +149,18 @@
rm -rf classes && mkdir classes
"$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"
+ mkdir -p "$TARGET_DIR/ext" || fail "Failed to create directory $TARGET_DIR/ext"
pushd classes >/dev/null
- jar cfe "$(jvmpath "$PURE_JAR")" isabelle.GUI_Setup isabelle || \
- fail "Failed to produce $PURE_JAR"
+ CHARSET_SERVICE="META-INF/services/java.nio.charset.spi.CharsetProvider"
+ mkdir -p "$(dirname "$CHARSET_SERVICE")"
+ echo isabelle.Isabelle_Charset_Provider > "$CHARSET_SERVICE"
- cp "$SCALA_HOME/lib/scala-swing.jar" .
- jar xf scala-swing.jar
+ jar cfe "$(jvmpath "$TARGET")" isabelle.GUI_Setup META-INF isabelle || \
+ fail "Failed to produce $TARGET"
- cp "$SCALA_HOME/lib/scala-library.jar" "$FULL_JAR"
- jar ufe "$(jvmpath "$FULL_JAR")" isabelle.GUI_Setup isabelle scala || \
- fail "Failed to produce $FULL_JAR"
+ cp "$SCALA_HOME/lib/scala-swing.jar" "$SCALA_HOME/lib/scala-library.jar" "$TARGET_DIR/ext"
popd >/dev/null
--- a/src/Tools/jEdit/lib/Tools/jedit Thu Jun 23 10:07:16 2011 -0700
+++ b/src/Tools/jEdit/lib/Tools/jedit Thu Jun 23 10:08:35 2011 -0700
@@ -146,7 +146,7 @@
[ -e "$ISABELLE_HOME/Admin/build" ] && \
{ "$ISABELLE_HOME/Admin/build" "$BUILD_JARS" || exit $?; }
-PURE_JAR="$ISABELLE_HOME/lib/classes/Pure.jar"
+PURE_JAR="$ISABELLE_HOME/lib/classes/ext/Pure.jar"
pushd "$JEDIT_HOME" >/dev/null || failed
@@ -234,14 +234,13 @@
print qq,<MODE NAME="scala" FILE="scala.xml" FILE_NAME_GLOB="*.scala" />\n\n,; }
print; }' dist/modes/catalog
- cp -a "${JEDIT_JARS[@]}" "${SCALA_JARS[@]}" "$PURE_JAR" dist/jars/. || failed
+ cp -a "${JEDIT_JARS[@]}" "$SCALA_HOME/lib/scala-compiler.jar" dist/jars/. || failed
(
- for JAR in "$JEDIT_JAR" "${JEDIT_JARS[@]}" "$SCALA_HOME/lib/scala-compiler.jar"
+ for JAR in "$JEDIT_JAR" "${JEDIT_JARS[@]}" "$PURE_JAR" "$SCALA_HOME/lib/scala-compiler.jar"
do
CLASSPATH="$CLASSPATH:$JAR"
done
CLASSPATH="$(jvmpath "$CLASSPATH")"
-
exec "$SCALA_HOME/bin/scalac" -unchecked -deprecation \
-d dist/classes -target:jvm-1.5 "${SOURCES[@]}"
) || fail "Failed to compile sources"
--- a/src/Tools/jEdit/src/document_view.scala Thu Jun 23 10:07:16 2011 -0700
+++ b/src/Tools/jEdit/src/document_view.scala Thu Jun 23 10:08:35 2011 -0700
@@ -12,6 +12,7 @@
import scala.actors.Actor._
+import java.lang.System
import java.awt.{BorderLayout, Graphics, Color, Dimension, Graphics2D, Point}
import java.awt.event.{MouseAdapter, MouseMotionAdapter, MouseEvent,
FocusAdapter, FocusEvent, WindowEvent, WindowAdapter}
--- a/src/Tools/jEdit/src/html_panel.scala Thu Jun 23 10:07:16 2011 -0700
+++ b/src/Tools/jEdit/src/html_panel.scala Thu Jun 23 10:08:35 2011 -0700
@@ -9,6 +9,7 @@
import isabelle._
+import java.lang.System
import java.io.StringReader
import java.awt.{Font, BorderLayout, Dimension, GraphicsEnvironment, Toolkit, FontMetrics}
import java.awt.event.MouseEvent
--- a/src/Tools/jEdit/src/isabelle_encoding.scala Thu Jun 23 10:07:16 2011 -0700
+++ b/src/Tools/jEdit/src/isabelle_encoding.scala Thu Jun 23 10:08:35 2011 -0700
@@ -29,8 +29,7 @@
class Isabelle_Encoding extends Encoding
{
- private val charset = Charset.forName(Standard_System.charset)
- val BUFSIZE = 32768
+ private val BUFSIZE = 32768
private def text_reader(in: InputStream, codec: Codec): Reader =
{
@@ -54,12 +53,12 @@
val buffer = new ByteArrayOutputStream(BUFSIZE) {
override def flush()
{
- val text = Isabelle.system.symbols.encode(toString(Standard_System.charset))
+ val text = Isabelle.system.symbols.encode(toString(Standard_System.charset_name))
out.write(text.getBytes(Standard_System.charset))
out.flush()
}
override def close() { out.close() }
}
- new OutputStreamWriter(buffer, charset.newEncoder())
+ new OutputStreamWriter(buffer, Standard_System.charset.newEncoder())
}
}
--- a/src/Tools/jEdit/src/output_dockable.scala Thu Jun 23 10:07:16 2011 -0700
+++ b/src/Tools/jEdit/src/output_dockable.scala Thu Jun 23 10:08:35 2011 -0700
@@ -14,6 +14,7 @@
import scala.swing.{FlowPanel, Button, CheckBox}
import scala.swing.event.ButtonClicked
+import java.lang.System
import java.awt.BorderLayout
import java.awt.event.{ComponentEvent, ComponentAdapter}
--- a/src/Tools/jEdit/src/plugin.scala Thu Jun 23 10:07:16 2011 -0700
+++ b/src/Tools/jEdit/src/plugin.scala Thu Jun 23 10:08:35 2011 -0700
@@ -9,6 +9,7 @@
import isabelle._
+import java.lang.System
import java.io.{FileInputStream, IOException}
import java.awt.Font
--- a/src/Tools/jEdit/src/protocol_dockable.scala Thu Jun 23 10:07:16 2011 -0700
+++ b/src/Tools/jEdit/src/protocol_dockable.scala Thu Jun 23 10:08:35 2011 -0700
@@ -9,6 +9,8 @@
import isabelle._
+import java.lang.System
+
import scala.actors.Actor._
import scala.swing.{TextArea, ScrollPane}
--- a/src/Tools/jEdit/src/raw_output_dockable.scala Thu Jun 23 10:07:16 2011 -0700
+++ b/src/Tools/jEdit/src/raw_output_dockable.scala Thu Jun 23 10:08:35 2011 -0700
@@ -9,6 +9,8 @@
import isabelle._
+import java.lang.System
+
import scala.actors.Actor._
import scala.swing.{TextArea, ScrollPane}
--- a/src/Tools/jEdit/src/scala_console.scala Thu Jun 23 10:07:16 2011 -0700
+++ b/src/Tools/jEdit/src/scala_console.scala Thu Jun 23 10:08:35 2011 -0700
@@ -14,6 +14,7 @@
import org.gjt.sp.jedit.{jEdit, JARClassLoader}
import org.gjt.sp.jedit.MiscUtilities
+import java.lang.System
import java.io.{File, OutputStream, Writer, PrintWriter}
import scala.tools.nsc.{Interpreter, GenericRunnerSettings, NewLinePrintWriter, ConsoleWriter}
--- a/src/Tools/jEdit/src/session_dockable.scala Thu Jun 23 10:07:16 2011 -0700
+++ b/src/Tools/jEdit/src/session_dockable.scala Thu Jun 23 10:08:35 2011 -0700
@@ -13,6 +13,7 @@
import scala.swing.{FlowPanel, Button, TextArea, Label, ScrollPane, TabbedPane, Component, Swing}
import scala.swing.event.{ButtonClicked, SelectionChanged}
+import java.lang.System
import java.awt.BorderLayout
import javax.swing.border.{BevelBorder, SoftBevelBorder}