--- 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
--- 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
--- 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 \<IMPORTS> B\<^sub>1 \<dots> B\<^sub>n \<BEGIN>"}
starts a new theory @{text A} based on the merge of existing
- theories @{text "B\<^sub>1 \<dots> 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 \<dots> 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}
*}
--- 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%
%
--- 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}%
--- 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")" "$@"
--- 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")" "$@"
--- 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")" "$@"
--- 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
--- 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 "$@"
--- 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"
--- 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")"
--- 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