merged
authorkuncar
Mon Mar 26 17:58:47 2012 +0200 (2012-03-26)
changeset 471182fe7a42ece1d
parent 47117 9890d4f0c1db
parent 47115 1a05adae1cc9
child 47119 81ada90d8220
merged
     1.1 --- a/Admin/build	Mon Mar 26 15:33:28 2012 +0200
     1.2 +++ b/Admin/build	Mon Mar 26 17:58:47 2012 +0200
     1.3 @@ -27,7 +27,7 @@
     1.4      browser         graph browser (requires jdk)
     1.5      doc             documentation (requires latex and rail)
     1.6      doc-src         documentation sources from Isabelle theories
     1.7 -    jars            Isabelle/Scala layer (requires Scala in \$SCALA_HOME)
     1.8 +    jars            Isabelle/Scala layer (requires \$ISABELLE_JDK_HOME and \$SCALA_HOME)
     1.9      jars_fresh      fresh build of jars
    1.10  
    1.11  EOF
     2.1 --- a/doc-src/IsarRef/Thy/Outer_Syntax.thy	Mon Mar 26 15:33:28 2012 +0200
     2.2 +++ b/doc-src/IsarRef/Thy/Outer_Syntax.thy	Mon Mar 26 17:58:47 2012 +0200
     2.3 @@ -2,7 +2,7 @@
     2.4  imports Base Main
     2.5  begin
     2.6  
     2.7 -chapter {* Outer syntax --- the theory language *}
     2.8 +chapter {* Outer syntax --- the theory language \label{ch:outer-syntax} *}
     2.9  
    2.10  text {*
    2.11    The rather generic framework of Isabelle/Isar syntax emerges from
     3.1 --- a/doc-src/IsarRef/Thy/Spec.thy	Mon Mar 26 15:33:28 2012 +0200
     3.2 +++ b/doc-src/IsarRef/Thy/Spec.thy	Mon Mar 26 17:58:47 2012 +0200
     3.3 @@ -51,9 +51,12 @@
     3.4    admissible.
     3.5  
     3.6    @{rail "
     3.7 -    @@{command theory} @{syntax name} \\ @'imports' (@{syntax name} +) uses? @'begin'
     3.8 +    @@{command theory} @{syntax name} imports \\ keywords? uses? @'begin'
     3.9      ;
    3.10 -
    3.11 +    imports: @'imports' (@{syntax name} +)
    3.12 +    ;
    3.13 +    keywords: @'keywords' ((@{syntax string} +) ('::' @{syntax name} @{syntax tags})? + @'and')
    3.14 +    ;
    3.15      uses: @'uses' ((@{syntax name} | @{syntax parname}) +)
    3.16    "}
    3.17  
    3.18 @@ -61,17 +64,28 @@
    3.19  
    3.20    \item @{command "theory"}~@{text "A \<IMPORTS> B\<^sub>1 \<dots> B\<^sub>n \<BEGIN>"}
    3.21    starts a new theory @{text A} based on the merge of existing
    3.22 -  theories @{text "B\<^sub>1 \<dots> B\<^sub>n"}.
    3.23 -  
    3.24 -  Due to the possibility to import more than one ancestor, the
    3.25 -  resulting theory structure of an Isabelle session forms a directed
    3.26 -  acyclic graph (DAG).  Isabelle's theory loader ensures that the
    3.27 -  sources contributing to the development graph are always up-to-date:
    3.28 -  changed files are automatically reloaded whenever a theory header
    3.29 -  specification is processed.
    3.30 +  theories @{text "B\<^sub>1 \<dots> B\<^sub>n"}.  Due to the possibility to import more
    3.31 +  than one ancestor, the resulting theory structure of an Isabelle
    3.32 +  session forms a directed acyclic graph (DAG).  Isabelle takes care
    3.33 +  that sources contributing to the development graph are always
    3.34 +  up-to-date: changed files are automatically rechecked whenever a
    3.35 +  theory header specification is processed.
    3.36 +
    3.37 +  The optional @{keyword_def "keywords"} specification declares outer
    3.38 +  syntax (\chref{ch:outer-syntax}) that is introduced in this theory
    3.39 +  later on (rare in end-user applications).  Both minor keywords and
    3.40 +  major keywords of the Isar command language need to be specified, in
    3.41 +  order to make parsing of proof documents work properly.  Command
    3.42 +  keywords need to be classified according to their structural role in
    3.43 +  the formal text.  Examples may be seen in Isabelle/HOL sources
    3.44 +  itself, such as @{keyword "keywords"}~@{verbatim "\"typedef\""}
    3.45 +  @{text ":: thy_goal"} or @{keyword "keywords"}~@{verbatim
    3.46 +  "\"datatype\""} @{text ":: thy_decl"} for theory-level declarations
    3.47 +  with and without proof, respectively.  Additional @{syntax tags}
    3.48 +  provide defaults for document preparation (\secref{sec:tags}).
    3.49    
    3.50    The optional @{keyword_def "uses"} specification declares additional
    3.51 -  dependencies on extra files (usually ML sources).  Files will be
    3.52 +  dependencies on external files (notably ML sources).  Files will be
    3.53    loaded immediately (as ML), unless the name is parenthesized.  The
    3.54    latter case records a dependency that needs to be resolved later in
    3.55    the text, usually via explicit @{command_ref "use"} for ML files;
    3.56 @@ -79,8 +93,10 @@
    3.57    corresponding tools or packages.
    3.58    
    3.59    \item @{command (global) "end"} concludes the current theory
    3.60 -  definition.  Note that local theory targets involve a local
    3.61 -  @{command (local) "end"}, which is clear from the nesting.
    3.62 +  definition.  Note that some other commands, e.g.\ local theory
    3.63 +  targets @{command locale} or @{command class} may involve a
    3.64 +  @{keyword "begin"} that needs to be matched by @{command (local)
    3.65 +  "end"}, according to the usual rules for nested blocks.
    3.66  
    3.67    \end{description}
    3.68  *}
     4.1 --- a/doc-src/IsarRef/Thy/document/Outer_Syntax.tex	Mon Mar 26 15:33:28 2012 +0200
     4.2 +++ b/doc-src/IsarRef/Thy/document/Outer_Syntax.tex	Mon Mar 26 17:58:47 2012 +0200
     4.3 @@ -18,7 +18,7 @@
     4.4  %
     4.5  \endisadelimtheory
     4.6  %
     4.7 -\isamarkupchapter{Outer syntax --- the theory language%
     4.8 +\isamarkupchapter{Outer syntax --- the theory language \label{ch:outer-syntax}%
     4.9  }
    4.10  \isamarkuptrue%
    4.11  %
     5.1 --- a/doc-src/IsarRef/Thy/document/Spec.tex	Mon Mar 26 15:33:28 2012 +0200
     5.2 +++ b/doc-src/IsarRef/Thy/document/Spec.tex	Mon Mar 26 17:58:47 2012 +0200
     5.3 @@ -72,18 +72,42 @@
     5.4  \rail@begin{4}{}
     5.5  \rail@term{\hyperlink{command.theory}{\mbox{\isa{\isacommand{theory}}}}}[]
     5.6  \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
     5.7 +\rail@nont{\isa{imports}}[]
     5.8  \rail@cr{2}
     5.9 -\rail@term{\isa{\isakeyword{imports}}}[]
    5.10 -\rail@plus
    5.11 -\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
    5.12 -\rail@nextplus{3}
    5.13 -\rail@endplus
    5.14 +\rail@bar
    5.15 +\rail@nextbar{3}
    5.16 +\rail@nont{\isa{keywords}}[]
    5.17 +\rail@endbar
    5.18  \rail@bar
    5.19  \rail@nextbar{3}
    5.20  \rail@nont{\isa{uses}}[]
    5.21  \rail@endbar
    5.22  \rail@term{\isa{\isakeyword{begin}}}[]
    5.23  \rail@end
    5.24 +\rail@begin{2}{\isa{imports}}
    5.25 +\rail@term{\isa{\isakeyword{imports}}}[]
    5.26 +\rail@plus
    5.27 +\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
    5.28 +\rail@nextplus{1}
    5.29 +\rail@endplus
    5.30 +\rail@end
    5.31 +\rail@begin{3}{\isa{keywords}}
    5.32 +\rail@term{\isa{\isakeyword{keywords}}}[]
    5.33 +\rail@plus
    5.34 +\rail@plus
    5.35 +\rail@nont{\hyperlink{syntax.string}{\mbox{\isa{string}}}}[]
    5.36 +\rail@nextplus{1}
    5.37 +\rail@endplus
    5.38 +\rail@bar
    5.39 +\rail@nextbar{1}
    5.40 +\rail@term{\isa{{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}}}[]
    5.41 +\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
    5.42 +\rail@nont{\hyperlink{syntax.tags}{\mbox{\isa{tags}}}}[]
    5.43 +\rail@endbar
    5.44 +\rail@nextplus{2}
    5.45 +\rail@cterm{\isa{\isakeyword{and}}}[]
    5.46 +\rail@endplus
    5.47 +\rail@end
    5.48  \rail@begin{3}{\isa{uses}}
    5.49  \rail@term{\isa{\isakeyword{uses}}}[]
    5.50  \rail@plus
    5.51 @@ -102,17 +126,27 @@
    5.52  
    5.53    \item \hyperlink{command.theory}{\mbox{\isa{\isacommand{theory}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}A\ {\isaliteral{5C3C494D504F5254533E}{\isasymIMPORTS}}\ B\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ B\isaliteral{5C3C5E7375623E}{}\isactrlsub n\ {\isaliteral{5C3C424547494E3E}{\isasymBEGIN}}{\isaliteral{22}{\isachardoublequote}}}
    5.54    starts a new theory \isa{A} based on the merge of existing
    5.55 -  theories \isa{{\isaliteral{22}{\isachardoublequote}}B\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ B\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}}.
    5.56 -  
    5.57 -  Due to the possibility to import more than one ancestor, the
    5.58 -  resulting theory structure of an Isabelle session forms a directed
    5.59 -  acyclic graph (DAG).  Isabelle's theory loader ensures that the
    5.60 -  sources contributing to the development graph are always up-to-date:
    5.61 -  changed files are automatically reloaded whenever a theory header
    5.62 -  specification is processed.
    5.63 +  theories \isa{{\isaliteral{22}{\isachardoublequote}}B\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ B\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}}.  Due to the possibility to import more
    5.64 +  than one ancestor, the resulting theory structure of an Isabelle
    5.65 +  session forms a directed acyclic graph (DAG).  Isabelle takes care
    5.66 +  that sources contributing to the development graph are always
    5.67 +  up-to-date: changed files are automatically rechecked whenever a
    5.68 +  theory header specification is processed.
    5.69 +
    5.70 +  The optional \indexdef{}{keyword}{keywords}\hypertarget{keyword.keywords}{\hyperlink{keyword.keywords}{\mbox{\isa{\isakeyword{keywords}}}}} specification declares outer
    5.71 +  syntax (\chref{ch:outer-syntax}) that is introduced in this theory
    5.72 +  later on (rare in end-user applications).  Both minor keywords and
    5.73 +  major keywords of the Isar command language need to be specified, in
    5.74 +  order to make parsing of proof documents work properly.  Command
    5.75 +  keywords need to be classified according to their structural role in
    5.76 +  the formal text.  Examples may be seen in Isabelle/HOL sources
    5.77 +  itself, such as \hyperlink{keyword.keywords}{\mbox{\isa{\isakeyword{keywords}}}}~\verb|"typedef"|
    5.78 +  \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ thy{\isaliteral{5F}{\isacharunderscore}}goal{\isaliteral{22}{\isachardoublequote}}} or \hyperlink{keyword.keywords}{\mbox{\isa{\isakeyword{keywords}}}}~\verb|"datatype"| \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ thy{\isaliteral{5F}{\isacharunderscore}}decl{\isaliteral{22}{\isachardoublequote}}} for theory-level declarations
    5.79 +  with and without proof, respectively.  Additional \hyperlink{syntax.tags}{\mbox{\isa{tags}}}
    5.80 +  provide defaults for document preparation (\secref{sec:tags}).
    5.81    
    5.82    The optional \indexdef{}{keyword}{uses}\hypertarget{keyword.uses}{\hyperlink{keyword.uses}{\mbox{\isa{\isakeyword{uses}}}}} specification declares additional
    5.83 -  dependencies on extra files (usually ML sources).  Files will be
    5.84 +  dependencies on external files (notably ML sources).  Files will be
    5.85    loaded immediately (as ML), unless the name is parenthesized.  The
    5.86    latter case records a dependency that needs to be resolved later in
    5.87    the text, usually via explicit \indexref{}{command}{use}\hyperlink{command.use}{\mbox{\isa{\isacommand{use}}}} for ML files;
    5.88 @@ -120,8 +154,9 @@
    5.89    corresponding tools or packages.
    5.90    
    5.91    \item \hyperlink{command.global.end}{\mbox{\isa{\isacommand{end}}}} concludes the current theory
    5.92 -  definition.  Note that local theory targets involve a local
    5.93 -  \hyperlink{command.local.end}{\mbox{\isa{\isacommand{end}}}}, which is clear from the nesting.
    5.94 +  definition.  Note that some other commands, e.g.\ local theory
    5.95 +  targets \hyperlink{command.locale}{\mbox{\isa{\isacommand{locale}}}} or \hyperlink{command.class}{\mbox{\isa{\isacommand{class}}}} may involve a
    5.96 +  \hyperlink{keyword.begin}{\mbox{\isa{\isakeyword{begin}}}} that needs to be matched by \hyperlink{command.local.end}{\mbox{\isa{\isacommand{end}}}}, according to the usual rules for nested blocks.
    5.97  
    5.98    \end{description}%
    5.99  \end{isamarkuptext}%
     6.1 --- a/lib/Tools/java	Mon Mar 26 15:33:28 2012 +0200
     6.2 +++ b/lib/Tools/java	Mon Mar 26 17:58:47 2012 +0200
     6.3 @@ -6,21 +6,12 @@
     6.4  
     6.5  CLASSPATH="$(jvmpath "$CLASSPATH")"
     6.6  
     6.7 -JAVA_EXE="$ISABELLE_JDK_HOME/bin/java"
     6.8 -
     6.9 -if "$JAVA_EXE" -version >/dev/null 2>/dev/null; then
    6.10 -  :
    6.11 -else
    6.12 -  echo "Bad Java executable: \"$JAVA_EXE\"" >&2
    6.13 -  exit 2
    6.14 -fi
    6.15 -
    6.16 -if "$JAVA_EXE" -server >/dev/null 2>/dev/null; then
    6.17 +if isabelle_jdk java -server >/dev/null 2>/dev/null; then
    6.18    SERVER="-server"
    6.19  else
    6.20    SERVER=""
    6.21  fi
    6.22  
    6.23 -exec "$JAVA_EXE" -Dfile.encoding=UTF-8 $SERVER \
    6.24 +exec "$ISABELLE_JDK_HOME/bin/java" -Dfile.encoding=UTF-8 $SERVER \
    6.25    "-Djava.ext.dirs=$("$ISABELLE_HOME/src/Tools/JVM/java_ext_dirs")" "$@"
    6.26  
     7.1 --- a/lib/Tools/scala	Mon Mar 26 15:33:28 2012 +0200
     7.2 +++ b/lib/Tools/scala	Mon Mar 26 17:58:47 2012 +0200
     7.3 @@ -4,10 +4,8 @@
     7.4  #
     7.5  # DESCRIPTION: invoke Scala within the Isabelle environment
     7.6  
     7.7 -[ -z "$SCALA_HOME" ] && { echo "Unknown SCALA_HOME -- Scala unavailable"; exit 2; }
     7.8 -
     7.9  [ -e "$ISABELLE_HOME/Admin/build" ] && { "$ISABELLE_HOME/Admin/build" jars || exit $?; }
    7.10  
    7.11  CLASSPATH="$(jvmpath "$CLASSPATH")"
    7.12 -exec "$SCALA_HOME/bin/scala" -Dfile.encoding=UTF-8 \
    7.13 +isabelle_scala scala -Dfile.encoding=UTF-8 \
    7.14    "-Djava.ext.dirs=$("$ISABELLE_HOME/src/Tools/JVM/java_ext_dirs")" "$@"
     8.1 --- a/lib/Tools/scalac	Mon Mar 26 15:33:28 2012 +0200
     8.2 +++ b/lib/Tools/scalac	Mon Mar 26 17:58:47 2012 +0200
     8.3 @@ -4,10 +4,8 @@
     8.4  #
     8.5  # DESCRIPTION: invoke Scala compiler within the Isabelle environment
     8.6  
     8.7 -[ -z "$SCALA_HOME" ] && { echo "Unknown SCALA_HOME -- Scala unavailable"; exit 2; }
     8.8 -
     8.9  [ -e "$ISABELLE_HOME/Admin/build" ] && { "$ISABELLE_HOME/Admin/build" jars || exit $?; }
    8.10  
    8.11  CLASSPATH="$(jvmpath "$CLASSPATH")"
    8.12 -exec "$SCALA_HOME/bin/scalac" -Dfile.encoding=UTF-8 \
    8.13 +isabelle_scala scalac -Dfile.encoding=UTF-8 \
    8.14    "-Djava.ext.dirs=$("$ISABELLE_HOME/src/Tools/JVM/java_ext_dirs")" "$@"
     9.1 --- a/lib/browser/build	Mon Mar 26 15:33:28 2012 +0200
     9.2 +++ b/lib/browser/build	Mon Mar 26 17:58:47 2012 +0200
     9.3 @@ -65,9 +65,9 @@
     9.4  
     9.5    rm -rf classes && mkdir classes
     9.6  
     9.7 -  "$ISABELLE_JDK_HOME/bin/javac" -d classes -source 1.4 "${SOURCES[@]}" || \
     9.8 +  isabelle_jdk javac -d classes -source 1.4 "${SOURCES[@]}" || \
     9.9      fail "Failed to compile sources"
    9.10 -  "$ISABELLE_JDK_HOME/bin/jar" cf "$(jvmpath "$TARGET")" -C classes . ||
    9.11 +  isabelle_jdk jar cf "$(jvmpath "$TARGET")" -C classes . ||
    9.12      fail "Failed to produce $TARGET"
    9.13  
    9.14    rm -rf classes
    10.1 --- a/lib/scripts/getsettings	Mon Mar 26 15:33:28 2012 +0200
    10.2 +++ b/lib/scripts/getsettings	Mon Mar 26 17:58:47 2012 +0200
    10.3 @@ -89,6 +89,22 @@
    10.4    done
    10.5  }
    10.6  
    10.7 +#robust invocation via ISABELLE_JDK_HOME
    10.8 +function isabelle_jdk () {
    10.9 +  [ -z "$ISABELLE_JDK_HOME" ] && \
   10.10 +    { echo "Unknown ISABELLE_JDK_HOME -- Java tools unavailable"; exit 2; }
   10.11 +  local PRG="$1"; shift
   10.12 +  "$ISABELLE_JDK_HOME/bin/$PRG" "$@"
   10.13 +}
   10.14 +
   10.15 +#robust invocation via SCALA_HOME
   10.16 +function isabelle_scala () {
   10.17 +  [ -z "$SCALA_HOME" ] && \
   10.18 +    { echo "Unknown SCALA_HOME -- Scala unavailable"; exit 2; }
   10.19 +  local PRG="$1"; shift
   10.20 +  "$SCALA_HOME/bin/$PRG" "$@"
   10.21 +}
   10.22 +
   10.23  #CLASSPATH convenience
   10.24  function classpath () {
   10.25    for X in "$@"
    11.1 --- a/src/Pure/build-jars	Mon Mar 26 15:33:28 2012 +0200
    11.2 +++ b/src/Pure/build-jars	Mon Mar 26 17:58:47 2012 +0200
    11.3 @@ -88,7 +88,6 @@
    11.4  }
    11.5  
    11.6  [ -z "$ISABELLE_HOME" ] && fail "Missing Isabelle settings environment"
    11.7 -[ -z "$SCALA_HOME" ] && fail "Unknown SCALA_HOME -- Scala unavailable"
    11.8  
    11.9  
   11.10  ## process command line
   11.11 @@ -172,10 +171,10 @@
   11.12  
   11.13    SCALAC_OPTIONS="$ISABELLE_SCALA_BUILD_OPTIONS -d classes"
   11.14  
   11.15 -  "$SCALA_HOME/bin/scalac" $SCALAC_OPTIONS "${PIDE_SOURCES[@]}" || \
   11.16 +  isabelle_scala scalac $SCALAC_OPTIONS "${PIDE_SOURCES[@]}" || \
   11.17      fail "Failed to compile PIDE sources"
   11.18  
   11.19 -  "$SCALA_HOME/bin/scalac" $SCALAC_OPTIONS -classpath classes "${PURE_SOURCES[@]}" || \
   11.20 +  isabelle_scala scalac $SCALAC_OPTIONS -classpath classes "${PURE_SOURCES[@]}" || \
   11.21      fail "Failed to compile Pure sources"
   11.22  
   11.23    mkdir -p "$TARGET_DIR/ext" || fail "Failed to create directory $TARGET_DIR/ext"
   11.24 @@ -186,7 +185,7 @@
   11.25    mkdir -p "$(dirname "$CHARSET_SERVICE")"
   11.26    echo isabelle.Isabelle_Charset_Provider > "$CHARSET_SERVICE"
   11.27  
   11.28 -  "$ISABELLE_JDK_HOME/bin/jar" cfe "$(jvmpath "$TARGET")" isabelle.GUI_Setup META-INF isabelle || \
   11.29 +  isabelle_jdk jar cfe "$(jvmpath "$TARGET")" isabelle.GUI_Setup META-INF isabelle || \
   11.30      fail "Failed to produce $TARGET"
   11.31  
   11.32    cp "$SCALA_HOME/lib/scala-swing.jar" "$SCALA_HOME/lib/scala-library.jar" "$TARGET_DIR/ext"
    12.1 --- a/src/Tools/JVM/java_ext_dirs	Mon Mar 26 15:33:28 2012 +0200
    12.2 +++ b/src/Tools/JVM/java_ext_dirs	Mon Mar 26 17:58:47 2012 +0200
    12.3 @@ -17,7 +17,7 @@
    12.4  
    12.5  ## main
    12.6  
    12.7 -exec "$ISABELLE_JDK_HOME/bin/java" \
    12.8 +isabelle_jdk java \
    12.9    -classpath "$(jvmpath "$ISABELLE_HOME/src/Tools/JVM/java_ext_dirs.jar")" \
   12.10    isabelle.Java_Ext_Dirs "$(jvmpath "$ISABELLE_HOME/lib/classes/ext")"
   12.11  
    13.1 --- a/src/Tools/jEdit/lib/Tools/jedit	Mon Mar 26 15:33:28 2012 +0200
    13.2 +++ b/src/Tools/jEdit/lib/Tools/jedit	Mon Mar 26 17:58:47 2012 +0200
    13.3 @@ -248,7 +248,7 @@
    13.4    ) || fail "Failed to compile sources"
    13.5  
    13.6    cd dist/classes
    13.7 -  "$ISABELLE_JDK_HOME/bin/jar" cf "../jars/Isabelle-jEdit.jar" * || failed
    13.8 +  isabelle_jdk jar cf "../jars/Isabelle-jEdit.jar" * || failed
    13.9    cd ../..
   13.10    rm -rf dist/classes
   13.11  fi