# HG changeset patch # User wenzelm # Date 1290974848 -3600 # Node ID 330eb65c9469f06c51fa40cb886e4f388fd75914 # Parent d44c87988a24d06bbdaa2dbc4b440e6e6e48ee20 Parse.liberal_name for document antiquotations and attributes; diff -r d44c87988a24 -r 330eb65c9469 doc-src/IsarImplementation/Thy/Isar.thy --- a/doc-src/IsarImplementation/Thy/Isar.thy Sun Nov 28 20:36:45 2010 +0100 +++ b/doc-src/IsarImplementation/Thy/Isar.thy Sun Nov 28 21:07:28 2010 +0100 @@ -440,7 +440,7 @@ text {* \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 - @{ML_functor Named_Thms} (see also @{"file" + @{ML_functor Named_Thms} (see also @{file "~~/src/Pure/Tools/named_thms.ML"}). *} ML {* diff -r d44c87988a24 -r 330eb65c9469 doc-src/IsarImplementation/Thy/ML.thy --- a/doc-src/IsarImplementation/Thy/ML.thy Sun Nov 28 20:36:45 2010 +0100 +++ b/doc-src/IsarImplementation/Thy/ML.thy Sun Nov 28 21:07:28 2010 +0100 @@ -63,7 +63,7 @@ text {* 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 @{"file" "~~/src/Pure/thm.ML"}, for example. + Paulson. See @{file "~~/src/Pure/thm.ML"}, for example. The header includes at least @{verbatim Title} and @{verbatim Author} entries, followed by a prose description of the purpose of @@ -1282,7 +1282,7 @@ integer type --- overloading of SML97 is disabled. Structure @{ML_struct IntInf} of SML97 is obsolete and superseded by - @{ML_struct Int}. Structure @{ML_struct Integer} in @{"file" + @{ML_struct Int}. Structure @{ML_struct Integer} in @{file "~~/src/Pure/General/integer.ML"} provides some additional operations. @@ -1330,7 +1330,7 @@ text {* Apart from @{ML Option.map} most operations defined in structure @{ML_struct Option} are alien to Isabelle/ML. The - operations shown above are defined in @{"file" + operations shown above are defined in @{file "~~/src/Pure/General/basics.ML"}, among others. *} @@ -1360,7 +1360,7 @@ \item @{ML member}, @{ML insert}, @{ML remove}, @{ML update} treat lists as a set-like container that maintains the order of elements. - See @{"file" "~~/src/Pure/library.ML"} for the full specifications + See @{file "~~/src/Pure/library.ML"} for the full specifications (written in ML). There are some further derived operations like @{ML union} or @{ML inter}. @@ -1407,7 +1407,7 @@ This way of merging lists is typical for context data (\secref{sec:context-data}). See also @{ML merge} as defined in - @{"file" "~~/src/Pure/library.ML"}. + @{file "~~/src/Pure/library.ML"}. *} @@ -1448,7 +1448,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 @{"file" + more heavy-duty table structure is defined in @{file "~~/src/Pure/General/table.ML"}; that version scales easily to thousands or millions of elements. *} @@ -1739,7 +1739,7 @@ \end{description} There are some further variants of the @{ML - Synchronized.guarded_access} combinator, see @{"file" + Synchronized.guarded_access} combinator, see @{file "~~/src/Pure/Concurrent/synchronized.ML"} for details. *} @@ -1766,7 +1766,7 @@ @{assert} (a <> b); *} -text {* \medskip See @{"file" "~~/src/Pure/Concurrent/mailbox.ML"} how +text {* \medskip See @{file "~~/src/Pure/Concurrent/mailbox.ML"} how to implement a mailbox as synchronized variable over a purely functional queue. *} diff -r d44c87988a24 -r 330eb65c9469 doc-src/IsarImplementation/Thy/Tactic.thy --- a/doc-src/IsarImplementation/Thy/Tactic.thy Sun Nov 28 20:36:45 2010 +0100 +++ b/doc-src/IsarImplementation/Thy/Tactic.thy Sun Nov 28 21:07:28 2010 +0100 @@ -182,7 +182,7 @@ \item Type @{ML_type tactic} represents tactics. The well-formedness conditions described above need to be observed. See - also @{"file" "~~/src/Pure/General/seq.ML"} for the underlying + also @{file "~~/src/Pure/General/seq.ML"} for the underlying implementation of lazy sequences. \item Type @{ML_type "int -> tactic"} represents tactics with diff -r d44c87988a24 -r 330eb65c9469 doc-src/IsarRef/Thy/Document_Preparation.thy --- a/doc-src/IsarRef/Thy/Document_Preparation.thy Sun Nov 28 20:36:45 2010 +0100 +++ b/doc-src/IsarRef/Thy/Document_Preparation.thy Sun Nov 28 21:07:28 2010 +0100 @@ -74,7 +74,7 @@ document generated from a theory. Each markup command takes a single @{syntax text} argument, which is passed as argument to a corresponding {\LaTeX} macro. The default macros provided by - @{"file" "~~/lib/texinputs/isabelle.sty"} can be redefined according + @{file "~~/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 @@ -449,7 +449,7 @@ \medskip Command tags merely produce certain markup environments for type-setting. The meaning of these is determined by {\LaTeX} - macros, as defined in @{"file" "~~/lib/texinputs/isabelle.sty"} or + macros, as defined in @{file "~~/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 d44c87988a24 -r 330eb65c9469 doc-src/IsarRef/Thy/HOL_Specific.thy --- a/doc-src/IsarRef/Thy/HOL_Specific.thy Sun Nov 28 20:36:45 2010 +0100 +++ b/doc-src/IsarRef/Thy/HOL_Specific.thy Sun Nov 28 21:07:28 2010 +0100 @@ -880,7 +880,7 @@ The @{method (HOL) coherent} method solves problems of \emph{Coherent Logic} \cite{Bezem-Coquand:2005}, which covers applications in confluence theory, lattice theory and projective - geometry. See @{"file" "~~/src/HOL/ex/Coherent.thy"} for some + geometry. See @{file "~~/src/HOL/ex/Coherent.thy"} for some examples. *} diff -r d44c87988a24 -r 330eb65c9469 doc-src/IsarRef/Thy/Spec.thy --- a/doc-src/IsarRef/Thy/Spec.thy Sun Nov 28 20:36:45 2010 +0100 +++ b/doc-src/IsarRef/Thy/Spec.thy Sun Nov 28 21:07:28 2010 +0100 @@ -1164,7 +1164,7 @@ \end{description} - See @{"file" "~~/src/HOL/ex/Iff_Oracle.thy"} for a worked example of + See @{file "~~/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. *} diff -r d44c87988a24 -r 330eb65c9469 doc-src/System/Thy/Basics.thy --- a/doc-src/System/Thy/Basics.thy Sun Nov 28 20:36:45 2010 +0100 +++ b/doc-src/System/Thy/Basics.thy Sun Nov 28 21:07:28 2010 +0100 @@ -53,7 +53,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 @{"file" + Occasionally, users would still want to put the @{file "$ISABELLE_HOME/bin"} directory into their shell's search path, but this is not required. *} @@ -78,10 +78,10 @@ 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 @{tool install} utility. Symbolic - links are admissible, but a plain copy of the @{"file" + links are admissible, but a plain copy of the @{file "$ISABELLE_HOME/bin"} files will not work! - \item The file @{"file" "$ISABELLE_HOME/etc/settings"} is run as a + \item The file @{file "$ISABELLE_HOME/etc/settings"} is run as a @{executable_ref bash} shell script with the auto-export option for variables enabled. @@ -99,10 +99,10 @@ "$HOME/.isabelle/IsabelleXXXX"}. Thus individual users may override the site-wide defaults. See also - file @{"file" "$ISABELLE_HOME/etc/user-settings.sample"} in the + file @{file "$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 @{"file" + definitely \emph{not} start with a full copy the basic @{file "$ISABELLE_HOME/etc/settings"}. This could cause very annoying maintainance problems later, when the Isabelle installation is updated or changed otherwise. @@ -179,7 +179,7 @@ ISABELLE_TOOL}@{text "\<^sup>*"}] are automatically set to the full path names of the @{executable "isabelle-process"} and @{executable isabelle} executables, respectively. Thus other tools and scripts - need not assume that the @{"file" "$ISABELLE_HOME/bin"} directory is + need not assume that the @{file "$ISABELLE_HOME/bin"} directory is on the current search path of the shell. \item[@{setting_def ISABELLE_IDENTIFIER}@{text "\<^sup>*"}] refers @@ -190,7 +190,7 @@ @{setting_def ML_OPTIONS}, @{setting_def ML_PLATFORM}, @{setting_def ML_IDENTIFIER}@{text "\<^sup>*"}] specify the underlying ML system to be used for Isabelle. There is only a fixed set of admissable - @{setting ML_SYSTEM} names (see the @{"file" + @{setting ML_SYSTEM} names (see the @{file "$ISABELLE_HOME/etc/settings"} file of the distribution). The actual compiler binary will be run from the directory @{setting @@ -418,7 +418,7 @@ \medskip The @{verbatim "-W"} option makes Isabelle enter a special process wrapper for interaction via the Isabelle/Scala layer, see - also @{"file" "~~/src/Pure/System/isabelle_process.scala"}. The + also @{file "~~/src/Pure/System/isabelle_process.scala"}. The protocol between the ML and JVM process is private to the implementation. diff -r d44c87988a24 -r 330eb65c9469 doc-src/System/Thy/Misc.thy --- a/doc-src/System/Thy/Misc.thy Sun Nov 28 20:36:45 2010 +0100 +++ b/doc-src/System/Thy/Misc.thy Sun Nov 28 21:07:28 2010 +0100 @@ -219,7 +219,7 @@ text {* Refer to the @{verbatim IsaMakefile}s of the Isabelle distribution's object-logics as a model for your own developments. For example, - see @{"file" "~~/src/FOL/IsaMakefile"}. + see @{file "~~/src/FOL/IsaMakefile"}. *} @@ -324,8 +324,8 @@ sub-chunks separated by @{text "\<^bold>Y"}. 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 @{"file" "~~/src/Pure/General/yxml.ML"} or - @{"file" "~~/src/Pure/General/yxml.scala"}. + text. For example, see @{file "~~/src/Pure/General/yxml.ML"} or + @{file "~~/src/Pure/General/yxml.scala"}. YXML documents may be detected quickly by checking that the first two characters are @{text "\<^bold>X\<^bold>Y"}. diff -r d44c87988a24 -r 330eb65c9469 doc-src/System/Thy/Presentation.thy --- a/doc-src/System/Thy/Presentation.thy Sun Nov 28 20:36:45 2010 +0100 +++ b/doc-src/System/Thy/Presentation.thy Sun Nov 28 21:07:28 2010 +0100 @@ -80,14 +80,14 @@ The easiest way to let Isabelle generate theory browsing information for existing sessions is to append ``@{verbatim "-i true"}'' to the @{setting_ref ISABELLE_USEDIR_OPTIONS} before invoking @{verbatim - isabelle} @{tool make} (or @{"file" "$ISABELLE_HOME/build"}). For + isabelle} @{tool make} (or @{file "$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 @{"file" "~~/src/FOL"} directory and run + and then change into the @{file "~~/src/FOL"} directory and run @{verbatim isabelle} @{tool make}, or even @{verbatim isabelle} @{tool make}~@{verbatim all}. The presentation output will appear in @{verbatim "ISABELLE_BROWSER_INFO/FOL"}, which usually refers to @@ -96,7 +96,7 @@ @{verbatim "-v true"} will make the internal runs of @{tool usedir} more explicit about such details. - Many standard Isabelle sessions (such as @{"file" "~~/src/HOL/ex"}) + Many standard Isabelle sessions (such as @{file "~~/src/HOL/ex"}) also provide actual printable documents. These are prepared automatically as well if enabled like this, using the @{verbatim "-d"} option @@ -427,7 +427,7 @@ meant to cover all of the sub-session directories at the same time (this is the deeper reasong why @{verbatim IsaMakefile} is not made part of the initial session directory created by @{verbatim - isabelle} @{tool mkdir}). See @{"file" "~~/src/HOL/IsaMakefile"} for + isabelle} @{tool mkdir}). See @{file "~~/src/HOL/IsaMakefile"} for a full-blown example. *} @@ -604,7 +604,7 @@ text {* Refer to the @{verbatim IsaMakefile}s of the Isabelle distribution's object-logics as a model for your own developments. For example, - see @{"file" "~~/src/FOL/IsaMakefile"}. The Isabelle @{tool_ref + see @{file "~~/src/FOL/IsaMakefile"}. The Isabelle @{tool_ref mkdir} tool creates @{verbatim IsaMakefile}s with proper invocation of @{tool usedir} as well. *} @@ -656,7 +656,7 @@ to the tag specification ``@{verbatim "+theory,+proof,+ML,+visible,-invisible"}''; see also the {\LaTeX} macros @{verbatim "\\isakeeptag"}, @{verbatim "\\isadroptag"}, and - @{verbatim "\\isafoldtag"}, in @{"file" + @{verbatim "\\isafoldtag"}, in @{file "~~/lib/texinputs/isabelle.sty"}. \medskip Document preparation requires a properly setup ``@{verbatim @@ -689,7 +689,7 @@ containing all the theories. The {\LaTeX} versions of the theories require some macros defined in - @{"file" "~~/lib/texinputs/isabelle.sty"}. Doing @{verbatim + @{file "~~/lib/texinputs/isabelle.sty"}. Doing @{verbatim "\\usepackage{isabelle}"} in @{verbatim root.tex} should be fine; the underlying Isabelle @{tool latex} tool already includes an appropriate path specification for {\TeX} inputs. @@ -702,11 +702,11 @@ "<"}@{text foo}@{verbatim ">"}, 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 @{"file" "~~/lib/texinputs/isabellesym.sty"} of + similar fashion as in @{file "~~/lib/texinputs/isabellesym.sty"} of the distribution. For proper setup of DVI and PDF documents (with hyperlinks and - bookmarks), we recommend to include @{"file" + bookmarks), we recommend to include @{file "~~/lib/texinputs/pdfsetup.sty"} as well. \medskip As a final step of document preparation within Isabelle, diff -r d44c87988a24 -r 330eb65c9469 src/Pure/Isar/parse.ML --- a/src/Pure/Isar/parse.ML Sun Nov 28 20:36:45 2010 +0100 +++ b/src/Pure/Isar/parse.ML Sun Nov 28 21:07:28 2010 +0100 @@ -63,6 +63,7 @@ val xname: xstring parser val text: string parser val path: Path.T parser + val liberal_name: xstring parser val parname: string parser val parbinding: binding parser val sort: string parser @@ -234,6 +235,8 @@ val text = group "text" (short_ident || long_ident || sym_ident || string || number || verbatim); val path = group "file name/path specification" name >> Path.explode; +val liberal_name = keyword_ident_or_symbolic || xname; + val parname = Scan.optional ($$$ "(" |-- name --| $$$ ")") ""; val parbinding = Scan.optional ($$$ "(" |-- binding --| $$$ ")") Binding.empty; diff -r d44c87988a24 -r 330eb65c9469 src/Pure/Isar/parse_spec.ML --- a/src/Pure/Isar/parse_spec.ML Sun Nov 28 20:36:45 2010 +0100 +++ b/src/Pure/Isar/parse_spec.ML Sun Nov 28 21:07:28 2010 +0100 @@ -37,10 +37,7 @@ (* theorem specifications *) -val attrib = - Parse.position ((Parse.keyword_ident_or_symbolic || Parse.xname) -- Parse.!!! Args.parse) - >> Args.src; - +val attrib = Parse.position (Parse.liberal_name -- Parse.!!! Args.parse) >> Args.src; val attribs = Parse.$$$ "[" |-- Parse.list attrib --| Parse.$$$ "]"; val opt_attribs = Scan.optional attribs []; diff -r d44c87988a24 -r 330eb65c9469 src/Pure/Thy/thy_output.ML --- a/src/Pure/Thy/thy_output.ML Sun Nov 28 20:36:45 2010 +0100 +++ b/src/Pure/Thy/thy_output.ML Sun Nov 28 21:07:28 2010 +0100 @@ -162,7 +162,8 @@ in val antiq = - Parse.!!! (Parse.position Parse.xname -- properties -- Args.parse --| Scan.ahead Parse.eof) + Parse.!!! + (Parse.position Parse.liberal_name -- properties -- Args.parse --| Scan.ahead Parse.eof) >> (fn (((x, pos), y), z) => (y, Args.src ((x, z), pos))); end;