# HG changeset patch
# User wenzelm
# Date 1289997570 -3600
# Node ID 4e10046d7aaa471183e4e9f4f7c31cf0d1db9d5e
# Parent  0592d3a39c085d0c327d5e1cfb0a20cf956f39b8# Parent  2265638295805a7b3eef36d0c4a0fe40803a11ce
merged

diff -r 0592d3a39c08 -r 4e10046d7aaa Admin/makedist
--- 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"
diff -r 0592d3a39c08 -r 4e10046d7aaa Isabelle
--- 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")" "$@"
diff -r 0592d3a39c08 -r 4e10046d7aaa doc-src/System/Thy/Basics.thy
--- 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}
 *}
 
 
diff -r 0592d3a39c08 -r 4e10046d7aaa doc-src/System/Thy/document/Basics.tex
--- 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%
 %
diff -r 0592d3a39c08 -r 4e10046d7aaa etc/settings
--- 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"
 
diff -r 0592d3a39c08 -r 4e10046d7aaa lib/scripts/getsettings
--- 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\""
diff -r 0592d3a39c08 -r 4e10046d7aaa src/Pure/PIDE/command.scala
--- 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 {
diff -r 0592d3a39c08 -r 4e10046d7aaa src/Pure/System/gui_setup.scala
--- 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
diff -r 0592d3a39c08 -r 4e10046d7aaa src/Tools/jEdit/dist-template/lib/Tools/jedit
--- 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