Parse.liberal_name for document antiquotations and attributes;
authorwenzelm
Sun Nov 28 21:07:28 2010 +0100 (2010-11-28)
changeset 40800330eb65c9469
parent 40799 d44c87988a24
child 40801 6cfacec435e6
child 40803 3f66ea311d44
child 40812 ff16e22e8776
Parse.liberal_name for document antiquotations and attributes;
doc-src/IsarImplementation/Thy/Isar.thy
doc-src/IsarImplementation/Thy/ML.thy
doc-src/IsarImplementation/Thy/Tactic.thy
doc-src/IsarRef/Thy/Document_Preparation.thy
doc-src/IsarRef/Thy/HOL_Specific.thy
doc-src/IsarRef/Thy/Spec.thy
doc-src/System/Thy/Basics.thy
doc-src/System/Thy/Misc.thy
doc-src/System/Thy/Presentation.thy
src/Pure/Isar/parse.ML
src/Pure/Isar/parse_spec.ML
src/Pure/Thy/thy_output.ML
     1.1 --- a/doc-src/IsarImplementation/Thy/Isar.thy	Sun Nov 28 20:36:45 2010 +0100
     1.2 +++ b/doc-src/IsarImplementation/Thy/Isar.thy	Sun Nov 28 21:07:28 2010 +0100
     1.3 @@ -440,7 +440,7 @@
     1.4  text {* \medskip Apart from explicit arguments, common proof methods
     1.5    typically work with a default configuration provided by the context.
     1.6    As a shortcut to rule management we use a cheap solution via functor
     1.7 -  @{ML_functor Named_Thms} (see also @{"file"
     1.8 +  @{ML_functor Named_Thms} (see also @{file
     1.9    "~~/src/Pure/Tools/named_thms.ML"}).  *}
    1.10  
    1.11  ML {*
     2.1 --- a/doc-src/IsarImplementation/Thy/ML.thy	Sun Nov 28 20:36:45 2010 +0100
     2.2 +++ b/doc-src/IsarImplementation/Thy/ML.thy	Sun Nov 28 21:07:28 2010 +0100
     2.3 @@ -63,7 +63,7 @@
     2.4  text {* Isabelle source files have a certain standardized header
     2.5    format (with precise spacing) that follows ancient traditions
     2.6    reaching back to the earliest versions of the system by Larry
     2.7 -  Paulson.  See @{"file" "~~/src/Pure/thm.ML"}, for example.
     2.8 +  Paulson.  See @{file "~~/src/Pure/thm.ML"}, for example.
     2.9  
    2.10    The header includes at least @{verbatim Title} and @{verbatim
    2.11    Author} entries, followed by a prose description of the purpose of
    2.12 @@ -1282,7 +1282,7 @@
    2.13    integer type --- overloading of SML97 is disabled.
    2.14  
    2.15    Structure @{ML_struct IntInf} of SML97 is obsolete and superseded by
    2.16 -  @{ML_struct Int}.  Structure @{ML_struct Integer} in @{"file"
    2.17 +  @{ML_struct Int}.  Structure @{ML_struct Integer} in @{file
    2.18    "~~/src/Pure/General/integer.ML"} provides some additional
    2.19    operations.
    2.20  
    2.21 @@ -1330,7 +1330,7 @@
    2.22  
    2.23  text {* Apart from @{ML Option.map} most operations defined in
    2.24    structure @{ML_struct Option} are alien to Isabelle/ML.  The
    2.25 -  operations shown above are defined in @{"file"
    2.26 +  operations shown above are defined in @{file
    2.27    "~~/src/Pure/General/basics.ML"}, among others.  *}
    2.28  
    2.29  
    2.30 @@ -1360,7 +1360,7 @@
    2.31  
    2.32    \item @{ML member}, @{ML insert}, @{ML remove}, @{ML update} treat
    2.33    lists as a set-like container that maintains the order of elements.
    2.34 -  See @{"file" "~~/src/Pure/library.ML"} for the full specifications
    2.35 +  See @{file "~~/src/Pure/library.ML"} for the full specifications
    2.36    (written in ML).  There are some further derived operations like
    2.37    @{ML union} or @{ML inter}.
    2.38  
    2.39 @@ -1407,7 +1407,7 @@
    2.40  
    2.41    This way of merging lists is typical for context data
    2.42    (\secref{sec:context-data}).  See also @{ML merge} as defined in
    2.43 -  @{"file" "~~/src/Pure/library.ML"}.
    2.44 +  @{file "~~/src/Pure/library.ML"}.
    2.45  *}
    2.46  
    2.47  
    2.48 @@ -1448,7 +1448,7 @@
    2.49  
    2.50    Association lists are adequate as simple and light-weight
    2.51    implementation of finite mappings in many practical situations.  A
    2.52 -  more heavy-duty table structure is defined in @{"file"
    2.53 +  more heavy-duty table structure is defined in @{file
    2.54    "~~/src/Pure/General/table.ML"}; that version scales easily to
    2.55    thousands or millions of elements.
    2.56  *}
    2.57 @@ -1739,7 +1739,7 @@
    2.58    \end{description}
    2.59  
    2.60    There are some further variants of the @{ML
    2.61 -  Synchronized.guarded_access} combinator, see @{"file"
    2.62 +  Synchronized.guarded_access} combinator, see @{file
    2.63    "~~/src/Pure/Concurrent/synchronized.ML"} for details.
    2.64  *}
    2.65  
    2.66 @@ -1766,7 +1766,7 @@
    2.67    @{assert} (a <> b);
    2.68  *}
    2.69  
    2.70 -text {* \medskip See @{"file" "~~/src/Pure/Concurrent/mailbox.ML"} how
    2.71 +text {* \medskip See @{file "~~/src/Pure/Concurrent/mailbox.ML"} how
    2.72    to implement a mailbox as synchronized variable over a purely
    2.73    functional queue. *}
    2.74  
     3.1 --- a/doc-src/IsarImplementation/Thy/Tactic.thy	Sun Nov 28 20:36:45 2010 +0100
     3.2 +++ b/doc-src/IsarImplementation/Thy/Tactic.thy	Sun Nov 28 21:07:28 2010 +0100
     3.3 @@ -182,7 +182,7 @@
     3.4  
     3.5    \item Type @{ML_type tactic} represents tactics.  The
     3.6    well-formedness conditions described above need to be observed.  See
     3.7 -  also @{"file" "~~/src/Pure/General/seq.ML"} for the underlying
     3.8 +  also @{file "~~/src/Pure/General/seq.ML"} for the underlying
     3.9    implementation of lazy sequences.
    3.10  
    3.11    \item Type @{ML_type "int -> tactic"} represents tactics with
     4.1 --- a/doc-src/IsarRef/Thy/Document_Preparation.thy	Sun Nov 28 20:36:45 2010 +0100
     4.2 +++ b/doc-src/IsarRef/Thy/Document_Preparation.thy	Sun Nov 28 21:07:28 2010 +0100
     4.3 @@ -74,7 +74,7 @@
     4.4    document generated from a theory.  Each markup command takes a
     4.5    single @{syntax text} argument, which is passed as argument to a
     4.6    corresponding {\LaTeX} macro.  The default macros provided by
     4.7 -  @{"file" "~~/lib/texinputs/isabelle.sty"} can be redefined according
     4.8 +  @{file "~~/lib/texinputs/isabelle.sty"} can be redefined according
     4.9    to the needs of the underlying document and {\LaTeX} styles.
    4.10  
    4.11    Note that formal comments (\secref{sec:comments}) are similar to
    4.12 @@ -449,7 +449,7 @@
    4.13  
    4.14    \medskip Command tags merely produce certain markup environments for
    4.15    type-setting.  The meaning of these is determined by {\LaTeX}
    4.16 -  macros, as defined in @{"file" "~~/lib/texinputs/isabelle.sty"} or
    4.17 +  macros, as defined in @{file "~~/lib/texinputs/isabelle.sty"} or
    4.18    by the document author.  The Isabelle document preparation tools
    4.19    also provide some high-level options to specify the meaning of
    4.20    arbitrary tags to ``keep'', ``drop'', or ``fold'' the corresponding
     5.1 --- a/doc-src/IsarRef/Thy/HOL_Specific.thy	Sun Nov 28 20:36:45 2010 +0100
     5.2 +++ b/doc-src/IsarRef/Thy/HOL_Specific.thy	Sun Nov 28 21:07:28 2010 +0100
     5.3 @@ -880,7 +880,7 @@
     5.4    The @{method (HOL) coherent} method solves problems of
     5.5    \emph{Coherent Logic} \cite{Bezem-Coquand:2005}, which covers
     5.6    applications in confluence theory, lattice theory and projective
     5.7 -  geometry.  See @{"file" "~~/src/HOL/ex/Coherent.thy"} for some
     5.8 +  geometry.  See @{file "~~/src/HOL/ex/Coherent.thy"} for some
     5.9    examples.
    5.10  *}
    5.11  
     6.1 --- a/doc-src/IsarRef/Thy/Spec.thy	Sun Nov 28 20:36:45 2010 +0100
     6.2 +++ b/doc-src/IsarRef/Thy/Spec.thy	Sun Nov 28 21:07:28 2010 +0100
     6.3 @@ -1164,7 +1164,7 @@
     6.4  
     6.5    \end{description}
     6.6  
     6.7 -  See @{"file" "~~/src/HOL/ex/Iff_Oracle.thy"} for a worked example of
     6.8 +  See @{file "~~/src/HOL/ex/Iff_Oracle.thy"} for a worked example of
     6.9    defining a new primitive rule as oracle, and turning it into a proof
    6.10    method.
    6.11  *}
     7.1 --- a/doc-src/System/Thy/Basics.thy	Sun Nov 28 20:36:45 2010 +0100
     7.2 +++ b/doc-src/System/Thy/Basics.thy	Sun Nov 28 21:07:28 2010 +0100
     7.3 @@ -53,7 +53,7 @@
     7.4    their shell startup scripts, before being able to actually run the
     7.5    program. Isabelle requires none such administrative chores of its
     7.6    end-users --- the executables can be invoked straight away.
     7.7 -  Occasionally, users would still want to put the @{"file"
     7.8 +  Occasionally, users would still want to put the @{file
     7.9    "$ISABELLE_HOME/bin"} directory into their shell's search path, but
    7.10    this is not required.
    7.11  *}
    7.12 @@ -78,10 +78,10 @@
    7.13    note that the Isabelle executables either have to be run from their
    7.14    original location in the distribution directory, or via the
    7.15    executable objects created by the @{tool install} utility.  Symbolic
    7.16 -  links are admissible, but a plain copy of the @{"file"
    7.17 +  links are admissible, but a plain copy of the @{file
    7.18    "$ISABELLE_HOME/bin"} files will not work!
    7.19  
    7.20 -  \item The file @{"file" "$ISABELLE_HOME/etc/settings"} is run as a
    7.21 +  \item The file @{file "$ISABELLE_HOME/etc/settings"} is run as a
    7.22    @{executable_ref bash} shell script with the auto-export option for
    7.23    variables enabled.
    7.24    
    7.25 @@ -99,10 +99,10 @@
    7.26    "$HOME/.isabelle/IsabelleXXXX"}.
    7.27    
    7.28    Thus individual users may override the site-wide defaults.  See also
    7.29 -  file @{"file" "$ISABELLE_HOME/etc/user-settings.sample"} in the
    7.30 +  file @{file "$ISABELLE_HOME/etc/user-settings.sample"} in the
    7.31    distribution.  Typically, a user settings file would contain only a
    7.32    few lines, just the assigments that are really changed.  One should
    7.33 -  definitely \emph{not} start with a full copy the basic @{"file"
    7.34 +  definitely \emph{not} start with a full copy the basic @{file
    7.35    "$ISABELLE_HOME/etc/settings"}. This could cause very annoying
    7.36    maintainance problems later, when the Isabelle installation is
    7.37    updated or changed otherwise.
    7.38 @@ -179,7 +179,7 @@
    7.39    ISABELLE_TOOL}@{text "\<^sup>*"}] are automatically set to the full path
    7.40    names of the @{executable "isabelle-process"} and @{executable
    7.41    isabelle} executables, respectively.  Thus other tools and scripts
    7.42 -  need not assume that the @{"file" "$ISABELLE_HOME/bin"} directory is
    7.43 +  need not assume that the @{file "$ISABELLE_HOME/bin"} directory is
    7.44    on the current search path of the shell.
    7.45    
    7.46    \item[@{setting_def ISABELLE_IDENTIFIER}@{text "\<^sup>*"}] refers
    7.47 @@ -190,7 +190,7 @@
    7.48    @{setting_def ML_OPTIONS}, @{setting_def ML_PLATFORM}, @{setting_def
    7.49    ML_IDENTIFIER}@{text "\<^sup>*"}] specify the underlying ML system
    7.50    to be used for Isabelle.  There is only a fixed set of admissable
    7.51 -  @{setting ML_SYSTEM} names (see the @{"file"
    7.52 +  @{setting ML_SYSTEM} names (see the @{file
    7.53    "$ISABELLE_HOME/etc/settings"} file of the distribution).
    7.54    
    7.55    The actual compiler binary will be run from the directory @{setting
    7.56 @@ -418,7 +418,7 @@
    7.57  
    7.58    \medskip The @{verbatim "-W"} option makes Isabelle enter a special
    7.59    process wrapper for interaction via the Isabelle/Scala layer, see
    7.60 -  also @{"file" "~~/src/Pure/System/isabelle_process.scala"}.  The
    7.61 +  also @{file "~~/src/Pure/System/isabelle_process.scala"}.  The
    7.62    protocol between the ML and JVM process is private to the
    7.63    implementation.
    7.64  
     8.1 --- a/doc-src/System/Thy/Misc.thy	Sun Nov 28 20:36:45 2010 +0100
     8.2 +++ b/doc-src/System/Thy/Misc.thy	Sun Nov 28 21:07:28 2010 +0100
     8.3 @@ -219,7 +219,7 @@
     8.4  text {*
     8.5    Refer to the @{verbatim IsaMakefile}s of the Isabelle distribution's
     8.6    object-logics as a model for your own developments.  For example,
     8.7 -  see @{"file" "~~/src/FOL/IsaMakefile"}.
     8.8 +  see @{file "~~/src/FOL/IsaMakefile"}.
     8.9  *}
    8.10  
    8.11  
    8.12 @@ -324,8 +324,8 @@
    8.13    sub-chunks separated by @{text "\<^bold>Y"}.  Markup chunks start
    8.14    with an empty sub-chunk, and a second empty sub-chunk indicates
    8.15    close of an element.  Any other non-empty chunk consists of plain
    8.16 -  text.  For example, see @{"file" "~~/src/Pure/General/yxml.ML"} or
    8.17 -  @{"file" "~~/src/Pure/General/yxml.scala"}.
    8.18 +  text.  For example, see @{file "~~/src/Pure/General/yxml.ML"} or
    8.19 +  @{file "~~/src/Pure/General/yxml.scala"}.
    8.20  
    8.21    YXML documents may be detected quickly by checking that the first
    8.22    two characters are @{text "\<^bold>X\<^bold>Y"}.
     9.1 --- a/doc-src/System/Thy/Presentation.thy	Sun Nov 28 20:36:45 2010 +0100
     9.2 +++ b/doc-src/System/Thy/Presentation.thy	Sun Nov 28 21:07:28 2010 +0100
     9.3 @@ -80,14 +80,14 @@
     9.4    The easiest way to let Isabelle generate theory browsing information
     9.5    for existing sessions is to append ``@{verbatim "-i true"}'' to the
     9.6    @{setting_ref ISABELLE_USEDIR_OPTIONS} before invoking @{verbatim
     9.7 -  isabelle} @{tool make} (or @{"file" "$ISABELLE_HOME/build"}).  For
     9.8 +  isabelle} @{tool make} (or @{file "$ISABELLE_HOME/build"}).  For
     9.9    example, add something like this to your Isabelle settings file
    9.10  
    9.11  \begin{ttbox}
    9.12  ISABELLE_USEDIR_OPTIONS="-i true"
    9.13  \end{ttbox}
    9.14  
    9.15 -  and then change into the @{"file" "~~/src/FOL"} directory and run
    9.16 +  and then change into the @{file "~~/src/FOL"} directory and run
    9.17    @{verbatim isabelle} @{tool make}, or even @{verbatim isabelle}
    9.18    @{tool make}~@{verbatim all}.  The presentation output will appear
    9.19    in @{verbatim "ISABELLE_BROWSER_INFO/FOL"}, which usually refers to
    9.20 @@ -96,7 +96,7 @@
    9.21    @{verbatim "-v true"} will make the internal runs of @{tool usedir}
    9.22    more explicit about such details.
    9.23  
    9.24 -  Many standard Isabelle sessions (such as @{"file" "~~/src/HOL/ex"})
    9.25 +  Many standard Isabelle sessions (such as @{file "~~/src/HOL/ex"})
    9.26    also provide actual printable documents.  These are prepared
    9.27    automatically as well if enabled like this, using the @{verbatim
    9.28    "-d"} option
    9.29 @@ -427,7 +427,7 @@
    9.30    meant to cover all of the sub-session directories at the same time
    9.31    (this is the deeper reasong why @{verbatim IsaMakefile} is not made
    9.32    part of the initial session directory created by @{verbatim
    9.33 -  isabelle} @{tool mkdir}).  See @{"file" "~~/src/HOL/IsaMakefile"} for
    9.34 +  isabelle} @{tool mkdir}).  See @{file "~~/src/HOL/IsaMakefile"} for
    9.35    a full-blown example.
    9.36  *}
    9.37  
    9.38 @@ -604,7 +604,7 @@
    9.39  text {*
    9.40    Refer to the @{verbatim IsaMakefile}s of the Isabelle distribution's
    9.41    object-logics as a model for your own developments.  For example,
    9.42 -  see @{"file" "~~/src/FOL/IsaMakefile"}.  The Isabelle @{tool_ref
    9.43 +  see @{file "~~/src/FOL/IsaMakefile"}.  The Isabelle @{tool_ref
    9.44    mkdir} tool creates @{verbatim IsaMakefile}s with proper invocation
    9.45    of @{tool usedir} as well.
    9.46  *}
    9.47 @@ -656,7 +656,7 @@
    9.48    to the tag specification ``@{verbatim
    9.49    "+theory,+proof,+ML,+visible,-invisible"}''; see also the {\LaTeX}
    9.50    macros @{verbatim "\\isakeeptag"}, @{verbatim "\\isadroptag"}, and
    9.51 -  @{verbatim "\\isafoldtag"}, in @{"file"
    9.52 +  @{verbatim "\\isafoldtag"}, in @{file
    9.53    "~~/lib/texinputs/isabelle.sty"}.
    9.54  
    9.55    \medskip Document preparation requires a properly setup ``@{verbatim
    9.56 @@ -689,7 +689,7 @@
    9.57    containing all the theories.
    9.58  
    9.59    The {\LaTeX} versions of the theories require some macros defined in
    9.60 -  @{"file" "~~/lib/texinputs/isabelle.sty"}.  Doing @{verbatim
    9.61 +  @{file "~~/lib/texinputs/isabelle.sty"}.  Doing @{verbatim
    9.62    "\\usepackage{isabelle}"} in @{verbatim root.tex} should be fine;
    9.63    the underlying Isabelle @{tool latex} tool already includes an
    9.64    appropriate path specification for {\TeX} inputs.
    9.65 @@ -702,11 +702,11 @@
    9.66    "<"}@{text foo}@{verbatim ">"}, see \cite{isabelle-implementation} for a
    9.67    complete list of predefined Isabelle symbols.  Users may invent
    9.68    further symbols as well, just by providing {\LaTeX} macros in a
    9.69 -  similar fashion as in @{"file" "~~/lib/texinputs/isabellesym.sty"} of
    9.70 +  similar fashion as in @{file "~~/lib/texinputs/isabellesym.sty"} of
    9.71    the distribution.
    9.72  
    9.73    For proper setup of DVI and PDF documents (with hyperlinks and
    9.74 -  bookmarks), we recommend to include @{"file"
    9.75 +  bookmarks), we recommend to include @{file
    9.76    "~~/lib/texinputs/pdfsetup.sty"} as well.
    9.77  
    9.78    \medskip As a final step of document preparation within Isabelle,
    10.1 --- a/src/Pure/Isar/parse.ML	Sun Nov 28 20:36:45 2010 +0100
    10.2 +++ b/src/Pure/Isar/parse.ML	Sun Nov 28 21:07:28 2010 +0100
    10.3 @@ -63,6 +63,7 @@
    10.4    val xname: xstring parser
    10.5    val text: string parser
    10.6    val path: Path.T parser
    10.7 +  val liberal_name: xstring parser
    10.8    val parname: string parser
    10.9    val parbinding: binding parser
   10.10    val sort: string parser
   10.11 @@ -234,6 +235,8 @@
   10.12  val text = group "text" (short_ident || long_ident || sym_ident || string || number || verbatim);
   10.13  val path = group "file name/path specification" name >> Path.explode;
   10.14  
   10.15 +val liberal_name = keyword_ident_or_symbolic || xname;
   10.16 +
   10.17  val parname = Scan.optional ($$$ "(" |-- name --| $$$ ")") "";
   10.18  val parbinding = Scan.optional ($$$ "(" |-- binding --| $$$ ")") Binding.empty;
   10.19  
    11.1 --- a/src/Pure/Isar/parse_spec.ML	Sun Nov 28 20:36:45 2010 +0100
    11.2 +++ b/src/Pure/Isar/parse_spec.ML	Sun Nov 28 21:07:28 2010 +0100
    11.3 @@ -37,10 +37,7 @@
    11.4  
    11.5  (* theorem specifications *)
    11.6  
    11.7 -val attrib =
    11.8 -  Parse.position ((Parse.keyword_ident_or_symbolic || Parse.xname) -- Parse.!!! Args.parse)
    11.9 -  >> Args.src;
   11.10 -
   11.11 +val attrib = Parse.position (Parse.liberal_name -- Parse.!!! Args.parse) >> Args.src;
   11.12  val attribs = Parse.$$$ "[" |-- Parse.list attrib --| Parse.$$$ "]";
   11.13  val opt_attribs = Scan.optional attribs [];
   11.14  
    12.1 --- a/src/Pure/Thy/thy_output.ML	Sun Nov 28 20:36:45 2010 +0100
    12.2 +++ b/src/Pure/Thy/thy_output.ML	Sun Nov 28 21:07:28 2010 +0100
    12.3 @@ -162,7 +162,8 @@
    12.4  in
    12.5  
    12.6  val antiq =
    12.7 -  Parse.!!! (Parse.position Parse.xname -- properties -- Args.parse --| Scan.ahead Parse.eof)
    12.8 +  Parse.!!!
    12.9 +    (Parse.position Parse.liberal_name -- properties -- Args.parse --| Scan.ahead Parse.eof)
   12.10    >> (fn (((x, pos), y), z) => (y, Args.src ((x, z), pos)));
   12.11  
   12.12  end;