--- 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 {*
--- 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. *}
--- 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
--- 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
--- 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.
*}
--- 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.
*}
--- 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.
--- 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"}.
--- 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,
--- 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;
--- 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 [];
--- 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;