merged
authorwenzelm
Mon Nov 29 16:10:44 2010 +0100 (2010-11-29)
changeset 408055a195f11ef46
parent 40804 c8494f89690a
parent 40802 3cd23f676c5b
child 40807 eeaa59fb5ad8
child 40808 63276d22ea60
merged
     1.1 --- a/NEWS	Mon Nov 29 11:39:00 2010 +0100
     1.2 +++ b/NEWS	Mon Nov 29 16:10:44 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 11:39:00 2010 +0100
     2.2 +++ b/doc-src/IsarImplementation/Thy/document/Isar.tex	Mon Nov 29 16:10:44 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 11:39:00 2010 +0100
     3.2 +++ b/doc-src/IsarImplementation/Thy/document/ML.tex	Mon Nov 29 16:10:44 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 11:39:00 2010 +0100
     4.2 +++ b/doc-src/IsarImplementation/Thy/document/Tactic.tex	Mon Nov 29 16:10:44 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 11:39:00 2010 +0100
     5.2 +++ b/doc-src/IsarRef/Thy/Document_Preparation.thy	Mon Nov 29 16:10:44 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 11:39:00 2010 +0100
     6.2 +++ b/doc-src/IsarRef/Thy/document/Document_Preparation.tex	Mon Nov 29 16:10:44 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 11:39:00 2010 +0100
     7.2 +++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Mon Nov 29 16:10:44 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 11:39:00 2010 +0100
     8.2 +++ b/doc-src/IsarRef/Thy/document/Spec.tex	Mon Nov 29 16:10:44 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 11:39:00 2010 +0100
     9.2 +++ b/doc-src/System/Thy/document/Basics.tex	Mon Nov 29 16:10:44 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 11:39:00 2010 +0100
    10.2 +++ b/doc-src/System/Thy/document/Misc.tex	Mon Nov 29 16:10:44 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 11:39:00 2010 +0100
    11.2 +++ b/doc-src/System/Thy/document/Presentation.tex	Mon Nov 29 16:10:44 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 11:39:00 2010 +0100
    12.2 +++ b/doc-src/antiquote_setup.ML	Mon Nov 29 16:10:44 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 11:39:00 2010 +0100
    13.2 +++ b/src/Pure/Thy/thy_output.ML	Mon Nov 29 16:10:44 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;