--- a/Admin/makedist Wed Nov 17 09:22:23 2010 +0100
+++ b/Admin/makedist Wed Nov 17 13:39:30 2010 +0100
@@ -108,7 +108,7 @@
if [ -z "$RELEASE" ]; then
DISTNAME="Isabelle_$DATE"
- DISTVERSION="Isabelle repository snapshot $IDENT ($DATE)"
+ DISTVERSION="Isabelle repository snapshot $IDENT $DATE"
else
DISTNAME="$RELEASE"
DISTVERSION="$DISTNAME: $DISTDATE"
--- a/Isabelle Wed Nov 17 09:22:23 2010 +0100
+++ b/Isabelle Wed Nov 17 13:39:30 2010 +0100
@@ -24,6 +24,6 @@
[ -e "$ISABELLE_HOME/Admin/build" ] && "$ISABELLE_HOME/Admin/build" jars
CLASSPATH="$(jvmpath "$CLASSPATH")"
-exec "$ISABELLE_JAVA" \
+exec "$ISABELLE_TOOL" java \
"-Disabelle.home=$(jvmpath "$ISABELLE_HOME")" \
-jar "$(jvmpath "$ISABELLE_HOME/lib/classes/isabelle-scala.jar")" "$@"
--- a/doc-src/System/Thy/Basics.thy Wed Nov 17 09:22:23 2010 +0100
+++ b/doc-src/System/Thy/Basics.thy Wed Nov 17 13:39:30 2010 +0100
@@ -309,12 +309,18 @@
The root of component initialization is @{setting ISABELLE_HOME}
itself. After initializing all of its sub-components recursively,
@{setting ISABELLE_HOME_USER} is included in the same manner (if
- that directory exists). Thus users can easily add private
- components to @{verbatim "$ISABELLE_HOME_USER/etc/components"}.
-
- It is also possible to initialize components programmatically via
- the \verb,init_component, shell function, say within the
- \verb,settings, script of another component.
+ that directory exists). This allows to install private components
+ via @{verbatim "$ISABELLE_HOME_USER/etc/components"}, although it is
+ often more convenient to do that programmatically via the
+ \verb,init_component, shell function in the \verb,etc/settings,
+ script of \verb,$ISABELLE_HOME_USER, (or any other component
+ directory). For example:
+ \begin{verbatim}
+ if [ -d "$HOME/screwdriver-2.0" ]
+ then
+ init_component "$HOME/screwdriver-2.0"
+ else
+ \end{verbatim}
*}
--- a/doc-src/System/Thy/document/Basics.tex Wed Nov 17 09:22:23 2010 +0100
+++ b/doc-src/System/Thy/document/Basics.tex Wed Nov 17 13:39:30 2010 +0100
@@ -318,12 +318,18 @@
The root of component initialization is \hyperlink{setting.ISABELLE-HOME}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}HOME}}}}
itself. After initializing all of its sub-components recursively,
\hyperlink{setting.ISABELLE-HOME-USER}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}HOME{\isaliteral{5F}{\isacharunderscore}}USER}}}} is included in the same manner (if
- that directory exists). Thus users can easily add private
- components to \verb|$ISABELLE_HOME_USER/etc/components|.
-
- It is also possible to initialize components programmatically via
- the \verb,init_component, shell function, say within the
- \verb,settings, script of another component.%
+ that directory exists). This allows to install private components
+ via \verb|$ISABELLE_HOME_USER/etc/components|, although it is
+ often more convenient to do that programmatically via the
+ \verb,init_component, shell function in the \verb,etc/settings,
+ script of \verb,$ISABELLE_HOME_USER, (or any other component
+ directory). For example:
+ \begin{verbatim}
+ if [ -d "$HOME/screwdriver-2.0" ]
+ then
+ init_component "$HOME/screwdriver-2.0"
+ else
+ \end{verbatim}%
\end{isamarkuptext}%
\isamarkuptrue%
%
--- a/etc/settings Wed Nov 17 09:22:23 2010 +0100
+++ b/etc/settings Wed Nov 17 13:39:30 2010 +0100
@@ -55,7 +55,11 @@
### JVM components (Scala or Java)
###
-ISABELLE_JAVA="java"
+if [ -n "$JAVA_HOME" ]; then
+ ISABELLE_JAVA="$JAVA_HOME/bin/java"
+else
+ ISABELLE_JAVA="java"
+fi
classpath "$ISABELLE_HOME/lib/classes/Pure.jar"
--- a/lib/scripts/getsettings Wed Nov 17 09:22:23 2010 +0100
+++ b/lib/scripts/getsettings Wed Nov 17 13:39:30 2010 +0100
@@ -72,6 +72,7 @@
CLASSPATH="$CLASSPATH:$X"
fi
done
+ export CLASSPATH
}
#arrays
@@ -90,6 +91,13 @@
function init_component ()
{
local COMPONENT="$1"
+ case "$COMPONENT" in
+ /*) ;;
+ *)
+ echo >&2 "Absolute component path required: \"$COMPONENT\""
+ exit 2
+ ;;
+ esac
if [ ! -d "$COMPONENT" ]; then
echo >&2 "Bad Isabelle component: \"$COMPONENT\""
--- a/src/Pure/PIDE/command.scala Wed Nov 17 09:22:23 2010 +0100
+++ b/src/Pure/PIDE/command.scala Wed Nov 17 13:39:30 2010 +0100
@@ -54,7 +54,9 @@
val props = Position.purge(atts)
val info = Text.Info[Any](range, XML.Elem(Markup(name, props), args))
state.add_markup(info)
- case _ => System.err.println("Ignored report message: " + msg); state
+ case _ =>
+ // FIXME System.err.println("Ignored report message: " + msg)
+ state
})
case XML.Elem(Markup(name, atts), body) =>
atts match {
--- a/src/Pure/System/gui_setup.scala Wed Nov 17 09:22:23 2010 +0100
+++ b/src/Pure/System/gui_setup.scala Wed Nov 17 13:39:30 2010 +0100
@@ -39,6 +39,7 @@
// values
if (Platform.is_windows)
text.append("Cygwin root: " + Cygwin.check_root() + "\n")
+ text.append("JVM name: " + System.getProperty("java.vm.name") + "\n")
text.append("JVM platform: " + Platform.jvm_platform + "\n")
try {
val isabelle_system = new Isabelle_System
--- a/src/Tools/jEdit/dist-template/lib/Tools/jedit Wed Nov 17 09:22:23 2010 +0100
+++ b/src/Tools/jEdit/dist-template/lib/Tools/jedit Wed Nov 17 13:39:30 2010 +0100
@@ -24,7 +24,6 @@
echo " -m MODE add print mode for output"
echo
echo "Start jEdit with Isabelle plugin setup and opens theory FILES"
- echo "(default ~/Scratch.thy)."
echo
exit 1
}
@@ -93,14 +92,10 @@
# args
-if [ "$#" -eq 0 ]; then
- ARGS["${#ARGS[@]}"]="Scratch.thy"
-else
- while [ "$#" -gt 0 ]; do
- ARGS["${#ARGS[@]}"]="$(jvmpath "$1")"
- shift
- done
-fi
+while [ "$#" -gt 0 ]; do
+ ARGS["${#ARGS[@]}"]="$(jvmpath "$1")"
+ shift
+done
## default perspective