1.1 --- a/Admin/makedist Wed Nov 17 09:22:23 2010 +0100
1.2 +++ b/Admin/makedist Wed Nov 17 13:39:30 2010 +0100
1.3 @@ -108,7 +108,7 @@
1.4
1.5 if [ -z "$RELEASE" ]; then
1.6 DISTNAME="Isabelle_$DATE"
1.7 - DISTVERSION="Isabelle repository snapshot $IDENT ($DATE)"
1.8 + DISTVERSION="Isabelle repository snapshot $IDENT $DATE"
1.9 else
1.10 DISTNAME="$RELEASE"
1.11 DISTVERSION="$DISTNAME: $DISTDATE"
2.1 --- a/Isabelle Wed Nov 17 09:22:23 2010 +0100
2.2 +++ b/Isabelle Wed Nov 17 13:39:30 2010 +0100
2.3 @@ -24,6 +24,6 @@
2.4 [ -e "$ISABELLE_HOME/Admin/build" ] && "$ISABELLE_HOME/Admin/build" jars
2.5
2.6 CLASSPATH="$(jvmpath "$CLASSPATH")"
2.7 -exec "$ISABELLE_JAVA" \
2.8 +exec "$ISABELLE_TOOL" java \
2.9 "-Disabelle.home=$(jvmpath "$ISABELLE_HOME")" \
2.10 -jar "$(jvmpath "$ISABELLE_HOME/lib/classes/isabelle-scala.jar")" "$@"
3.1 --- a/doc-src/System/Thy/Basics.thy Wed Nov 17 09:22:23 2010 +0100
3.2 +++ b/doc-src/System/Thy/Basics.thy Wed Nov 17 13:39:30 2010 +0100
3.3 @@ -309,12 +309,18 @@
3.4 The root of component initialization is @{setting ISABELLE_HOME}
3.5 itself. After initializing all of its sub-components recursively,
3.6 @{setting ISABELLE_HOME_USER} is included in the same manner (if
3.7 - that directory exists). Thus users can easily add private
3.8 - components to @{verbatim "$ISABELLE_HOME_USER/etc/components"}.
3.9 -
3.10 - It is also possible to initialize components programmatically via
3.11 - the \verb,init_component, shell function, say within the
3.12 - \verb,settings, script of another component.
3.13 + that directory exists). This allows to install private components
3.14 + via @{verbatim "$ISABELLE_HOME_USER/etc/components"}, although it is
3.15 + often more convenient to do that programmatically via the
3.16 + \verb,init_component, shell function in the \verb,etc/settings,
3.17 + script of \verb,$ISABELLE_HOME_USER, (or any other component
3.18 + directory). For example:
3.19 + \begin{verbatim}
3.20 + if [ -d "$HOME/screwdriver-2.0" ]
3.21 + then
3.22 + init_component "$HOME/screwdriver-2.0"
3.23 + else
3.24 + \end{verbatim}
3.25 *}
3.26
3.27
4.1 --- a/doc-src/System/Thy/document/Basics.tex Wed Nov 17 09:22:23 2010 +0100
4.2 +++ b/doc-src/System/Thy/document/Basics.tex Wed Nov 17 13:39:30 2010 +0100
4.3 @@ -318,12 +318,18 @@
4.4 The root of component initialization is \hyperlink{setting.ISABELLE-HOME}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}HOME}}}}
4.5 itself. After initializing all of its sub-components recursively,
4.6 \hyperlink{setting.ISABELLE-HOME-USER}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}HOME{\isaliteral{5F}{\isacharunderscore}}USER}}}} is included in the same manner (if
4.7 - that directory exists). Thus users can easily add private
4.8 - components to \verb|$ISABELLE_HOME_USER/etc/components|.
4.9 -
4.10 - It is also possible to initialize components programmatically via
4.11 - the \verb,init_component, shell function, say within the
4.12 - \verb,settings, script of another component.%
4.13 + that directory exists). This allows to install private components
4.14 + via \verb|$ISABELLE_HOME_USER/etc/components|, although it is
4.15 + often more convenient to do that programmatically via the
4.16 + \verb,init_component, shell function in the \verb,etc/settings,
4.17 + script of \verb,$ISABELLE_HOME_USER, (or any other component
4.18 + directory). For example:
4.19 + \begin{verbatim}
4.20 + if [ -d "$HOME/screwdriver-2.0" ]
4.21 + then
4.22 + init_component "$HOME/screwdriver-2.0"
4.23 + else
4.24 + \end{verbatim}%
4.25 \end{isamarkuptext}%
4.26 \isamarkuptrue%
4.27 %
5.1 --- a/etc/settings Wed Nov 17 09:22:23 2010 +0100
5.2 +++ b/etc/settings Wed Nov 17 13:39:30 2010 +0100
5.3 @@ -55,7 +55,11 @@
5.4 ### JVM components (Scala or Java)
5.5 ###
5.6
5.7 -ISABELLE_JAVA="java"
5.8 +if [ -n "$JAVA_HOME" ]; then
5.9 + ISABELLE_JAVA="$JAVA_HOME/bin/java"
5.10 +else
5.11 + ISABELLE_JAVA="java"
5.12 +fi
5.13
5.14 classpath "$ISABELLE_HOME/lib/classes/Pure.jar"
5.15
6.1 --- a/lib/scripts/getsettings Wed Nov 17 09:22:23 2010 +0100
6.2 +++ b/lib/scripts/getsettings Wed Nov 17 13:39:30 2010 +0100
6.3 @@ -72,6 +72,7 @@
6.4 CLASSPATH="$CLASSPATH:$X"
6.5 fi
6.6 done
6.7 + export CLASSPATH
6.8 }
6.9
6.10 #arrays
6.11 @@ -90,6 +91,13 @@
6.12 function init_component ()
6.13 {
6.14 local COMPONENT="$1"
6.15 + case "$COMPONENT" in
6.16 + /*) ;;
6.17 + *)
6.18 + echo >&2 "Absolute component path required: \"$COMPONENT\""
6.19 + exit 2
6.20 + ;;
6.21 + esac
6.22
6.23 if [ ! -d "$COMPONENT" ]; then
6.24 echo >&2 "Bad Isabelle component: \"$COMPONENT\""
7.1 --- a/src/Pure/PIDE/command.scala Wed Nov 17 09:22:23 2010 +0100
7.2 +++ b/src/Pure/PIDE/command.scala Wed Nov 17 13:39:30 2010 +0100
7.3 @@ -54,7 +54,9 @@
7.4 val props = Position.purge(atts)
7.5 val info = Text.Info[Any](range, XML.Elem(Markup(name, props), args))
7.6 state.add_markup(info)
7.7 - case _ => System.err.println("Ignored report message: " + msg); state
7.8 + case _ =>
7.9 + // FIXME System.err.println("Ignored report message: " + msg)
7.10 + state
7.11 })
7.12 case XML.Elem(Markup(name, atts), body) =>
7.13 atts match {
8.1 --- a/src/Pure/System/gui_setup.scala Wed Nov 17 09:22:23 2010 +0100
8.2 +++ b/src/Pure/System/gui_setup.scala Wed Nov 17 13:39:30 2010 +0100
8.3 @@ -39,6 +39,7 @@
8.4 // values
8.5 if (Platform.is_windows)
8.6 text.append("Cygwin root: " + Cygwin.check_root() + "\n")
8.7 + text.append("JVM name: " + System.getProperty("java.vm.name") + "\n")
8.8 text.append("JVM platform: " + Platform.jvm_platform + "\n")
8.9 try {
8.10 val isabelle_system = new Isabelle_System
9.1 --- a/src/Tools/jEdit/dist-template/lib/Tools/jedit Wed Nov 17 09:22:23 2010 +0100
9.2 +++ b/src/Tools/jEdit/dist-template/lib/Tools/jedit Wed Nov 17 13:39:30 2010 +0100
9.3 @@ -24,7 +24,6 @@
9.4 echo " -m MODE add print mode for output"
9.5 echo
9.6 echo "Start jEdit with Isabelle plugin setup and opens theory FILES"
9.7 - echo "(default ~/Scratch.thy)."
9.8 echo
9.9 exit 1
9.10 }
9.11 @@ -93,14 +92,10 @@
9.12
9.13 # args
9.14
9.15 -if [ "$#" -eq 0 ]; then
9.16 - ARGS["${#ARGS[@]}"]="Scratch.thy"
9.17 -else
9.18 - while [ "$#" -gt 0 ]; do
9.19 - ARGS["${#ARGS[@]}"]="$(jvmpath "$1")"
9.20 - shift
9.21 - done
9.22 -fi
9.23 +while [ "$#" -gt 0 ]; do
9.24 + ARGS["${#ARGS[@]}"]="$(jvmpath "$1")"
9.25 + shift
9.26 +done
9.27
9.28
9.29 ## default perspective