# HG changeset patch # User kuncar # Date 1332777527 -7200 # Node ID 2fe7a42ece1dc4ed718b6d869c516cc2d70ef630 # Parent 9890d4f0c1db02fde9d259901c0c19827c7fe790# Parent 1a05adae1cc951aae9ef455732a108f5663e28c6 merged diff -r 9890d4f0c1db -r 2fe7a42ece1d Admin/build --- a/Admin/build Mon Mar 26 15:33:28 2012 +0200 +++ b/Admin/build Mon Mar 26 17:58:47 2012 +0200 @@ -27,7 +27,7 @@ browser graph browser (requires jdk) doc documentation (requires latex and rail) doc-src documentation sources from Isabelle theories - jars Isabelle/Scala layer (requires Scala in \$SCALA_HOME) + jars Isabelle/Scala layer (requires \$ISABELLE_JDK_HOME and \$SCALA_HOME) jars_fresh fresh build of jars EOF diff -r 9890d4f0c1db -r 2fe7a42ece1d doc-src/IsarRef/Thy/Outer_Syntax.thy --- a/doc-src/IsarRef/Thy/Outer_Syntax.thy Mon Mar 26 15:33:28 2012 +0200 +++ b/doc-src/IsarRef/Thy/Outer_Syntax.thy Mon Mar 26 17:58:47 2012 +0200 @@ -2,7 +2,7 @@ imports Base Main begin -chapter {* Outer syntax --- the theory language *} +chapter {* Outer syntax --- the theory language \label{ch:outer-syntax} *} text {* The rather generic framework of Isabelle/Isar syntax emerges from diff -r 9890d4f0c1db -r 2fe7a42ece1d doc-src/IsarRef/Thy/Spec.thy --- a/doc-src/IsarRef/Thy/Spec.thy Mon Mar 26 15:33:28 2012 +0200 +++ b/doc-src/IsarRef/Thy/Spec.thy Mon Mar 26 17:58:47 2012 +0200 @@ -51,9 +51,12 @@ admissible. @{rail " - @@{command theory} @{syntax name} \\ @'imports' (@{syntax name} +) uses? @'begin' + @@{command theory} @{syntax name} imports \\ keywords? uses? @'begin' ; - + imports: @'imports' (@{syntax name} +) + ; + keywords: @'keywords' ((@{syntax string} +) ('::' @{syntax name} @{syntax tags})? + @'and') + ; uses: @'uses' ((@{syntax name} | @{syntax parname}) +) "} @@ -61,17 +64,28 @@ \item @{command "theory"}~@{text "A \ B\<^sub>1 \ B\<^sub>n \"} starts a new theory @{text A} based on the merge of existing - theories @{text "B\<^sub>1 \ B\<^sub>n"}. - - Due to the possibility to import more than one ancestor, the - resulting theory structure of an Isabelle session forms a directed - acyclic graph (DAG). Isabelle's theory loader ensures that the - sources contributing to the development graph are always up-to-date: - changed files are automatically reloaded whenever a theory header - specification is processed. + theories @{text "B\<^sub>1 \ B\<^sub>n"}. Due to the possibility to import more + than one ancestor, the resulting theory structure of an Isabelle + session forms a directed acyclic graph (DAG). Isabelle takes care + that sources contributing to the development graph are always + up-to-date: changed files are automatically rechecked whenever a + theory header specification is processed. + + The optional @{keyword_def "keywords"} specification declares outer + syntax (\chref{ch:outer-syntax}) that is introduced in this theory + later on (rare in end-user applications). Both minor keywords and + major keywords of the Isar command language need to be specified, in + order to make parsing of proof documents work properly. Command + keywords need to be classified according to their structural role in + the formal text. Examples may be seen in Isabelle/HOL sources + itself, such as @{keyword "keywords"}~@{verbatim "\"typedef\""} + @{text ":: thy_goal"} or @{keyword "keywords"}~@{verbatim + "\"datatype\""} @{text ":: thy_decl"} for theory-level declarations + with and without proof, respectively. Additional @{syntax tags} + provide defaults for document preparation (\secref{sec:tags}). The optional @{keyword_def "uses"} specification declares additional - dependencies on extra files (usually ML sources). Files will be + dependencies on external files (notably ML sources). Files will be loaded immediately (as ML), unless the name is parenthesized. The latter case records a dependency that needs to be resolved later in the text, usually via explicit @{command_ref "use"} for ML files; @@ -79,8 +93,10 @@ corresponding tools or packages. \item @{command (global) "end"} concludes the current theory - definition. Note that local theory targets involve a local - @{command (local) "end"}, which is clear from the nesting. + definition. Note that some other commands, e.g.\ local theory + targets @{command locale} or @{command class} may involve a + @{keyword "begin"} that needs to be matched by @{command (local) + "end"}, according to the usual rules for nested blocks. \end{description} *} diff -r 9890d4f0c1db -r 2fe7a42ece1d doc-src/IsarRef/Thy/document/Outer_Syntax.tex --- a/doc-src/IsarRef/Thy/document/Outer_Syntax.tex Mon Mar 26 15:33:28 2012 +0200 +++ b/doc-src/IsarRef/Thy/document/Outer_Syntax.tex Mon Mar 26 17:58:47 2012 +0200 @@ -18,7 +18,7 @@ % \endisadelimtheory % -\isamarkupchapter{Outer syntax --- the theory language% +\isamarkupchapter{Outer syntax --- the theory language \label{ch:outer-syntax}% } \isamarkuptrue% % diff -r 9890d4f0c1db -r 2fe7a42ece1d doc-src/IsarRef/Thy/document/Spec.tex --- a/doc-src/IsarRef/Thy/document/Spec.tex Mon Mar 26 15:33:28 2012 +0200 +++ b/doc-src/IsarRef/Thy/document/Spec.tex Mon Mar 26 17:58:47 2012 +0200 @@ -72,18 +72,42 @@ \rail@begin{4}{} \rail@term{\hyperlink{command.theory}{\mbox{\isa{\isacommand{theory}}}}}[] \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[] +\rail@nont{\isa{imports}}[] \rail@cr{2} -\rail@term{\isa{\isakeyword{imports}}}[] -\rail@plus -\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[] -\rail@nextplus{3} -\rail@endplus +\rail@bar +\rail@nextbar{3} +\rail@nont{\isa{keywords}}[] +\rail@endbar \rail@bar \rail@nextbar{3} \rail@nont{\isa{uses}}[] \rail@endbar \rail@term{\isa{\isakeyword{begin}}}[] \rail@end +\rail@begin{2}{\isa{imports}} +\rail@term{\isa{\isakeyword{imports}}}[] +\rail@plus +\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[] +\rail@nextplus{1} +\rail@endplus +\rail@end +\rail@begin{3}{\isa{keywords}} +\rail@term{\isa{\isakeyword{keywords}}}[] +\rail@plus +\rail@plus +\rail@nont{\hyperlink{syntax.string}{\mbox{\isa{string}}}}[] +\rail@nextplus{1} +\rail@endplus +\rail@bar +\rail@nextbar{1} +\rail@term{\isa{{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}}}[] +\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[] +\rail@nont{\hyperlink{syntax.tags}{\mbox{\isa{tags}}}}[] +\rail@endbar +\rail@nextplus{2} +\rail@cterm{\isa{\isakeyword{and}}}[] +\rail@endplus +\rail@end \rail@begin{3}{\isa{uses}} \rail@term{\isa{\isakeyword{uses}}}[] \rail@plus @@ -102,17 +126,27 @@ \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}}} starts a new theory \isa{A} based on the merge of existing - 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 than one ancestor, the - resulting theory structure of an Isabelle session forms a directed - acyclic graph (DAG). Isabelle's theory loader ensures that the - sources contributing to the development graph are always up-to-date: - changed files are automatically reloaded whenever a theory header - specification is processed. + 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 + than one ancestor, the resulting theory structure of an Isabelle + session forms a directed acyclic graph (DAG). Isabelle takes care + that sources contributing to the development graph are always + up-to-date: changed files are automatically rechecked whenever a + theory header specification is processed. + + The optional \indexdef{}{keyword}{keywords}\hypertarget{keyword.keywords}{\hyperlink{keyword.keywords}{\mbox{\isa{\isakeyword{keywords}}}}} specification declares outer + syntax (\chref{ch:outer-syntax}) that is introduced in this theory + later on (rare in end-user applications). Both minor keywords and + major keywords of the Isar command language need to be specified, in + order to make parsing of proof documents work properly. Command + keywords need to be classified according to their structural role in + the formal text. Examples may be seen in Isabelle/HOL sources + itself, such as \hyperlink{keyword.keywords}{\mbox{\isa{\isakeyword{keywords}}}}~\verb|"typedef"| + \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 + with and without proof, respectively. Additional \hyperlink{syntax.tags}{\mbox{\isa{tags}}} + provide defaults for document preparation (\secref{sec:tags}). The optional \indexdef{}{keyword}{uses}\hypertarget{keyword.uses}{\hyperlink{keyword.uses}{\mbox{\isa{\isakeyword{uses}}}}} specification declares additional - dependencies on extra files (usually ML sources). Files will be + dependencies on external files (notably ML sources). Files will be loaded immediately (as ML), unless the name is parenthesized. The latter case records a dependency that needs to be resolved later in the text, usually via explicit \indexref{}{command}{use}\hyperlink{command.use}{\mbox{\isa{\isacommand{use}}}} for ML files; @@ -120,8 +154,9 @@ corresponding tools or packages. \item \hyperlink{command.global.end}{\mbox{\isa{\isacommand{end}}}} concludes the current theory - definition. Note that local theory targets involve a local - \hyperlink{command.local.end}{\mbox{\isa{\isacommand{end}}}}, which is clear from the nesting. + definition. Note that some other commands, e.g.\ local theory + targets \hyperlink{command.locale}{\mbox{\isa{\isacommand{locale}}}} or \hyperlink{command.class}{\mbox{\isa{\isacommand{class}}}} may involve a + \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. \end{description}% \end{isamarkuptext}% diff -r 9890d4f0c1db -r 2fe7a42ece1d lib/Tools/java --- a/lib/Tools/java Mon Mar 26 15:33:28 2012 +0200 +++ b/lib/Tools/java Mon Mar 26 17:58:47 2012 +0200 @@ -6,21 +6,12 @@ CLASSPATH="$(jvmpath "$CLASSPATH")" -JAVA_EXE="$ISABELLE_JDK_HOME/bin/java" - -if "$JAVA_EXE" -version >/dev/null 2>/dev/null; then - : -else - echo "Bad Java executable: \"$JAVA_EXE\"" >&2 - exit 2 -fi - -if "$JAVA_EXE" -server >/dev/null 2>/dev/null; then +if isabelle_jdk java -server >/dev/null 2>/dev/null; then SERVER="-server" else SERVER="" fi -exec "$JAVA_EXE" -Dfile.encoding=UTF-8 $SERVER \ +exec "$ISABELLE_JDK_HOME/bin/java" -Dfile.encoding=UTF-8 $SERVER \ "-Djava.ext.dirs=$("$ISABELLE_HOME/src/Tools/JVM/java_ext_dirs")" "$@" diff -r 9890d4f0c1db -r 2fe7a42ece1d lib/Tools/scala --- a/lib/Tools/scala Mon Mar 26 15:33:28 2012 +0200 +++ b/lib/Tools/scala Mon Mar 26 17:58:47 2012 +0200 @@ -4,10 +4,8 @@ # # DESCRIPTION: invoke Scala within the Isabelle environment -[ -z "$SCALA_HOME" ] && { echo "Unknown SCALA_HOME -- Scala unavailable"; exit 2; } - [ -e "$ISABELLE_HOME/Admin/build" ] && { "$ISABELLE_HOME/Admin/build" jars || exit $?; } CLASSPATH="$(jvmpath "$CLASSPATH")" -exec "$SCALA_HOME/bin/scala" -Dfile.encoding=UTF-8 \ +isabelle_scala scala -Dfile.encoding=UTF-8 \ "-Djava.ext.dirs=$("$ISABELLE_HOME/src/Tools/JVM/java_ext_dirs")" "$@" diff -r 9890d4f0c1db -r 2fe7a42ece1d lib/Tools/scalac --- a/lib/Tools/scalac Mon Mar 26 15:33:28 2012 +0200 +++ b/lib/Tools/scalac Mon Mar 26 17:58:47 2012 +0200 @@ -4,10 +4,8 @@ # # DESCRIPTION: invoke Scala compiler within the Isabelle environment -[ -z "$SCALA_HOME" ] && { echo "Unknown SCALA_HOME -- Scala unavailable"; exit 2; } - [ -e "$ISABELLE_HOME/Admin/build" ] && { "$ISABELLE_HOME/Admin/build" jars || exit $?; } CLASSPATH="$(jvmpath "$CLASSPATH")" -exec "$SCALA_HOME/bin/scalac" -Dfile.encoding=UTF-8 \ +isabelle_scala scalac -Dfile.encoding=UTF-8 \ "-Djava.ext.dirs=$("$ISABELLE_HOME/src/Tools/JVM/java_ext_dirs")" "$@" diff -r 9890d4f0c1db -r 2fe7a42ece1d lib/browser/build --- a/lib/browser/build Mon Mar 26 15:33:28 2012 +0200 +++ b/lib/browser/build Mon Mar 26 17:58:47 2012 +0200 @@ -65,9 +65,9 @@ rm -rf classes && mkdir classes - "$ISABELLE_JDK_HOME/bin/javac" -d classes -source 1.4 "${SOURCES[@]}" || \ + isabelle_jdk javac -d classes -source 1.4 "${SOURCES[@]}" || \ fail "Failed to compile sources" - "$ISABELLE_JDK_HOME/bin/jar" cf "$(jvmpath "$TARGET")" -C classes . || + isabelle_jdk jar cf "$(jvmpath "$TARGET")" -C classes . || fail "Failed to produce $TARGET" rm -rf classes diff -r 9890d4f0c1db -r 2fe7a42ece1d lib/scripts/getsettings --- a/lib/scripts/getsettings Mon Mar 26 15:33:28 2012 +0200 +++ b/lib/scripts/getsettings Mon Mar 26 17:58:47 2012 +0200 @@ -89,6 +89,22 @@ done } +#robust invocation via ISABELLE_JDK_HOME +function isabelle_jdk () { + [ -z "$ISABELLE_JDK_HOME" ] && \ + { echo "Unknown ISABELLE_JDK_HOME -- Java tools unavailable"; exit 2; } + local PRG="$1"; shift + "$ISABELLE_JDK_HOME/bin/$PRG" "$@" +} + +#robust invocation via SCALA_HOME +function isabelle_scala () { + [ -z "$SCALA_HOME" ] && \ + { echo "Unknown SCALA_HOME -- Scala unavailable"; exit 2; } + local PRG="$1"; shift + "$SCALA_HOME/bin/$PRG" "$@" +} + #CLASSPATH convenience function classpath () { for X in "$@" diff -r 9890d4f0c1db -r 2fe7a42ece1d src/Pure/build-jars --- a/src/Pure/build-jars Mon Mar 26 15:33:28 2012 +0200 +++ b/src/Pure/build-jars Mon Mar 26 17:58:47 2012 +0200 @@ -88,7 +88,6 @@ } [ -z "$ISABELLE_HOME" ] && fail "Missing Isabelle settings environment" -[ -z "$SCALA_HOME" ] && fail "Unknown SCALA_HOME -- Scala unavailable" ## process command line @@ -172,10 +171,10 @@ SCALAC_OPTIONS="$ISABELLE_SCALA_BUILD_OPTIONS -d classes" - "$SCALA_HOME/bin/scalac" $SCALAC_OPTIONS "${PIDE_SOURCES[@]}" || \ + isabelle_scala scalac $SCALAC_OPTIONS "${PIDE_SOURCES[@]}" || \ fail "Failed to compile PIDE sources" - "$SCALA_HOME/bin/scalac" $SCALAC_OPTIONS -classpath classes "${PURE_SOURCES[@]}" || \ + isabelle_scala scalac $SCALAC_OPTIONS -classpath classes "${PURE_SOURCES[@]}" || \ fail "Failed to compile Pure sources" mkdir -p "$TARGET_DIR/ext" || fail "Failed to create directory $TARGET_DIR/ext" @@ -186,7 +185,7 @@ mkdir -p "$(dirname "$CHARSET_SERVICE")" echo isabelle.Isabelle_Charset_Provider > "$CHARSET_SERVICE" - "$ISABELLE_JDK_HOME/bin/jar" cfe "$(jvmpath "$TARGET")" isabelle.GUI_Setup META-INF isabelle || \ + isabelle_jdk jar cfe "$(jvmpath "$TARGET")" isabelle.GUI_Setup META-INF isabelle || \ fail "Failed to produce $TARGET" cp "$SCALA_HOME/lib/scala-swing.jar" "$SCALA_HOME/lib/scala-library.jar" "$TARGET_DIR/ext" diff -r 9890d4f0c1db -r 2fe7a42ece1d src/Tools/JVM/java_ext_dirs --- a/src/Tools/JVM/java_ext_dirs Mon Mar 26 15:33:28 2012 +0200 +++ b/src/Tools/JVM/java_ext_dirs Mon Mar 26 17:58:47 2012 +0200 @@ -17,7 +17,7 @@ ## main -exec "$ISABELLE_JDK_HOME/bin/java" \ +isabelle_jdk java \ -classpath "$(jvmpath "$ISABELLE_HOME/src/Tools/JVM/java_ext_dirs.jar")" \ isabelle.Java_Ext_Dirs "$(jvmpath "$ISABELLE_HOME/lib/classes/ext")" diff -r 9890d4f0c1db -r 2fe7a42ece1d src/Tools/jEdit/lib/Tools/jedit --- a/src/Tools/jEdit/lib/Tools/jedit Mon Mar 26 15:33:28 2012 +0200 +++ b/src/Tools/jEdit/lib/Tools/jedit Mon Mar 26 17:58:47 2012 +0200 @@ -248,7 +248,7 @@ ) || fail "Failed to compile sources" cd dist/classes - "$ISABELLE_JDK_HOME/bin/jar" cf "../jars/Isabelle-jEdit.jar" * || failed + isabelle_jdk jar cf "../jars/Isabelle-jEdit.jar" * || failed cd ../.. rm -rf dist/classes fi