1.1 --- a/NEWS Mon Nov 29 23:41:09 2010 +0100
1.2 +++ b/NEWS Tue Nov 30 00:12:29 2010 +0100
1.3 @@ -83,8 +83,11 @@
1.4 * Discontinued ancient 'constdefs' command. INCOMPATIBILITY, use
1.5 'definition' instead.
1.6
1.7 -* Document antiquotations @{class} and @{type} for printing classes
1.8 -and type constructors.
1.9 +* Document antiquotations @{class} and @{type} print classes and type
1.10 +constructors.
1.11 +
1.12 +* Document antiquotation @{file} checks file/directory entries within
1.13 +the local file system.
1.14
1.15
1.16 *** HOL ***
2.1 --- a/doc-src/IsarImplementation/Thy/document/Isar.tex Mon Nov 29 23:41:09 2010 +0100
2.2 +++ b/doc-src/IsarImplementation/Thy/document/Isar.tex Tue Nov 30 00:12:29 2010 +0100
2.3 @@ -708,7 +708,7 @@
2.4 \medskip Apart from explicit arguments, common proof methods
2.5 typically work with a default configuration provided by the context.
2.6 As a shortcut to rule management we use a cheap solution via functor
2.7 - \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}}}}).%
2.8 + \verb|Named_Thms| (see also \verb|~~/src/Pure/Tools/named_thms.ML|).%
2.9 \end{isamarkuptext}%
2.10 \isamarkuptrue%
2.11 %
3.1 --- a/doc-src/IsarImplementation/Thy/document/ML.tex Mon Nov 29 23:41:09 2010 +0100
3.2 +++ b/doc-src/IsarImplementation/Thy/document/ML.tex Tue Nov 30 00:12:29 2010 +0100
3.3 @@ -89,7 +89,7 @@
3.4 Isabelle source files have a certain standardized header
3.5 format (with precise spacing) that follows ancient traditions
3.6 reaching back to the earliest versions of the system by Larry
3.7 - 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.
3.8 + Paulson. See \verb|~~/src/Pure/thm.ML|, for example.
3.9
3.10 The header includes at least \verb|Title| and \verb|Author| entries, followed by a prose description of the purpose of
3.11 the module. The latter can range from a single line to several
3.12 @@ -1645,7 +1645,7 @@
3.13 integer type --- overloading of SML97 is disabled.
3.14
3.15 Structure \verb|IntInf| of SML97 is obsolete and superseded by
3.16 - \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
3.17 + \verb|Int|. Structure \verb|Integer| in \verb|~~/src/Pure/General/integer.ML| provides some additional
3.18 operations.
3.19
3.20 \end{description}%
3.21 @@ -1730,7 +1730,7 @@
3.22 \begin{isamarkuptext}%
3.23 Apart from \verb|Option.map| most operations defined in
3.24 structure \verb|Option| are alien to Isabelle/ML. The
3.25 - 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.%
3.26 + operations shown above are defined in \verb|~~/src/Pure/General/basics.ML|, among others.%
3.27 \end{isamarkuptext}%
3.28 \isamarkuptrue%
3.29 %
3.30 @@ -1771,7 +1771,7 @@
3.31
3.32 \item \verb|member|, \verb|insert|, \verb|remove|, \verb|update| treat
3.33 lists as a set-like container that maintains the order of elements.
3.34 - 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
3.35 + See \verb|~~/src/Pure/library.ML| for the full specifications
3.36 (written in ML). There are some further derived operations like
3.37 \verb|union| or \verb|inter|.
3.38
3.39 @@ -1877,7 +1877,7 @@
3.40
3.41 This way of merging lists is typical for context data
3.42 (\secref{sec:context-data}). See also \verb|merge| as defined in
3.43 - \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}}}}.%
3.44 + \verb|~~/src/Pure/library.ML|.%
3.45 \end{isamarkuptext}%
3.46 \isamarkuptrue%
3.47 %
3.48 @@ -1921,7 +1921,7 @@
3.49
3.50 Association lists are adequate as simple and light-weight
3.51 implementation of finite mappings in many practical situations. A
3.52 - 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
3.53 + more heavy-duty table structure is defined in \verb|~~/src/Pure/General/table.ML|; that version scales easily to
3.54 thousands or millions of elements.%
3.55 \end{isamarkuptext}%
3.56 \isamarkuptrue%
3.57 @@ -2290,7 +2290,7 @@
3.58
3.59 \end{description}
3.60
3.61 - 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.%
3.62 + There are some further variants of the \verb|Synchronized.guarded_access| combinator, see \verb|~~/src/Pure/Concurrent/synchronized.ML| for details.%
3.63 \end{isamarkuptext}%
3.64 \isamarkuptrue%
3.65 %
3.66 @@ -2357,7 +2357,7 @@
3.67 \endisadelimML
3.68 %
3.69 \begin{isamarkuptext}%
3.70 -\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
3.71 +\medskip See \verb|~~/src/Pure/Concurrent/mailbox.ML| how
3.72 to implement a mailbox as synchronized variable over a purely
3.73 functional queue.%
3.74 \end{isamarkuptext}%
4.1 --- a/doc-src/IsarImplementation/Thy/document/Tactic.tex Mon Nov 29 23:41:09 2010 +0100
4.2 +++ b/doc-src/IsarImplementation/Thy/document/Tactic.tex Tue Nov 30 00:12:29 2010 +0100
4.3 @@ -222,7 +222,7 @@
4.4
4.5 \item Type \verb|tactic| represents tactics. The
4.6 well-formedness conditions described above need to be observed. See
4.7 - 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
4.8 + also \verb|~~/src/Pure/General/seq.ML| for the underlying
4.9 implementation of lazy sequences.
4.10
4.11 \item Type \verb|int -> tactic| represents tactics with
5.1 --- a/doc-src/IsarRef/Thy/Document_Preparation.thy Mon Nov 29 23:41:09 2010 +0100
5.2 +++ b/doc-src/IsarRef/Thy/Document_Preparation.thy Tue Nov 30 00:12:29 2010 +0100
5.3 @@ -156,6 +156,7 @@
5.4 @{antiquotation_def ML} & : & @{text antiquotation} \\
5.5 @{antiquotation_def ML_type} & : & @{text antiquotation} \\
5.6 @{antiquotation_def ML_struct} & : & @{text antiquotation} \\
5.7 + @{antiquotation_def "file"} & : & @{text antiquotation} \\
5.8 \end{matharray}
5.9
5.10 The overall content of an Isabelle/Isar theory may alternate between
5.11 @@ -201,7 +202,8 @@
5.12 'full_prf' options thmrefs |
5.13 'ML' options name |
5.14 'ML_type' options name |
5.15 - 'ML_struct' options name
5.16 + 'ML_struct' options name |
5.17 + 'file' options name
5.18 ;
5.19 options: '[' (option * ',') ']'
5.20 ;
5.21 @@ -287,6 +289,9 @@
5.22 "@{ML_struct s}"} check text @{text s} as ML value, type, and
5.23 structure, respectively. The source is printed verbatim.
5.24
5.25 + \item @{text "@{file path}"} checks that @{text "path"} refers to a
5.26 + file (or directory) and prints it verbatim.
5.27 +
5.28 \end{description}
5.29 *}
5.30
6.1 --- a/doc-src/IsarRef/Thy/document/Document_Preparation.tex Mon Nov 29 23:41:09 2010 +0100
6.2 +++ b/doc-src/IsarRef/Thy/document/Document_Preparation.tex Tue Nov 30 00:12:29 2010 +0100
6.3 @@ -95,7 +95,7 @@
6.4 document generated from a theory. Each markup command takes a
6.5 single \hyperlink{syntax.text}{\mbox{\isa{text}}} argument, which is passed as argument to a
6.6 corresponding {\LaTeX} macro. The default macros provided by
6.7 - \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
6.8 + \verb|~~/lib/texinputs/isabelle.sty| can be redefined according
6.9 to the needs of the underlying document and {\LaTeX} styles.
6.10
6.11 Note that formal comments (\secref{sec:comments}) are similar to
6.12 @@ -174,6 +174,7 @@
6.13 \indexdef{}{antiquotation}{ML}\hypertarget{antiquotation.ML}{\hyperlink{antiquotation.ML}{\mbox{\isa{ML}}}} & : & \isa{antiquotation} \\
6.14 \indexdef{}{antiquotation}{ML\_type}\hypertarget{antiquotation.ML-type}{\hyperlink{antiquotation.ML-type}{\mbox{\isa{ML{\isaliteral{5F}{\isacharunderscore}}type}}}} & : & \isa{antiquotation} \\
6.15 \indexdef{}{antiquotation}{ML\_struct}\hypertarget{antiquotation.ML-struct}{\hyperlink{antiquotation.ML-struct}{\mbox{\isa{ML{\isaliteral{5F}{\isacharunderscore}}struct}}}} & : & \isa{antiquotation} \\
6.16 + \indexdef{}{antiquotation}{file}\hypertarget{antiquotation.file}{\hyperlink{antiquotation.file}{\mbox{\isa{file}}}} & : & \isa{antiquotation} \\
6.17 \end{matharray}
6.18
6.19 The overall content of an Isabelle/Isar theory may alternate between
6.20 @@ -219,7 +220,8 @@
6.21 'full_prf' options thmrefs |
6.22 'ML' options name |
6.23 'ML_type' options name |
6.24 - 'ML_struct' options name
6.25 + 'ML_struct' options name |
6.26 + 'file' options name
6.27 ;
6.28 options: '[' (option * ',') ']'
6.29 ;
6.30 @@ -300,6 +302,9 @@
6.31 \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
6.32 structure, respectively. The source is printed verbatim.
6.33
6.34 + \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
6.35 + file (or directory) and prints it verbatim.
6.36 +
6.37 \end{description}%
6.38 \end{isamarkuptext}%
6.39 \isamarkuptrue%
6.40 @@ -466,7 +471,7 @@
6.41
6.42 \medskip Command tags merely produce certain markup environments for
6.43 type-setting. The meaning of these is determined by {\LaTeX}
6.44 - 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
6.45 + macros, as defined in \verb|~~/lib/texinputs/isabelle.sty| or
6.46 by the document author. The Isabelle document preparation tools
6.47 also provide some high-level options to specify the meaning of
6.48 arbitrary tags to ``keep'', ``drop'', or ``fold'' the corresponding
7.1 --- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex Mon Nov 29 23:41:09 2010 +0100
7.2 +++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex Tue Nov 30 00:12:29 2010 +0100
7.3 @@ -897,7 +897,7 @@
7.4 The \hyperlink{method.HOL.coherent}{\mbox{\isa{coherent}}} method solves problems of
7.5 \emph{Coherent Logic} \cite{Bezem-Coquand:2005}, which covers
7.6 applications in confluence theory, lattice theory and projective
7.7 - 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
7.8 + geometry. See \verb|~~/src/HOL/ex/Coherent.thy| for some
7.9 examples.%
7.10 \end{isamarkuptext}%
7.11 \isamarkuptrue%
8.1 --- a/doc-src/IsarRef/Thy/document/Spec.tex Mon Nov 29 23:41:09 2010 +0100
8.2 +++ b/doc-src/IsarRef/Thy/document/Spec.tex Tue Nov 30 00:12:29 2010 +0100
8.3 @@ -1203,7 +1203,7 @@
8.4
8.5 \end{description}
8.6
8.7 - 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
8.8 + See \verb|~~/src/HOL/ex/Iff_Oracle.thy| for a worked example of
8.9 defining a new primitive rule as oracle, and turning it into a proof
8.10 method.%
8.11 \end{isamarkuptext}%
9.1 --- a/doc-src/System/Thy/document/Basics.tex Mon Nov 29 23:41:09 2010 +0100
9.2 +++ b/doc-src/System/Thy/document/Basics.tex Tue Nov 30 00:12:29 2010 +0100
9.3 @@ -71,7 +71,7 @@
9.4 their shell startup scripts, before being able to actually run the
9.5 program. Isabelle requires none such administrative chores of its
9.6 end-users --- the executables can be invoked straight away.
9.7 - 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
9.8 + Occasionally, users would still want to put the \verb|$ISABELLE_HOME/bin| directory into their shell's search path, but
9.9 this is not required.%
9.10 \end{isamarkuptext}%
9.11 \isamarkuptrue%
9.12 @@ -98,9 +98,9 @@
9.13 note that the Isabelle executables either have to be run from their
9.14 original location in the distribution directory, or via the
9.15 executable objects created by the \hyperlink{tool.install}{\mbox{\isa{\isatt{install}}}} utility. Symbolic
9.16 - 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!
9.17 + links are admissible, but a plain copy of the \verb|$ISABELLE_HOME/bin| files will not work!
9.18
9.19 - \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
9.20 + \item The file \verb|$ISABELLE_HOME/etc/settings| is run as a
9.21 \indexref{}{executable}{bash}\hyperlink{executable.bash}{\mbox{\isa{\isatt{bash}}}} shell script with the auto-export option for
9.22 variables enabled.
9.23
9.24 @@ -117,10 +117,10 @@
9.25 before --- usually to something like \verb|$HOME/.isabelle/IsabelleXXXX|.
9.26
9.27 Thus individual users may override the site-wide defaults. See also
9.28 - 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
9.29 + file \verb|$ISABELLE_HOME/etc/user-settings.sample| in the
9.30 distribution. Typically, a user settings file would contain only a
9.31 few lines, just the assigments that are really changed. One should
9.32 - 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
9.33 + definitely \emph{not} start with a full copy the basic \verb|$ISABELLE_HOME/etc/settings|. This could cause very annoying
9.34 maintainance problems later, when the Isabelle installation is
9.35 updated or changed otherwise.
9.36
9.37 @@ -193,7 +193,7 @@
9.38
9.39 \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
9.40 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
9.41 - 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
9.42 + need not assume that the \verb|$ISABELLE_HOME/bin| directory is
9.43 on the current search path of the shell.
9.44
9.45 \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
9.46 @@ -202,7 +202,7 @@
9.47 \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}}}}},
9.48 \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
9.49 to be used for Isabelle. There is only a fixed set of admissable
9.50 - \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).
9.51 + \hyperlink{setting.ML-SYSTEM}{\mbox{\isa{\isatt{ML{\isaliteral{5F}{\isacharunderscore}}SYSTEM}}}} names (see the \verb|$ISABELLE_HOME/etc/settings| file of the distribution).
9.52
9.53 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
9.54 command line. The optional \hyperlink{setting.ML-PLATFORM}{\mbox{\isa{\isatt{ML{\isaliteral{5F}{\isacharunderscore}}PLATFORM}}}} may specify the
9.55 @@ -429,7 +429,7 @@
9.56
9.57 \medskip The \verb|-W| option makes Isabelle enter a special
9.58 process wrapper for interaction via the Isabelle/Scala layer, see
9.59 - 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
9.60 + also \verb|~~/src/Pure/System/isabelle_process.scala|. The
9.61 protocol between the ML and JVM process is private to the
9.62 implementation.
9.63
10.1 --- a/doc-src/System/Thy/document/Misc.tex Mon Nov 29 23:41:09 2010 +0100
10.2 +++ b/doc-src/System/Thy/document/Misc.tex Tue Nov 30 00:12:29 2010 +0100
10.3 @@ -250,7 +250,7 @@
10.4 \begin{isamarkuptext}%
10.5 Refer to the \verb|IsaMakefile|s of the Isabelle distribution's
10.6 object-logics as a model for your own developments. For example,
10.7 - 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}}}}.%
10.8 + see \verb|~~/src/FOL/IsaMakefile|.%
10.9 \end{isamarkuptext}%
10.10 \isamarkuptrue%
10.11 %
10.12 @@ -363,8 +363,8 @@
10.13 sub-chunks separated by \isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E626F6C643E}{}\isactrlbold Y{\isaliteral{22}{\isachardoublequote}}}. Markup chunks start
10.14 with an empty sub-chunk, and a second empty sub-chunk indicates
10.15 close of an element. Any other non-empty chunk consists of plain
10.16 - 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
10.17 - \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}}}}.
10.18 + text. For example, see \verb|~~/src/Pure/General/yxml.ML| or
10.19 + \verb|~~/src/Pure/General/yxml.scala|.
10.20
10.21 YXML documents may be detected quickly by checking that the first
10.22 two characters are \isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E626F6C643E}{}\isactrlbold X\isaliteral{5C3C5E626F6C643E}{}\isactrlbold Y{\isaliteral{22}{\isachardoublequote}}}.%
11.1 --- a/doc-src/System/Thy/document/Presentation.tex Mon Nov 29 23:41:09 2010 +0100
11.2 +++ b/doc-src/System/Thy/document/Presentation.tex Tue Nov 30 00:12:29 2010 +0100
11.3 @@ -96,14 +96,14 @@
11.4
11.5 The easiest way to let Isabelle generate theory browsing information
11.6 for existing sessions is to append ``\verb|-i true|'' to the
11.7 - \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
11.8 + \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
11.9 example, add something like this to your Isabelle settings file
11.10
11.11 \begin{ttbox}
11.12 ISABELLE_USEDIR_OPTIONS="-i true"
11.13 \end{ttbox}
11.14
11.15 - 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
11.16 + and then change into the \verb|~~/src/FOL| directory and run
11.17 \verb|isabelle| \hyperlink{tool.make}{\mbox{\isa{\isatt{make}}}}, or even \verb|isabelle|
11.18 \hyperlink{tool.make}{\mbox{\isa{\isatt{make}}}}~\verb|all|. The presentation output will appear
11.19 in \verb|ISABELLE_BROWSER_INFO/FOL|, which usually refers to
11.20 @@ -111,7 +111,7 @@
11.21 \verb|-v true| will make the internal runs of \hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}}
11.22 more explicit about such details.
11.23
11.24 - 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}}}})
11.25 + Many standard Isabelle sessions (such as \verb|~~/src/HOL/ex|)
11.26 also provide actual printable documents. These are prepared
11.27 automatically as well if enabled like this, using the \verb|-d| option
11.28 \begin{ttbox}
11.29 @@ -451,7 +451,7 @@
11.30 manual editing of the generated \verb|IsaMakefile|, which is
11.31 meant to cover all of the sub-session directories at the same time
11.32 (this is the deeper reasong why \verb|IsaMakefile| is not made
11.33 - 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
11.34 + part of the initial session directory created by \verb|isabelle| \hyperlink{tool.mkdir}{\mbox{\isa{\isatt{mkdir}}}}). See \verb|~~/src/HOL/IsaMakefile| for
11.35 a full-blown example.%
11.36 \end{isamarkuptext}%
11.37 \isamarkuptrue%
11.38 @@ -621,7 +621,7 @@
11.39 \begin{isamarkuptext}%
11.40 Refer to the \verb|IsaMakefile|s of the Isabelle distribution's
11.41 object-logics as a model for your own developments. For example,
11.42 - 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
11.43 + 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
11.44 of \hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}} as well.%
11.45 \end{isamarkuptext}%
11.46 \isamarkuptrue%
11.47 @@ -670,7 +670,7 @@
11.48 fold text tagged as \isa{foo}. The builtin default is equivalent
11.49 to the tag specification ``\verb|+theory,+proof,+ML,+visible,-invisible|''; see also the {\LaTeX}
11.50 macros \verb|\isakeeptag|, \verb|\isadroptag|, and
11.51 - \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}}}}.
11.52 + \verb|\isafoldtag|, in \verb|~~/lib/texinputs/isabelle.sty|.
11.53
11.54 \medskip Document preparation requires a properly setup ``\verb|document|'' directory within the logic session sources. This
11.55 directory is supposed to contain all the files needed to produce the
11.56 @@ -701,7 +701,7 @@
11.57 containing all the theories.
11.58
11.59 The {\LaTeX} versions of the theories require some macros defined in
11.60 - \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;
11.61 + \verb|~~/lib/texinputs/isabelle.sty|. Doing \verb|\usepackage{isabelle}| in \verb|root.tex| should be fine;
11.62 the underlying Isabelle \hyperlink{tool.latex}{\mbox{\isa{\isatt{latex}}}} tool already includes an
11.63 appropriate path specification for {\TeX} inputs.
11.64
11.65 @@ -710,11 +710,11 @@
11.66 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
11.67 complete list of predefined Isabelle symbols. Users may invent
11.68 further symbols as well, just by providing {\LaTeX} macros in a
11.69 - 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
11.70 + similar fashion as in \verb|~~/lib/texinputs/isabellesym.sty| of
11.71 the distribution.
11.72
11.73 For proper setup of DVI and PDF documents (with hyperlinks and
11.74 - 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.
11.75 + bookmarks), we recommend to include \verb|~~/lib/texinputs/pdfsetup.sty| as well.
11.76
11.77 \medskip As a final step of document preparation within Isabelle,
11.78 \verb|isabelle| \hyperlink{tool.document}{\mbox{\isa{\isatt{document}}}}~\verb|-c| is run on the
12.1 --- a/doc-src/antiquote_setup.ML Mon Nov 29 23:41:09 2010 +0100
12.2 +++ b/doc-src/antiquote_setup.ML Tue Nov 30 00:12:29 2010 +0100
12.3 @@ -4,7 +4,7 @@
12.4 Auxiliary antiquotations for the Isabelle manuals.
12.5 *)
12.6
12.7 -structure AntiquoteSetup: sig end =
12.8 +structure Antiquote_Setup: sig end =
12.9 struct
12.10
12.11 (* misc utils *)
12.12 @@ -190,7 +190,6 @@
12.13 val _ = entity_antiqs no_check "" "inference";
12.14 val _ = entity_antiqs no_check "isatt" "executable";
12.15 val _ = entity_antiqs (K check_tool) "isatt" "tool";
12.16 -val _ = entity_antiqs (K (File.exists o Path.explode)) "isatt" "file";
12.17 val _ = entity_antiqs (K (can Thy_Info.get_theory)) "" "theory";
12.18 val _ = entity_antiqs no_check "" "ML antiquotation"; (* FIXME proper check *)
12.19
13.1 --- a/src/Pure/Thy/thy_output.ML Mon Nov 29 23:41:09 2010 +0100
13.2 +++ b/src/Pure/Thy/thy_output.ML Tue Nov 30 00:12:29 2010 +0100
13.3 @@ -575,7 +575,6 @@
13.4 val _ = basic_entities "prf" Attrib.thms (pretty_prf false);
13.5 val _ = basic_entities "full_prf" Attrib.thms (pretty_prf true);
13.6 val _ = basic_entity "theory" (Scan.lift Args.name) pretty_theory;
13.7 -
13.8 val _ = basic_entities_style "thm_style" (Term_Style.parse_bare -- Attrib.thms) pretty_thm_style;
13.9 val _ = basic_entity "term_style" (Term_Style.parse_bare -- Args.term) pretty_term_style;
13.10
13.11 @@ -622,6 +621,11 @@
13.12
13.13 (* ML text *)
13.14
13.15 +val verb_text =
13.16 + split_lines
13.17 + #> map (space_implode "\\verb,|," o map (enclose "\\verb|" "|") o space_explode "|")
13.18 + #> space_implode "\\isasep\\isanewline%\n";
13.19 +
13.20 local
13.21
13.22 fun ml_text name ml = antiquotation name (Scan.lift Args.name_source_position)
13.23 @@ -630,10 +634,7 @@
13.24 Symbol_Pos.content (Symbol_Pos.explode (txt, pos))
13.25 |> (if Config.get context quotes then quote else I)
13.26 |> (if Config.get context display then enclose "\\begin{verbatim}\n" "\n\\end{verbatim}"
13.27 - else
13.28 - split_lines
13.29 - #> map (space_implode "\\verb,|," o map (enclose "\\verb|" "|") o space_explode "|")
13.30 - #> space_implode "\\isasep\\isanewline%\n")));
13.31 + else verb_text)));
13.32
13.33 fun ml_enclose bg en pos txt =
13.34 ML_Lex.read Position.none bg @ ML_Lex.read pos txt @ ML_Lex.read Position.none en;
13.35 @@ -653,4 +654,12 @@
13.36
13.37 end;
13.38
13.39 +
13.40 +(* files *)
13.41 +
13.42 +val _ = antiquotation "file" (Scan.lift Args.name)
13.43 + (fn {context, ...} => fn path =>
13.44 + if File.exists (Path.explode path) then verb_text path
13.45 + else error ("Bad file: " ^ quote path));
13.46 +
13.47 end;