# HG changeset patch # User wenzelm # Date 1291043444 -3600 # Node ID 5a195f11ef46b17c4d9b3ad8993c66e2b82898ca # Parent c8494f89690a5e4d395d0a2ec9e54e2beb4a28cc# Parent 3cd23f676c5bb73bf15ac429f458a312f4d0d74e merged diff -r c8494f89690a -r 5a195f11ef46 NEWS --- a/NEWS Mon Nov 29 11:39:00 2010 +0100 +++ b/NEWS Mon Nov 29 16:10:44 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 *** diff -r c8494f89690a -r 5a195f11ef46 doc-src/IsarImplementation/Thy/document/Isar.tex --- a/doc-src/IsarImplementation/Thy/document/Isar.tex Mon Nov 29 11:39:00 2010 +0100 +++ b/doc-src/IsarImplementation/Thy/document/Isar.tex Mon Nov 29 16:10:44 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% % diff -r c8494f89690a -r 5a195f11ef46 doc-src/IsarImplementation/Thy/document/ML.tex --- a/doc-src/IsarImplementation/Thy/document/ML.tex Mon Nov 29 11:39:00 2010 +0100 +++ b/doc-src/IsarImplementation/Thy/document/ML.tex Mon Nov 29 16:10:44 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}% diff -r c8494f89690a -r 5a195f11ef46 doc-src/IsarImplementation/Thy/document/Tactic.tex --- a/doc-src/IsarImplementation/Thy/document/Tactic.tex Mon Nov 29 11:39:00 2010 +0100 +++ b/doc-src/IsarImplementation/Thy/document/Tactic.tex Mon Nov 29 16:10:44 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 diff -r c8494f89690a -r 5a195f11ef46 doc-src/IsarRef/Thy/Document_Preparation.thy --- a/doc-src/IsarRef/Thy/Document_Preparation.thy Mon Nov 29 11:39:00 2010 +0100 +++ b/doc-src/IsarRef/Thy/Document_Preparation.thy Mon Nov 29 16:10:44 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} *} diff -r c8494f89690a -r 5a195f11ef46 doc-src/IsarRef/Thy/document/Document_Preparation.tex --- a/doc-src/IsarRef/Thy/document/Document_Preparation.tex Mon Nov 29 11:39:00 2010 +0100 +++ b/doc-src/IsarRef/Thy/document/Document_Preparation.tex Mon Nov 29 16:10:44 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 diff -r c8494f89690a -r 5a195f11ef46 doc-src/IsarRef/Thy/document/HOL_Specific.tex --- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex Mon Nov 29 11:39:00 2010 +0100 +++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex Mon Nov 29 16:10:44 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% diff -r c8494f89690a -r 5a195f11ef46 doc-src/IsarRef/Thy/document/Spec.tex --- a/doc-src/IsarRef/Thy/document/Spec.tex Mon Nov 29 11:39:00 2010 +0100 +++ b/doc-src/IsarRef/Thy/document/Spec.tex Mon Nov 29 16:10:44 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}% diff -r c8494f89690a -r 5a195f11ef46 doc-src/System/Thy/document/Basics.tex --- a/doc-src/System/Thy/document/Basics.tex Mon Nov 29 11:39:00 2010 +0100 +++ b/doc-src/System/Thy/document/Basics.tex Mon Nov 29 16:10:44 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. diff -r c8494f89690a -r 5a195f11ef46 doc-src/System/Thy/document/Misc.tex --- a/doc-src/System/Thy/document/Misc.tex Mon Nov 29 11:39:00 2010 +0100 +++ b/doc-src/System/Thy/document/Misc.tex Mon Nov 29 16:10:44 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}}}.% diff -r c8494f89690a -r 5a195f11ef46 doc-src/System/Thy/document/Presentation.tex --- a/doc-src/System/Thy/document/Presentation.tex Mon Nov 29 11:39:00 2010 +0100 +++ b/doc-src/System/Thy/document/Presentation.tex Mon Nov 29 16:10:44 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 diff -r c8494f89690a -r 5a195f11ef46 doc-src/antiquote_setup.ML --- a/doc-src/antiquote_setup.ML Mon Nov 29 11:39:00 2010 +0100 +++ b/doc-src/antiquote_setup.ML Mon Nov 29 16:10:44 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 *) diff -r c8494f89690a -r 5a195f11ef46 src/Pure/Thy/thy_output.ML --- a/src/Pure/Thy/thy_output.ML Mon Nov 29 11:39:00 2010 +0100 +++ b/src/Pure/Thy/thy_output.ML Mon Nov 29 16:10:44 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;