--- a/NEWS Mon Nov 29 23:41:09 2010 +0100
+++ b/NEWS Tue Nov 30 00:12:29 2010 +0100
@@ -83,8 +83,11 @@
* Discontinued ancient 'constdefs' command. INCOMPATIBILITY, use
'definition' instead.
-* Document antiquotations @{class} and @{type} for printing classes
-and type constructors.
+* Document antiquotations @{class} and @{type} print classes and type
+constructors.
+
+* Document antiquotation @{file} checks file/directory entries within
+the local file system.
*** HOL ***
--- a/doc-src/IsarImplementation/Thy/document/Isar.tex Mon Nov 29 23:41:09 2010 +0100
+++ b/doc-src/IsarImplementation/Thy/document/Isar.tex Tue Nov 30 00:12:29 2010 +0100
@@ -708,7 +708,7 @@
\medskip Apart from explicit arguments, common proof methods
typically work with a default configuration provided by the context.
As a shortcut to rule management we use a cheap solution via functor
- \verb|Named_Thms| (see also \hyperlink{file.~~/src/Pure/Tools/named-thms.ML}{\mbox{\isa{\isatt{{\isaliteral{7E}{\isachartilde}}{\isaliteral{7E}{\isachartilde}}{\isaliteral{2F}{\isacharslash}}src{\isaliteral{2F}{\isacharslash}}Pure{\isaliteral{2F}{\isacharslash}}Tools{\isaliteral{2F}{\isacharslash}}named{\isaliteral{5F}{\isacharunderscore}}thms{\isaliteral{2E}{\isachardot}}ML}}}}).%
+ \verb|Named_Thms| (see also \verb|~~/src/Pure/Tools/named_thms.ML|).%
\end{isamarkuptext}%
\isamarkuptrue%
%
--- a/doc-src/IsarImplementation/Thy/document/ML.tex Mon Nov 29 23:41:09 2010 +0100
+++ b/doc-src/IsarImplementation/Thy/document/ML.tex Tue Nov 30 00:12:29 2010 +0100
@@ -89,7 +89,7 @@
Isabelle source files have a certain standardized header
format (with precise spacing) that follows ancient traditions
reaching back to the earliest versions of the system by Larry
- Paulson. See \hyperlink{file.~~/src/Pure/thm.ML}{\mbox{\isa{\isatt{{\isaliteral{7E}{\isachartilde}}{\isaliteral{7E}{\isachartilde}}{\isaliteral{2F}{\isacharslash}}src{\isaliteral{2F}{\isacharslash}}Pure{\isaliteral{2F}{\isacharslash}}thm{\isaliteral{2E}{\isachardot}}ML}}}}, for example.
+ Paulson. See \verb|~~/src/Pure/thm.ML|, for example.
The header includes at least \verb|Title| and \verb|Author| entries, followed by a prose description of the purpose of
the module. The latter can range from a single line to several
@@ -1645,7 +1645,7 @@
integer type --- overloading of SML97 is disabled.
Structure \verb|IntInf| of SML97 is obsolete and superseded by
- \verb|Int|. Structure \verb|Integer| in \hyperlink{file.~~/src/Pure/General/integer.ML}{\mbox{\isa{\isatt{{\isaliteral{7E}{\isachartilde}}{\isaliteral{7E}{\isachartilde}}{\isaliteral{2F}{\isacharslash}}src{\isaliteral{2F}{\isacharslash}}Pure{\isaliteral{2F}{\isacharslash}}General{\isaliteral{2F}{\isacharslash}}integer{\isaliteral{2E}{\isachardot}}ML}}}} provides some additional
+ \verb|Int|. Structure \verb|Integer| in \verb|~~/src/Pure/General/integer.ML| provides some additional
operations.
\end{description}%
@@ -1730,7 +1730,7 @@
\begin{isamarkuptext}%
Apart from \verb|Option.map| most operations defined in
structure \verb|Option| are alien to Isabelle/ML. The
- operations shown above are defined in \hyperlink{file.~~/src/Pure/General/basics.ML}{\mbox{\isa{\isatt{{\isaliteral{7E}{\isachartilde}}{\isaliteral{7E}{\isachartilde}}{\isaliteral{2F}{\isacharslash}}src{\isaliteral{2F}{\isacharslash}}Pure{\isaliteral{2F}{\isacharslash}}General{\isaliteral{2F}{\isacharslash}}basics{\isaliteral{2E}{\isachardot}}ML}}}}, among others.%
+ operations shown above are defined in \verb|~~/src/Pure/General/basics.ML|, among others.%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -1771,7 +1771,7 @@
\item \verb|member|, \verb|insert|, \verb|remove|, \verb|update| treat
lists as a set-like container that maintains the order of elements.
- See \hyperlink{file.~~/src/Pure/library.ML}{\mbox{\isa{\isatt{{\isaliteral{7E}{\isachartilde}}{\isaliteral{7E}{\isachartilde}}{\isaliteral{2F}{\isacharslash}}src{\isaliteral{2F}{\isacharslash}}Pure{\isaliteral{2F}{\isacharslash}}library{\isaliteral{2E}{\isachardot}}ML}}}} for the full specifications
+ See \verb|~~/src/Pure/library.ML| for the full specifications
(written in ML). There are some further derived operations like
\verb|union| or \verb|inter|.
@@ -1877,7 +1877,7 @@
This way of merging lists is typical for context data
(\secref{sec:context-data}). See also \verb|merge| as defined in
- \hyperlink{file.~~/src/Pure/library.ML}{\mbox{\isa{\isatt{{\isaliteral{7E}{\isachartilde}}{\isaliteral{7E}{\isachartilde}}{\isaliteral{2F}{\isacharslash}}src{\isaliteral{2F}{\isacharslash}}Pure{\isaliteral{2F}{\isacharslash}}library{\isaliteral{2E}{\isachardot}}ML}}}}.%
+ \verb|~~/src/Pure/library.ML|.%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -1921,7 +1921,7 @@
Association lists are adequate as simple and light-weight
implementation of finite mappings in many practical situations. A
- more heavy-duty table structure is defined in \hyperlink{file.~~/src/Pure/General/table.ML}{\mbox{\isa{\isatt{{\isaliteral{7E}{\isachartilde}}{\isaliteral{7E}{\isachartilde}}{\isaliteral{2F}{\isacharslash}}src{\isaliteral{2F}{\isacharslash}}Pure{\isaliteral{2F}{\isacharslash}}General{\isaliteral{2F}{\isacharslash}}table{\isaliteral{2E}{\isachardot}}ML}}}}; that version scales easily to
+ more heavy-duty table structure is defined in \verb|~~/src/Pure/General/table.ML|; that version scales easily to
thousands or millions of elements.%
\end{isamarkuptext}%
\isamarkuptrue%
@@ -2290,7 +2290,7 @@
\end{description}
- There are some further variants of the \verb|Synchronized.guarded_access| combinator, see \hyperlink{file.~~/src/Pure/Concurrent/synchronized.ML}{\mbox{\isa{\isatt{{\isaliteral{7E}{\isachartilde}}{\isaliteral{7E}{\isachartilde}}{\isaliteral{2F}{\isacharslash}}src{\isaliteral{2F}{\isacharslash}}Pure{\isaliteral{2F}{\isacharslash}}Concurrent{\isaliteral{2F}{\isacharslash}}synchronized{\isaliteral{2E}{\isachardot}}ML}}}} for details.%
+ There are some further variants of the \verb|Synchronized.guarded_access| combinator, see \verb|~~/src/Pure/Concurrent/synchronized.ML| for details.%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -2357,7 +2357,7 @@
\endisadelimML
%
\begin{isamarkuptext}%
-\medskip See \hyperlink{file.~~/src/Pure/Concurrent/mailbox.ML}{\mbox{\isa{\isatt{{\isaliteral{7E}{\isachartilde}}{\isaliteral{7E}{\isachartilde}}{\isaliteral{2F}{\isacharslash}}src{\isaliteral{2F}{\isacharslash}}Pure{\isaliteral{2F}{\isacharslash}}Concurrent{\isaliteral{2F}{\isacharslash}}mailbox{\isaliteral{2E}{\isachardot}}ML}}}} how
+\medskip See \verb|~~/src/Pure/Concurrent/mailbox.ML| how
to implement a mailbox as synchronized variable over a purely
functional queue.%
\end{isamarkuptext}%
--- a/doc-src/IsarImplementation/Thy/document/Tactic.tex Mon Nov 29 23:41:09 2010 +0100
+++ b/doc-src/IsarImplementation/Thy/document/Tactic.tex Tue Nov 30 00:12:29 2010 +0100
@@ -222,7 +222,7 @@
\item Type \verb|tactic| represents tactics. The
well-formedness conditions described above need to be observed. See
- also \hyperlink{file.~~/src/Pure/General/seq.ML}{\mbox{\isa{\isatt{{\isaliteral{7E}{\isachartilde}}{\isaliteral{7E}{\isachartilde}}{\isaliteral{2F}{\isacharslash}}src{\isaliteral{2F}{\isacharslash}}Pure{\isaliteral{2F}{\isacharslash}}General{\isaliteral{2F}{\isacharslash}}seq{\isaliteral{2E}{\isachardot}}ML}}}} for the underlying
+ also \verb|~~/src/Pure/General/seq.ML| for the underlying
implementation of lazy sequences.
\item Type \verb|int -> tactic| represents tactics with
--- a/doc-src/IsarRef/Thy/Document_Preparation.thy Mon Nov 29 23:41:09 2010 +0100
+++ b/doc-src/IsarRef/Thy/Document_Preparation.thy Tue Nov 30 00:12:29 2010 +0100
@@ -156,6 +156,7 @@
@{antiquotation_def ML} & : & @{text antiquotation} \\
@{antiquotation_def ML_type} & : & @{text antiquotation} \\
@{antiquotation_def ML_struct} & : & @{text antiquotation} \\
+ @{antiquotation_def "file"} & : & @{text antiquotation} \\
\end{matharray}
The overall content of an Isabelle/Isar theory may alternate between
@@ -201,7 +202,8 @@
'full_prf' options thmrefs |
'ML' options name |
'ML_type' options name |
- 'ML_struct' options name
+ 'ML_struct' options name |
+ 'file' options name
;
options: '[' (option * ',') ']'
;
@@ -287,6 +289,9 @@
"@{ML_struct s}"} check text @{text s} as ML value, type, and
structure, respectively. The source is printed verbatim.
+ \item @{text "@{file path}"} checks that @{text "path"} refers to a
+ file (or directory) and prints it verbatim.
+
\end{description}
*}
--- a/doc-src/IsarRef/Thy/document/Document_Preparation.tex Mon Nov 29 23:41:09 2010 +0100
+++ b/doc-src/IsarRef/Thy/document/Document_Preparation.tex Tue Nov 30 00:12:29 2010 +0100
@@ -95,7 +95,7 @@
document generated from a theory. Each markup command takes a
single \hyperlink{syntax.text}{\mbox{\isa{text}}} argument, which is passed as argument to a
corresponding {\LaTeX} macro. The default macros provided by
- \hyperlink{file.~~/lib/texinputs/isabelle.sty}{\mbox{\isa{\isatt{{\isaliteral{7E}{\isachartilde}}{\isaliteral{7E}{\isachartilde}}{\isaliteral{2F}{\isacharslash}}lib{\isaliteral{2F}{\isacharslash}}texinputs{\isaliteral{2F}{\isacharslash}}isabelle{\isaliteral{2E}{\isachardot}}sty}}}} can be redefined according
+ \verb|~~/lib/texinputs/isabelle.sty| can be redefined according
to the needs of the underlying document and {\LaTeX} styles.
Note that formal comments (\secref{sec:comments}) are similar to
@@ -174,6 +174,7 @@
\indexdef{}{antiquotation}{ML}\hypertarget{antiquotation.ML}{\hyperlink{antiquotation.ML}{\mbox{\isa{ML}}}} & : & \isa{antiquotation} \\
\indexdef{}{antiquotation}{ML\_type}\hypertarget{antiquotation.ML-type}{\hyperlink{antiquotation.ML-type}{\mbox{\isa{ML{\isaliteral{5F}{\isacharunderscore}}type}}}} & : & \isa{antiquotation} \\
\indexdef{}{antiquotation}{ML\_struct}\hypertarget{antiquotation.ML-struct}{\hyperlink{antiquotation.ML-struct}{\mbox{\isa{ML{\isaliteral{5F}{\isacharunderscore}}struct}}}} & : & \isa{antiquotation} \\
+ \indexdef{}{antiquotation}{file}\hypertarget{antiquotation.file}{\hyperlink{antiquotation.file}{\mbox{\isa{file}}}} & : & \isa{antiquotation} \\
\end{matharray}
The overall content of an Isabelle/Isar theory may alternate between
@@ -219,7 +220,8 @@
'full_prf' options thmrefs |
'ML' options name |
'ML_type' options name |
- 'ML_struct' options name
+ 'ML_struct' options name |
+ 'file' options name
;
options: '[' (option * ',') ']'
;
@@ -300,6 +302,9 @@
\item \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{40}{\isacharat}}{\isaliteral{7B}{\isacharbraceleft}}ML\ s{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{22}{\isachardoublequote}}}, \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{40}{\isacharat}}{\isaliteral{7B}{\isacharbraceleft}}ML{\isaliteral{5F}{\isacharunderscore}}type\ s{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{22}{\isachardoublequote}}}, and \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{40}{\isacharat}}{\isaliteral{7B}{\isacharbraceleft}}ML{\isaliteral{5F}{\isacharunderscore}}struct\ s{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{22}{\isachardoublequote}}} check text \isa{s} as ML value, type, and
structure, respectively. The source is printed verbatim.
+ \item \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{40}{\isacharat}}{\isaliteral{7B}{\isacharbraceleft}}file\ path{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{22}{\isachardoublequote}}} checks that \isa{{\isaliteral{22}{\isachardoublequote}}path{\isaliteral{22}{\isachardoublequote}}} refers to a
+ file (or directory) and prints it verbatim.
+
\end{description}%
\end{isamarkuptext}%
\isamarkuptrue%
@@ -466,7 +471,7 @@
\medskip Command tags merely produce certain markup environments for
type-setting. The meaning of these is determined by {\LaTeX}
- macros, as defined in \hyperlink{file.~~/lib/texinputs/isabelle.sty}{\mbox{\isa{\isatt{{\isaliteral{7E}{\isachartilde}}{\isaliteral{7E}{\isachartilde}}{\isaliteral{2F}{\isacharslash}}lib{\isaliteral{2F}{\isacharslash}}texinputs{\isaliteral{2F}{\isacharslash}}isabelle{\isaliteral{2E}{\isachardot}}sty}}}} or
+ macros, as defined in \verb|~~/lib/texinputs/isabelle.sty| or
by the document author. The Isabelle document preparation tools
also provide some high-level options to specify the meaning of
arbitrary tags to ``keep'', ``drop'', or ``fold'' the corresponding
--- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex Mon Nov 29 23:41:09 2010 +0100
+++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex Tue Nov 30 00:12:29 2010 +0100
@@ -897,7 +897,7 @@
The \hyperlink{method.HOL.coherent}{\mbox{\isa{coherent}}} method solves problems of
\emph{Coherent Logic} \cite{Bezem-Coquand:2005}, which covers
applications in confluence theory, lattice theory and projective
- geometry. See \hyperlink{file.~~/src/HOL/ex/Coherent.thy}{\mbox{\isa{\isatt{{\isaliteral{7E}{\isachartilde}}{\isaliteral{7E}{\isachartilde}}{\isaliteral{2F}{\isacharslash}}src{\isaliteral{2F}{\isacharslash}}HOL{\isaliteral{2F}{\isacharslash}}ex{\isaliteral{2F}{\isacharslash}}Coherent{\isaliteral{2E}{\isachardot}}thy}}}} for some
+ geometry. See \verb|~~/src/HOL/ex/Coherent.thy| for some
examples.%
\end{isamarkuptext}%
\isamarkuptrue%
--- a/doc-src/IsarRef/Thy/document/Spec.tex Mon Nov 29 23:41:09 2010 +0100
+++ b/doc-src/IsarRef/Thy/document/Spec.tex Tue Nov 30 00:12:29 2010 +0100
@@ -1203,7 +1203,7 @@
\end{description}
- See \hyperlink{file.~~/src/HOL/ex/Iff-Oracle.thy}{\mbox{\isa{\isatt{{\isaliteral{7E}{\isachartilde}}{\isaliteral{7E}{\isachartilde}}{\isaliteral{2F}{\isacharslash}}src{\isaliteral{2F}{\isacharslash}}HOL{\isaliteral{2F}{\isacharslash}}ex{\isaliteral{2F}{\isacharslash}}Iff{\isaliteral{5F}{\isacharunderscore}}Oracle{\isaliteral{2E}{\isachardot}}thy}}}} for a worked example of
+ See \verb|~~/src/HOL/ex/Iff_Oracle.thy| for a worked example of
defining a new primitive rule as oracle, and turning it into a proof
method.%
\end{isamarkuptext}%
--- a/doc-src/System/Thy/document/Basics.tex Mon Nov 29 23:41:09 2010 +0100
+++ b/doc-src/System/Thy/document/Basics.tex Tue Nov 30 00:12:29 2010 +0100
@@ -71,7 +71,7 @@
their shell startup scripts, before being able to actually run the
program. Isabelle requires none such administrative chores of its
end-users --- the executables can be invoked straight away.
- Occasionally, users would still want to put the \hyperlink{file.$ISABELLE-HOME/bin}{\mbox{\isa{\isatt{{\isaliteral{24}{\isachardollar}}ISABELLE{\isaliteral{5F}{\isacharunderscore}}HOME{\isaliteral{2F}{\isacharslash}}bin}}}} directory into their shell's search path, but
+ Occasionally, users would still want to put the \verb|$ISABELLE_HOME/bin| directory into their shell's search path, but
this is not required.%
\end{isamarkuptext}%
\isamarkuptrue%
@@ -98,9 +98,9 @@
note that the Isabelle executables either have to be run from their
original location in the distribution directory, or via the
executable objects created by the \hyperlink{tool.install}{\mbox{\isa{\isatt{install}}}} utility. Symbolic
- links are admissible, but a plain copy of the \hyperlink{file.$ISABELLE-HOME/bin}{\mbox{\isa{\isatt{{\isaliteral{24}{\isachardollar}}ISABELLE{\isaliteral{5F}{\isacharunderscore}}HOME{\isaliteral{2F}{\isacharslash}}bin}}}} files will not work!
+ links are admissible, but a plain copy of the \verb|$ISABELLE_HOME/bin| files will not work!
- \item The file \hyperlink{file.$ISABELLE-HOME/etc/settings}{\mbox{\isa{\isatt{{\isaliteral{24}{\isachardollar}}ISABELLE{\isaliteral{5F}{\isacharunderscore}}HOME{\isaliteral{2F}{\isacharslash}}etc{\isaliteral{2F}{\isacharslash}}settings}}}} is run as a
+ \item The file \verb|$ISABELLE_HOME/etc/settings| is run as a
\indexref{}{executable}{bash}\hyperlink{executable.bash}{\mbox{\isa{\isatt{bash}}}} shell script with the auto-export option for
variables enabled.
@@ -117,10 +117,10 @@
before --- usually to something like \verb|$HOME/.isabelle/IsabelleXXXX|.
Thus individual users may override the site-wide defaults. See also
- file \hyperlink{file.$ISABELLE-HOME/etc/user-settings.sample}{\mbox{\isa{\isatt{{\isaliteral{24}{\isachardollar}}ISABELLE{\isaliteral{5F}{\isacharunderscore}}HOME{\isaliteral{2F}{\isacharslash}}etc{\isaliteral{2F}{\isacharslash}}user{\isaliteral{2D}{\isacharminus}}settings{\isaliteral{2E}{\isachardot}}sample}}}} in the
+ file \verb|$ISABELLE_HOME/etc/user-settings.sample| in the
distribution. Typically, a user settings file would contain only a
few lines, just the assigments that are really changed. One should
- definitely \emph{not} start with a full copy the basic \hyperlink{file.$ISABELLE-HOME/etc/settings}{\mbox{\isa{\isatt{{\isaliteral{24}{\isachardollar}}ISABELLE{\isaliteral{5F}{\isacharunderscore}}HOME{\isaliteral{2F}{\isacharslash}}etc{\isaliteral{2F}{\isacharslash}}settings}}}}. This could cause very annoying
+ definitely \emph{not} start with a full copy the basic \verb|$ISABELLE_HOME/etc/settings|. This could cause very annoying
maintainance problems later, when the Isabelle installation is
updated or changed otherwise.
@@ -193,7 +193,7 @@
\item[\indexdef{}{setting}{ISABELLE\_PROCESS}\hypertarget{setting.ISABELLE-PROCESS}{\hyperlink{setting.ISABELLE-PROCESS}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}PROCESS}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}}, \hyperlink{setting.ISABELLE-TOOL}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}TOOL}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}}] are automatically set to the full path
names of the \hyperlink{executable.isabelle-process}{\mbox{\isa{\isatt{isabelle{\isaliteral{2D}{\isacharminus}}process}}}} and \hyperlink{executable.isabelle}{\mbox{\isa{\isatt{isabelle}}}} executables, respectively. Thus other tools and scripts
- need not assume that the \hyperlink{file.$ISABELLE-HOME/bin}{\mbox{\isa{\isatt{{\isaliteral{24}{\isachardollar}}ISABELLE{\isaliteral{5F}{\isacharunderscore}}HOME{\isaliteral{2F}{\isacharslash}}bin}}}} directory is
+ need not assume that the \verb|$ISABELLE_HOME/bin| directory is
on the current search path of the shell.
\item[\indexdef{}{setting}{ISABELLE\_IDENTIFIER}\hypertarget{setting.ISABELLE-IDENTIFIER}{\hyperlink{setting.ISABELLE-IDENTIFIER}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}IDENTIFIER}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}}] refers
@@ -202,7 +202,7 @@
\item[\indexdef{}{setting}{ML\_SYSTEM}\hypertarget{setting.ML-SYSTEM}{\hyperlink{setting.ML-SYSTEM}{\mbox{\isa{\isatt{ML{\isaliteral{5F}{\isacharunderscore}}SYSTEM}}}}}, \indexdef{}{setting}{ML\_HOME}\hypertarget{setting.ML-HOME}{\hyperlink{setting.ML-HOME}{\mbox{\isa{\isatt{ML{\isaliteral{5F}{\isacharunderscore}}HOME}}}}},
\indexdef{}{setting}{ML\_OPTIONS}\hypertarget{setting.ML-OPTIONS}{\hyperlink{setting.ML-OPTIONS}{\mbox{\isa{\isatt{ML{\isaliteral{5F}{\isacharunderscore}}OPTIONS}}}}}, \indexdef{}{setting}{ML\_PLATFORM}\hypertarget{setting.ML-PLATFORM}{\hyperlink{setting.ML-PLATFORM}{\mbox{\isa{\isatt{ML{\isaliteral{5F}{\isacharunderscore}}PLATFORM}}}}}, \indexdef{}{setting}{ML\_IDENTIFIER}\hypertarget{setting.ML-IDENTIFIER}{\hyperlink{setting.ML-IDENTIFIER}{\mbox{\isa{\isatt{ML{\isaliteral{5F}{\isacharunderscore}}IDENTIFIER}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}}] specify the underlying ML system
to be used for Isabelle. There is only a fixed set of admissable
- \hyperlink{setting.ML-SYSTEM}{\mbox{\isa{\isatt{ML{\isaliteral{5F}{\isacharunderscore}}SYSTEM}}}} names (see the \hyperlink{file.$ISABELLE-HOME/etc/settings}{\mbox{\isa{\isatt{{\isaliteral{24}{\isachardollar}}ISABELLE{\isaliteral{5F}{\isacharunderscore}}HOME{\isaliteral{2F}{\isacharslash}}etc{\isaliteral{2F}{\isacharslash}}settings}}}} file of the distribution).
+ \hyperlink{setting.ML-SYSTEM}{\mbox{\isa{\isatt{ML{\isaliteral{5F}{\isacharunderscore}}SYSTEM}}}} names (see the \verb|$ISABELLE_HOME/etc/settings| file of the distribution).
The actual compiler binary will be run from the directory \hyperlink{setting.ML-HOME}{\mbox{\isa{\isatt{ML{\isaliteral{5F}{\isacharunderscore}}HOME}}}}, with \hyperlink{setting.ML-OPTIONS}{\mbox{\isa{\isatt{ML{\isaliteral{5F}{\isacharunderscore}}OPTIONS}}}} as first arguments on the
command line. The optional \hyperlink{setting.ML-PLATFORM}{\mbox{\isa{\isatt{ML{\isaliteral{5F}{\isacharunderscore}}PLATFORM}}}} may specify the
@@ -429,7 +429,7 @@
\medskip The \verb|-W| option makes Isabelle enter a special
process wrapper for interaction via the Isabelle/Scala layer, see
- also \hyperlink{file.~~/src/Pure/System/isabelle-process.scala}{\mbox{\isa{\isatt{{\isaliteral{7E}{\isachartilde}}{\isaliteral{7E}{\isachartilde}}{\isaliteral{2F}{\isacharslash}}src{\isaliteral{2F}{\isacharslash}}Pure{\isaliteral{2F}{\isacharslash}}System{\isaliteral{2F}{\isacharslash}}isabelle{\isaliteral{5F}{\isacharunderscore}}process{\isaliteral{2E}{\isachardot}}scala}}}}. The
+ also \verb|~~/src/Pure/System/isabelle_process.scala|. The
protocol between the ML and JVM process is private to the
implementation.
--- a/doc-src/System/Thy/document/Misc.tex Mon Nov 29 23:41:09 2010 +0100
+++ b/doc-src/System/Thy/document/Misc.tex Tue Nov 30 00:12:29 2010 +0100
@@ -250,7 +250,7 @@
\begin{isamarkuptext}%
Refer to the \verb|IsaMakefile|s of the Isabelle distribution's
object-logics as a model for your own developments. For example,
- see \hyperlink{file.~~/src/FOL/IsaMakefile}{\mbox{\isa{\isatt{{\isaliteral{7E}{\isachartilde}}{\isaliteral{7E}{\isachartilde}}{\isaliteral{2F}{\isacharslash}}src{\isaliteral{2F}{\isacharslash}}FOL{\isaliteral{2F}{\isacharslash}}IsaMakefile}}}}.%
+ see \verb|~~/src/FOL/IsaMakefile|.%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -363,8 +363,8 @@
sub-chunks separated by \isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E626F6C643E}{}\isactrlbold Y{\isaliteral{22}{\isachardoublequote}}}. Markup chunks start
with an empty sub-chunk, and a second empty sub-chunk indicates
close of an element. Any other non-empty chunk consists of plain
- text. For example, see \hyperlink{file.~~/src/Pure/General/yxml.ML}{\mbox{\isa{\isatt{{\isaliteral{7E}{\isachartilde}}{\isaliteral{7E}{\isachartilde}}{\isaliteral{2F}{\isacharslash}}src{\isaliteral{2F}{\isacharslash}}Pure{\isaliteral{2F}{\isacharslash}}General{\isaliteral{2F}{\isacharslash}}yxml{\isaliteral{2E}{\isachardot}}ML}}}} or
- \hyperlink{file.~~/src/Pure/General/yxml.scala}{\mbox{\isa{\isatt{{\isaliteral{7E}{\isachartilde}}{\isaliteral{7E}{\isachartilde}}{\isaliteral{2F}{\isacharslash}}src{\isaliteral{2F}{\isacharslash}}Pure{\isaliteral{2F}{\isacharslash}}General{\isaliteral{2F}{\isacharslash}}yxml{\isaliteral{2E}{\isachardot}}scala}}}}.
+ text. For example, see \verb|~~/src/Pure/General/yxml.ML| or
+ \verb|~~/src/Pure/General/yxml.scala|.
YXML documents may be detected quickly by checking that the first
two characters are \isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E626F6C643E}{}\isactrlbold X\isaliteral{5C3C5E626F6C643E}{}\isactrlbold Y{\isaliteral{22}{\isachardoublequote}}}.%
--- a/doc-src/System/Thy/document/Presentation.tex Mon Nov 29 23:41:09 2010 +0100
+++ b/doc-src/System/Thy/document/Presentation.tex Tue Nov 30 00:12:29 2010 +0100
@@ -96,14 +96,14 @@
The easiest way to let Isabelle generate theory browsing information
for existing sessions is to append ``\verb|-i true|'' to the
- \indexref{}{setting}{ISABELLE\_USEDIR\_OPTIONS}\hyperlink{setting.ISABELLE-USEDIR-OPTIONS}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}USEDIR{\isaliteral{5F}{\isacharunderscore}}OPTIONS}}}} before invoking \verb|isabelle| \hyperlink{tool.make}{\mbox{\isa{\isatt{make}}}} (or \hyperlink{file.$ISABELLE-HOME/build}{\mbox{\isa{\isatt{{\isaliteral{24}{\isachardollar}}ISABELLE{\isaliteral{5F}{\isacharunderscore}}HOME{\isaliteral{2F}{\isacharslash}}build}}}}). For
+ \indexref{}{setting}{ISABELLE\_USEDIR\_OPTIONS}\hyperlink{setting.ISABELLE-USEDIR-OPTIONS}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}USEDIR{\isaliteral{5F}{\isacharunderscore}}OPTIONS}}}} before invoking \verb|isabelle| \hyperlink{tool.make}{\mbox{\isa{\isatt{make}}}} (or \verb|$ISABELLE_HOME/build|). For
example, add something like this to your Isabelle settings file
\begin{ttbox}
ISABELLE_USEDIR_OPTIONS="-i true"
\end{ttbox}
- and then change into the \hyperlink{file.~~/src/FOL}{\mbox{\isa{\isatt{{\isaliteral{7E}{\isachartilde}}{\isaliteral{7E}{\isachartilde}}{\isaliteral{2F}{\isacharslash}}src{\isaliteral{2F}{\isacharslash}}FOL}}}} directory and run
+ and then change into the \verb|~~/src/FOL| directory and run
\verb|isabelle| \hyperlink{tool.make}{\mbox{\isa{\isatt{make}}}}, or even \verb|isabelle|
\hyperlink{tool.make}{\mbox{\isa{\isatt{make}}}}~\verb|all|. The presentation output will appear
in \verb|ISABELLE_BROWSER_INFO/FOL|, which usually refers to
@@ -111,7 +111,7 @@
\verb|-v true| will make the internal runs of \hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}}
more explicit about such details.
- Many standard Isabelle sessions (such as \hyperlink{file.~~/src/HOL/ex}{\mbox{\isa{\isatt{{\isaliteral{7E}{\isachartilde}}{\isaliteral{7E}{\isachartilde}}{\isaliteral{2F}{\isacharslash}}src{\isaliteral{2F}{\isacharslash}}HOL{\isaliteral{2F}{\isacharslash}}ex}}}})
+ Many standard Isabelle sessions (such as \verb|~~/src/HOL/ex|)
also provide actual printable documents. These are prepared
automatically as well if enabled like this, using the \verb|-d| option
\begin{ttbox}
@@ -451,7 +451,7 @@
manual editing of the generated \verb|IsaMakefile|, which is
meant to cover all of the sub-session directories at the same time
(this is the deeper reasong why \verb|IsaMakefile| is not made
- part of the initial session directory created by \verb|isabelle| \hyperlink{tool.mkdir}{\mbox{\isa{\isatt{mkdir}}}}). See \hyperlink{file.~~/src/HOL/IsaMakefile}{\mbox{\isa{\isatt{{\isaliteral{7E}{\isachartilde}}{\isaliteral{7E}{\isachartilde}}{\isaliteral{2F}{\isacharslash}}src{\isaliteral{2F}{\isacharslash}}HOL{\isaliteral{2F}{\isacharslash}}IsaMakefile}}}} for
+ part of the initial session directory created by \verb|isabelle| \hyperlink{tool.mkdir}{\mbox{\isa{\isatt{mkdir}}}}). See \verb|~~/src/HOL/IsaMakefile| for
a full-blown example.%
\end{isamarkuptext}%
\isamarkuptrue%
@@ -621,7 +621,7 @@
\begin{isamarkuptext}%
Refer to the \verb|IsaMakefile|s of the Isabelle distribution's
object-logics as a model for your own developments. For example,
- see \hyperlink{file.~~/src/FOL/IsaMakefile}{\mbox{\isa{\isatt{{\isaliteral{7E}{\isachartilde}}{\isaliteral{7E}{\isachartilde}}{\isaliteral{2F}{\isacharslash}}src{\isaliteral{2F}{\isacharslash}}FOL{\isaliteral{2F}{\isacharslash}}IsaMakefile}}}}. The Isabelle \indexref{}{tool}{mkdir}\hyperlink{tool.mkdir}{\mbox{\isa{\isatt{mkdir}}}} tool creates \verb|IsaMakefile|s with proper invocation
+ see \verb|~~/src/FOL/IsaMakefile|. The Isabelle \indexref{}{tool}{mkdir}\hyperlink{tool.mkdir}{\mbox{\isa{\isatt{mkdir}}}} tool creates \verb|IsaMakefile|s with proper invocation
of \hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}} as well.%
\end{isamarkuptext}%
\isamarkuptrue%
@@ -670,7 +670,7 @@
fold text tagged as \isa{foo}. The builtin default is equivalent
to the tag specification ``\verb|+theory,+proof,+ML,+visible,-invisible|''; see also the {\LaTeX}
macros \verb|\isakeeptag|, \verb|\isadroptag|, and
- \verb|\isafoldtag|, in \hyperlink{file.~~/lib/texinputs/isabelle.sty}{\mbox{\isa{\isatt{{\isaliteral{7E}{\isachartilde}}{\isaliteral{7E}{\isachartilde}}{\isaliteral{2F}{\isacharslash}}lib{\isaliteral{2F}{\isacharslash}}texinputs{\isaliteral{2F}{\isacharslash}}isabelle{\isaliteral{2E}{\isachardot}}sty}}}}.
+ \verb|\isafoldtag|, in \verb|~~/lib/texinputs/isabelle.sty|.
\medskip Document preparation requires a properly setup ``\verb|document|'' directory within the logic session sources. This
directory is supposed to contain all the files needed to produce the
@@ -701,7 +701,7 @@
containing all the theories.
The {\LaTeX} versions of the theories require some macros defined in
- \hyperlink{file.~~/lib/texinputs/isabelle.sty}{\mbox{\isa{\isatt{{\isaliteral{7E}{\isachartilde}}{\isaliteral{7E}{\isachartilde}}{\isaliteral{2F}{\isacharslash}}lib{\isaliteral{2F}{\isacharslash}}texinputs{\isaliteral{2F}{\isacharslash}}isabelle{\isaliteral{2E}{\isachardot}}sty}}}}. Doing \verb|\usepackage{isabelle}| in \verb|root.tex| should be fine;
+ \verb|~~/lib/texinputs/isabelle.sty|. Doing \verb|\usepackage{isabelle}| in \verb|root.tex| should be fine;
the underlying Isabelle \hyperlink{tool.latex}{\mbox{\isa{\isatt{latex}}}} tool already includes an
appropriate path specification for {\TeX} inputs.
@@ -710,11 +710,11 @@
contains a standard set of {\LaTeX} macro definitions \verb|\isasym|\isa{foo} corresponding to \verb|\|\verb|<|\isa{foo}\verb|>|, see \cite{isabelle-implementation} for a
complete list of predefined Isabelle symbols. Users may invent
further symbols as well, just by providing {\LaTeX} macros in a
- similar fashion as in \hyperlink{file.~~/lib/texinputs/isabellesym.sty}{\mbox{\isa{\isatt{{\isaliteral{7E}{\isachartilde}}{\isaliteral{7E}{\isachartilde}}{\isaliteral{2F}{\isacharslash}}lib{\isaliteral{2F}{\isacharslash}}texinputs{\isaliteral{2F}{\isacharslash}}isabellesym{\isaliteral{2E}{\isachardot}}sty}}}} of
+ similar fashion as in \verb|~~/lib/texinputs/isabellesym.sty| of
the distribution.
For proper setup of DVI and PDF documents (with hyperlinks and
- bookmarks), we recommend to include \hyperlink{file.~~/lib/texinputs/pdfsetup.sty}{\mbox{\isa{\isatt{{\isaliteral{7E}{\isachartilde}}{\isaliteral{7E}{\isachartilde}}{\isaliteral{2F}{\isacharslash}}lib{\isaliteral{2F}{\isacharslash}}texinputs{\isaliteral{2F}{\isacharslash}}pdfsetup{\isaliteral{2E}{\isachardot}}sty}}}} as well.
+ bookmarks), we recommend to include \verb|~~/lib/texinputs/pdfsetup.sty| as well.
\medskip As a final step of document preparation within Isabelle,
\verb|isabelle| \hyperlink{tool.document}{\mbox{\isa{\isatt{document}}}}~\verb|-c| is run on the
--- a/doc-src/antiquote_setup.ML Mon Nov 29 23:41:09 2010 +0100
+++ b/doc-src/antiquote_setup.ML Tue Nov 30 00:12:29 2010 +0100
@@ -4,7 +4,7 @@
Auxiliary antiquotations for the Isabelle manuals.
*)
-structure AntiquoteSetup: sig end =
+structure Antiquote_Setup: sig end =
struct
(* misc utils *)
@@ -190,7 +190,6 @@
val _ = entity_antiqs no_check "" "inference";
val _ = entity_antiqs no_check "isatt" "executable";
val _ = entity_antiqs (K check_tool) "isatt" "tool";
-val _ = entity_antiqs (K (File.exists o Path.explode)) "isatt" "file";
val _ = entity_antiqs (K (can Thy_Info.get_theory)) "" "theory";
val _ = entity_antiqs no_check "" "ML antiquotation"; (* FIXME proper check *)
--- a/src/Pure/Thy/thy_output.ML Mon Nov 29 23:41:09 2010 +0100
+++ b/src/Pure/Thy/thy_output.ML Tue Nov 30 00:12:29 2010 +0100
@@ -575,7 +575,6 @@
val _ = basic_entities "prf" Attrib.thms (pretty_prf false);
val _ = basic_entities "full_prf" Attrib.thms (pretty_prf true);
val _ = basic_entity "theory" (Scan.lift Args.name) pretty_theory;
-
val _ = basic_entities_style "thm_style" (Term_Style.parse_bare -- Attrib.thms) pretty_thm_style;
val _ = basic_entity "term_style" (Term_Style.parse_bare -- Args.term) pretty_term_style;
@@ -622,6 +621,11 @@
(* ML text *)
+val verb_text =
+ split_lines
+ #> map (space_implode "\\verb,|," o map (enclose "\\verb|" "|") o space_explode "|")
+ #> space_implode "\\isasep\\isanewline%\n";
+
local
fun ml_text name ml = antiquotation name (Scan.lift Args.name_source_position)
@@ -630,10 +634,7 @@
Symbol_Pos.content (Symbol_Pos.explode (txt, pos))
|> (if Config.get context quotes then quote else I)
|> (if Config.get context display then enclose "\\begin{verbatim}\n" "\n\\end{verbatim}"
- else
- split_lines
- #> map (space_implode "\\verb,|," o map (enclose "\\verb|" "|") o space_explode "|")
- #> space_implode "\\isasep\\isanewline%\n")));
+ else verb_text)));
fun ml_enclose bg en pos txt =
ML_Lex.read Position.none bg @ ML_Lex.read pos txt @ ML_Lex.read Position.none en;
@@ -653,4 +654,12 @@
end;
+
+(* files *)
+
+val _ = antiquotation "file" (Scan.lift Args.name)
+ (fn {context, ...} => fn path =>
+ if File.exists (Path.explode path) then verb_text path
+ else error ("Bad file: " ^ quote path));
+
end;