merged
authorwenzelm
Sun Apr 22 16:33:41 2012 +0200 (2012-04-22)
changeset 47673dd253cfa5b23
parent 47672 1bf4fa90cd03
parent 47666 cf5fe7eb6793
child 47674 cdf95042e09c
child 47677 4977297873a2
merged
NEWS
     1.1 --- a/Admin/launch4j/isabelle.xml	Sun Apr 22 14:16:46 2012 +0200
     1.2 +++ b/Admin/launch4j/isabelle.xml	Sun Apr 22 16:33:41 2012 +0200
     1.3 @@ -1,23 +1,29 @@
     1.4  <launch4jConfig>
     1.5    <dontWrapJar>true</dontWrapJar>
     1.6    <headerType>gui</headerType>
     1.7 -  <jar>lib\classes\isabelle-scala.jar</jar>
     1.8 +  <jar></jar>
     1.9    <outfile>Isabelle.exe</outfile>
    1.10    <errTitle></errTitle>
    1.11    <cmdLine></cmdLine>
    1.12    <chdir></chdir>
    1.13    <priority>normal</priority>
    1.14 -  <downloadUrl>http://java.com/download</downloadUrl>
    1.15 +  <downloadUrl></downloadUrl>
    1.16    <supportUrl></supportUrl>
    1.17    <customProcName>false</customProcName>
    1.18    <stayAlive>true</stayAlive>
    1.19    <manifest></manifest>
    1.20    <icon>isabelle.ico</icon>
    1.21 +  <classPath>
    1.22 +    <mainClass>isabelle.Main</mainClass>
    1.23 +    <cp>lib\classes\ext\Pure.jar</cp>
    1.24 +    <cp>lib\classes\ext\scala-library.jar</cp>
    1.25 +    <cp>lib\classes\ext\scala-swing.jar</cp>
    1.26 +  </classPath>
    1.27    <jre>
    1.28 -    <path></path>
    1.29 -    <minVersion>1.6.0</minVersion>
    1.30 +    <path>contrib\jdk-7u3_x86-cygwin\jdk1.7.0_03</path>
    1.31 +    <minVersion></minVersion>
    1.32      <maxVersion></maxVersion>
    1.33 -    <jdkPreference>preferJre</jdkPreference>
    1.34 +    <jdkPreference>jdkOnly</jdkPreference>
    1.35      <opt>-Disabelle.home=&quot;%EXEDIR%&quot;</opt>
    1.36    </jre>
    1.37  </launch4jConfig>
    1.38 \ No newline at end of file
     2.1 --- a/NEWS	Sun Apr 22 14:16:46 2012 +0200
     2.2 +++ b/NEWS	Sun Apr 22 16:33:41 2012 +0200
     2.3 @@ -869,6 +869,14 @@
     2.4  
     2.5  *** System ***
     2.6  
     2.7 +* USER_HOME settings variable points to cross-platform user home
     2.8 +directory, which coincides with HOME on POSIX systems only.  Likewise,
     2.9 +the Isabelle path specification "~" now expands to $USER_HOME, instead
    2.10 +of former $HOME.  A different default for USER_HOME may be set
    2.11 +explicitly in shell environment, before Isabelle settings are
    2.12 +evaluated.  Minor INCOMPATIBILITY: need to adapt Isabelle path where
    2.13 +the generic user home was intended.
    2.14 +
    2.15  * ISABELLE_JDK_HOME settings variable points to JDK with javac and jar
    2.16  (not just JRE).
    2.17  
     3.1 --- a/doc-src/IsarRef/Thy/Misc.thy	Sun Apr 22 14:16:46 2012 +0200
     3.2 +++ b/doc-src/IsarRef/Thy/Misc.thy	Sun Apr 22 16:33:41 2012 +0200
     3.3 @@ -143,9 +143,9 @@
     3.4    %FIXME proper place (!?)
     3.5    Isabelle file specification may contain path variables (e.g.\
     3.6    @{verbatim "$ISABELLE_HOME"}) that are expanded accordingly.  Note
     3.7 -  that @{verbatim "~"} abbreviates @{verbatim "$HOME"}, and @{verbatim
     3.8 -  "~~"} abbreviates @{verbatim "$ISABELLE_HOME"}.  The general syntax
     3.9 -  for path specifications follows POSIX conventions.
    3.10 +  that @{verbatim "~"} abbreviates @{verbatim "$USER_HOME"}, and
    3.11 +  @{verbatim "~~"} abbreviates @{verbatim "$ISABELLE_HOME"}.  The
    3.12 +  general syntax for path specifications follows POSIX conventions.
    3.13  *}
    3.14  
    3.15  end
     4.1 --- a/doc-src/IsarRef/Thy/document/Misc.tex	Sun Apr 22 14:16:46 2012 +0200
     4.2 +++ b/doc-src/IsarRef/Thy/document/Misc.tex	Sun Apr 22 16:33:41 2012 +0200
     4.3 @@ -256,8 +256,9 @@
     4.4    %FIXME proper place (!?)
     4.5    Isabelle file specification may contain path variables (e.g.\
     4.6    \verb|$ISABELLE_HOME|) that are expanded accordingly.  Note
     4.7 -  that \verb|~| abbreviates \verb|$HOME|, and \verb|~~| abbreviates \verb|$ISABELLE_HOME|.  The general syntax
     4.8 -  for path specifications follows POSIX conventions.%
     4.9 +  that \verb|~| abbreviates \verb|$USER_HOME|, and
    4.10 +  \verb|~~| abbreviates \verb|$ISABELLE_HOME|.  The
    4.11 +  general syntax for path specifications follows POSIX conventions.%
    4.12  \end{isamarkuptext}%
    4.13  \isamarkuptrue%
    4.14  %
     5.1 --- a/doc-src/System/Thy/Basics.thy	Sun Apr 22 14:16:46 2012 +0200
     5.2 +++ b/doc-src/System/Thy/Basics.thy	Sun Apr 22 16:33:41 2012 +0200
     5.3 @@ -96,7 +96,7 @@
     5.4    exists) is run in the same way as the site default settings. Note
     5.5    that the variable @{setting ISABELLE_HOME_USER} has already been set
     5.6    before --- usually to something like @{verbatim
     5.7 -  "$HOME/.isabelle/IsabelleXXXX"}.
     5.8 +  "$USER_HOME/.isabelle/IsabelleXXXX"}.
     5.9    
    5.10    Thus individual users may override the site-wide defaults.  See also
    5.11    file @{file "$ISABELLE_HOME/etc/user-settings.sample"} in the
    5.12 @@ -149,19 +149,24 @@
    5.13  
    5.14    \begin{description}
    5.15  
    5.16 -  \item[@{setting_def ISABELLE_HOME}@{text "\<^sup>*"}] is the
    5.17 -  location of the top-level Isabelle distribution directory. This is
    5.18 -  automatically determined from the Isabelle executable that has been
    5.19 -  invoked.  Do not attempt to set @{setting ISABELLE_HOME} yourself
    5.20 -  from the shell!
    5.21 +  \item[@{setting_def USER_HOME}@{text "\<^sup>*"}] Is the
    5.22 +  cross-platform user home directory.  On Unix systems this is usually
    5.23 +  the same as @{setting HOME}, but on Windows it is the regular home
    5.24 +  directory of the user, not the one of within the Cygwin root
    5.25 +  file-system.
    5.26 +
    5.27 + \item[@{setting_def ISABELLE_HOME}@{text "\<^sup>*"}] is the location of the
    5.28 +  top-level Isabelle distribution directory. This is automatically
    5.29 +  determined from the Isabelle executable that has been invoked.  Do
    5.30 +  not attempt to set @{setting ISABELLE_HOME} yourself from the shell!
    5.31    
    5.32    \item[@{setting_def ISABELLE_HOME_USER}] is the user-specific
    5.33    counterpart of @{setting ISABELLE_HOME}. The default value is
    5.34 -  relative to @{verbatim "$HOME/.isabelle"}, under rare circumstances
    5.35 -  this may be changed in the global setting file.  Typically, the
    5.36 -  @{setting ISABELLE_HOME_USER} directory mimics @{setting
    5.37 -  ISABELLE_HOME} to some extend. In particular, site-wide defaults may
    5.38 -  be overridden by a private @{verbatim
    5.39 +  relative to @{verbatim "$USER_HOME/.isabelle"}, under rare
    5.40 +  circumstances this may be changed in the global setting file.
    5.41 +  Typically, the @{setting ISABELLE_HOME_USER} directory mimics
    5.42 +  @{setting ISABELLE_HOME} to some extend. In particular, site-wide
    5.43 +  defaults may be overridden by a private @{verbatim
    5.44    "$ISABELLE_HOME_USER/etc/settings"}.
    5.45    
    5.46    \item[@{setting_def ISABELLE_PLATFORM}@{text "\<^sup>*"}] is automatically
     6.1 --- a/doc-src/System/Thy/document/Basics.tex	Sun Apr 22 14:16:46 2012 +0200
     6.2 +++ b/doc-src/System/Thy/document/Basics.tex	Sun Apr 22 16:33:41 2012 +0200
     6.3 @@ -114,7 +114,7 @@
     6.4    \item The file \verb|$ISABELLE_HOME_USER/etc/settings| (if it
     6.5    exists) is run in the same way as the site default settings. Note
     6.6    that the variable \hyperlink{setting.ISABELLE-HOME-USER}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}HOME{\isaliteral{5F}{\isacharunderscore}}USER}}}} has already been set
     6.7 -  before --- usually to something like \verb|$HOME/.isabelle/IsabelleXXXX|.
     6.8 +  before --- usually to something like \verb|$USER_HOME/.isabelle/IsabelleXXXX|.
     6.9    
    6.10    Thus individual users may override the site-wide defaults.  See also
    6.11    file \verb|$ISABELLE_HOME/etc/user-settings.sample| in the
    6.12 @@ -167,18 +167,23 @@
    6.13  
    6.14    \begin{description}
    6.15  
    6.16 -  \item[\indexdef{}{setting}{ISABELLE\_HOME}\hypertarget{setting.ISABELLE-HOME}{\hyperlink{setting.ISABELLE-HOME}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}HOME}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}}] is the
    6.17 -  location of the top-level Isabelle distribution directory. This is
    6.18 -  automatically determined from the Isabelle executable that has been
    6.19 -  invoked.  Do not attempt to set \hyperlink{setting.ISABELLE-HOME}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}HOME}}}} yourself
    6.20 -  from the shell!
    6.21 +  \item[\indexdef{}{setting}{USER\_HOME}\hypertarget{setting.USER-HOME}{\hyperlink{setting.USER-HOME}{\mbox{\isa{\isatt{USER{\isaliteral{5F}{\isacharunderscore}}HOME}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}}] Is the cross-platform
    6.22 +  user home directory.  On Unix systems this is usually the same as
    6.23 +  \hyperlink{setting.HOME}{\mbox{\isa{\isatt{HOME}}}}, but on Windows it is the regular home directory of
    6.24 +  the, not the one of within the Cygwin root file-system.
    6.25 +
    6.26 + \item[\indexdef{}{setting}{ISABELLE\_HOME}\hypertarget{setting.ISABELLE-HOME}{\hyperlink{setting.ISABELLE-HOME}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}HOME}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}}] is the location of the
    6.27 +  top-level Isabelle distribution directory. This is automatically
    6.28 +  determined from the Isabelle executable that has been invoked.  Do
    6.29 +  not attempt to set \hyperlink{setting.ISABELLE-HOME}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}HOME}}}} yourself from the shell!
    6.30    
    6.31    \item[\indexdef{}{setting}{ISABELLE\_HOME\_USER}\hypertarget{setting.ISABELLE-HOME-USER}{\hyperlink{setting.ISABELLE-HOME-USER}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}HOME{\isaliteral{5F}{\isacharunderscore}}USER}}}}}] is the user-specific
    6.32    counterpart of \hyperlink{setting.ISABELLE-HOME}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}HOME}}}}. The default value is
    6.33 -  relative to \verb|$HOME/.isabelle|, under rare circumstances
    6.34 -  this may be changed in the global setting file.  Typically, the
    6.35 -  \hyperlink{setting.ISABELLE-HOME-USER}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}HOME{\isaliteral{5F}{\isacharunderscore}}USER}}}} directory mimics \hyperlink{setting.ISABELLE-HOME}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}HOME}}}} to some extend. In particular, site-wide defaults may
    6.36 -  be overridden by a private \verb|$ISABELLE_HOME_USER/etc/settings|.
    6.37 +  relative to \verb|$USER_HOME/.isabelle|, under rare
    6.38 +  circumstances this may be changed in the global setting file.
    6.39 +  Typically, the \hyperlink{setting.ISABELLE-HOME-USER}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}HOME{\isaliteral{5F}{\isacharunderscore}}USER}}}} directory mimics
    6.40 +  \hyperlink{setting.ISABELLE-HOME}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}HOME}}}} to some extend. In particular, site-wide
    6.41 +  defaults may be overridden by a private \verb|$ISABELLE_HOME_USER/etc/settings|.
    6.42    
    6.43    \item[\indexdef{}{setting}{ISABELLE\_PLATFORM}\hypertarget{setting.ISABELLE-PLATFORM}{\hyperlink{setting.ISABELLE-PLATFORM}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}PLATFORM}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}}] is automatically
    6.44    set to a symbolic identifier for the underlying hardware and
     7.1 --- a/etc/settings	Sun Apr 22 14:16:46 2012 +0200
     7.2 +++ b/etc/settings	Sun Apr 22 16:33:41 2012 +0200
     7.3 @@ -93,7 +93,7 @@
     7.4  ###
     7.5  
     7.6  # The place for user configuration, heap files, etc.
     7.7 -ISABELLE_HOME_USER="$HOME/.isabelle/${ISABELLE_IDENTIFIER:-.}"
     7.8 +ISABELLE_HOME_USER="$USER_HOME/.isabelle/${ISABELLE_IDENTIFIER:-.}"
     7.9  
    7.10  # Where to look for isabelle tools (multiple dirs separated by ':').
    7.11  ISABELLE_TOOLS="$ISABELLE_HOME/lib/Tools"
     8.1 --- a/lib/scripts/getsettings	Sun Apr 22 14:16:46 2012 +0200
     8.2 +++ b/lib/scripts/getsettings	Sun Apr 22 16:33:41 2012 +0200
     8.3 @@ -11,9 +11,13 @@
     8.4  
     8.5  ISABELLE_SETTINGS_PRESENT=true
     8.6  
     8.7 -#JVM path wrapper
     8.8 +#Cygwin vs Posix
     8.9  if [ "$OSTYPE" = cygwin ]
    8.10  then
    8.11 +  if [ -z "$USER_HOME" ]; then
    8.12 +    USER_HOME="$(cygpath -u "$HOMEDRIVE\\$HOMEPATH")"
    8.13 +  fi
    8.14 +
    8.15    ISABELLE_HOME_WINDOWS="$(cygpath -w "$(dirname "$ISABELLE_HOME")")\\$(basename "$ISABELLE_HOME")"
    8.16    ISABELLE_HOME="$(cygpath -u "$ISABELLE_HOME_WINDOWS")"
    8.17  
    8.18 @@ -21,10 +25,13 @@
    8.19    function jvmpath() { cygpath -i -C UTF8 -w -p "$@"; }
    8.20    THIS_CYGWIN="$(jvmpath "/")"
    8.21  else
    8.22 +  if [ -z "$USER_HOME" ]; then
    8.23 +    USER_HOME="$HOME"
    8.24 +  fi
    8.25 +
    8.26    function jvmpath() { echo "$@"; }
    8.27    CLASSPATH="$CLASSPATH"
    8.28  fi
    8.29 -HOME_JVM="$HOME"
    8.30  
    8.31  export ISABELLE_HOME
    8.32  if { echo -n "$ISABELLE_HOME" | fgrep " " >/dev/null; }
     9.1 --- a/src/Pure/General/path.ML	Sun Apr 22 14:16:46 2012 +0200
     9.2 +++ b/src/Pure/General/path.ML	Sun Apr 22 16:33:41 2012 +0200
     9.3 @@ -127,7 +127,7 @@
     9.4  local
     9.5  
     9.6  fun explode_elem ".." = Parent
     9.7 -  | explode_elem "~" = Variable "HOME"
     9.8 +  | explode_elem "~" = Variable "USER_HOME"
     9.9    | explode_elem "~~" = Variable "ISABELLE_HOME"
    9.10    | explode_elem s =
    9.11        (case raw_explode s of
    10.1 --- a/src/Pure/General/path.scala	Sun Apr 22 14:16:46 2012 +0200
    10.2 +++ b/src/Pure/General/path.scala	Sun Apr 22 16:33:41 2012 +0200
    10.3 @@ -72,7 +72,7 @@
    10.4  
    10.5    private def explode_elem(s: String): Elem =
    10.6      if (s == "..") Parent
    10.7 -    else if (s == "~") Variable("HOME")
    10.8 +    else if (s == "~") Variable("USER_HOME")
    10.9      else if (s == "~~") Variable("ISABELLE_HOME")
   10.10      else if (s.startsWith("$")) variable_elem(s.substring(1))
   10.11      else basic_elem(s)
    11.1 --- a/src/Pure/System/isabelle_system.scala	Sun Apr 22 14:16:46 2012 +0200
    11.2 +++ b/src/Pure/System/isabelle_system.scala	Sun Apr 22 16:33:41 2012 +0200
    11.3 @@ -79,9 +79,7 @@
    11.4                    if (i <= 0) (entry -> "")
    11.5                    else (entry.substring(0, i) -> entry.substring(i + 1))
    11.6                  }
    11.7 -              Map(entries: _*) +
    11.8 -                ("HOME" -> System.getenv("HOME")) +
    11.9 -                ("PATH" -> System.getenv("PATH"))
   11.10 +              Map(entries: _*) + ("PATH" -> System.getenv("PATH"))
   11.11              }
   11.12            }
   11.13        _state = Some(State(standard_system, settings))
   11.14 @@ -91,8 +89,7 @@
   11.15  
   11.16    /* getenv */
   11.17  
   11.18 -  def getenv(name: String): String =
   11.19 -    settings.getOrElse(if (name == "HOME") "HOME_JVM" else name, "")
   11.20 +  def getenv(name: String): String = settings.getOrElse(name, "")
   11.21  
   11.22    def getenv_strict(name: String): String =
   11.23    {
    12.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    12.2 +++ b/src/Pure/System/main.scala	Sun Apr 22 16:33:41 2012 +0200
    12.3 @@ -0,0 +1,33 @@
    12.4 +/*  Title:      Pure/System/main.scala
    12.5 +    Author:     Makarius
    12.6 +
    12.7 +Default Isabelle application wrapper.
    12.8 +*/
    12.9 +
   12.10 +package isabelle
   12.11 +
   12.12 +import scala.swing.TextArea
   12.13 +
   12.14 +
   12.15 +object Main
   12.16 +{
   12.17 +  def main(args: Array[String]) =
   12.18 +  {
   12.19 +    val (out, rc) =
   12.20 +      try {
   12.21 +        Platform.init_laf()
   12.22 +        Isabelle_System.init()
   12.23 +        Isabelle_System.isabelle_tool("jedit", args: _*)
   12.24 +      }
   12.25 +      catch { case exn: Throwable => (Exn.message(exn), 2) }
   12.26 +
   12.27 +    if (rc != 0) {
   12.28 +      val text = new TextArea(out + "\nReturn code: " + rc)
   12.29 +      text.editable = false
   12.30 +      Library.dialog(null, "Isabelle", "Isabelle output", text)
   12.31 +    }
   12.32 +
   12.33 +    System.exit(rc)
   12.34 +  }
   12.35 +}
   12.36 +
    13.1 --- a/src/Pure/build-jars	Sun Apr 22 14:16:46 2012 +0200
    13.2 +++ b/src/Pure/build-jars	Sun Apr 22 16:33:41 2012 +0200
    13.3 @@ -47,6 +47,7 @@
    13.4    System/isabelle_charset.scala
    13.5    System/isabelle_process.scala
    13.6    System/isabelle_system.scala
    13.7 +  System/main.scala
    13.8    System/platform.scala
    13.9    System/session.scala
   13.10    System/session_manager.scala
    14.1 --- a/src/Tools/jEdit/lib/Tools/jedit	Sun Apr 22 14:16:46 2012 +0200
    14.2 +++ b/src/Tools/jEdit/lib/Tools/jedit	Sun Apr 22 16:33:41 2012 +0200
    14.3 @@ -189,8 +189,10 @@
    14.4    else
    14.5      if [ -n "$ISABELLE_JEDIT_BUILD_HOME" ]; then
    14.6        declare -a DEPS=("$JEDIT_JAR" "${JEDIT_JARS[@]}" "$PURE_JAR" "${SOURCES[@]}" "${RESOURCES[@]}")
    14.7 +    elif [ -e "$ISABELLE_HOME/Admin/build" ]; then
    14.8 +      declare -a DEPS=("$PURE_JAR" "${SOURCES[@]}" "${RESOURCES[@]}")
    14.9      else
   14.10 -      declare -a DEPS=("$PURE_JAR" "${SOURCES[@]}" "${RESOURCES[@]}")
   14.11 +      declare -a DEPS=()
   14.12      fi
   14.13      for DEP in "${DEPS[@]}"
   14.14      do