--- a/NEWS Thu Aug 11 18:26:16 2016 +0200
+++ b/NEWS Thu Aug 11 18:26:44 2016 +0200
@@ -137,6 +137,18 @@
accordingly: optional abbrevs need to go into the new 'abbrevs' section.
+*** Document preparation ***
+
+* Document antiquotations for file-systems paths are more specific and
+diverse:
+
+ @{path NAME} -- no check (formerly @{file_unchecked})
+ @{file NAME} -- plain file (formerly file or directory)
+ @{dir NAME} -- directory (formerly subsumed by @{file})
+
+Minor INCOMPATIBILITY.
+
+
*** Isar ***
* The defining position of a literal fact \<open>prop\<close> is maintained more
@@ -624,6 +636,9 @@
*** ML ***
+* ML antiquotation @{path} is superseded by @{file}, which ensures that
+the argument is a plain file. Minor INCOMPATIBILITY.
+
* Integer.gcd and Integer.lcm use efficient operations from the Poly/ML
library (notably for big integers). Subtle change of semantics:
Integer.gcd and Integer.lcm both normalize the sign, results are never
--- a/src/Doc/Codegen/Adaptation.thy Thu Aug 11 18:26:16 2016 +0200
+++ b/src/Doc/Codegen/Adaptation.thy Thu Aug 11 18:26:44 2016 +0200
@@ -154,7 +154,7 @@
The @{theory HOL} @{theory Main} theory already provides a code
generator setup which should be suitable for most applications.
Common extensions and modifications are available by certain
- theories in @{file "~~/src/HOL/Library"}; beside being useful in
+ theories in @{dir "~~/src/HOL/Library"}; beside being useful in
applications, they may serve as a tutorial for customising the code
generator setup (see below \secref{sec:adaptation_mechanisms}).
--- a/src/Doc/Codegen/Further.thy Thu Aug 11 18:26:16 2016 +0200
+++ b/src/Doc/Codegen/Further.thy Thu Aug 11 18:26:44 2016 +0200
@@ -148,7 +148,7 @@
subsection \<open>Parallel computation\<close>
text \<open>
- Theory @{text Parallel} in @{file "~~/src/HOL/Library"} contains
+ Theory @{text Parallel} in @{dir "~~/src/HOL/Library"} contains
operations to exploit parallelism inside the Isabelle/ML
runtime engine.
\<close>
--- a/src/Doc/Corec/Corec.thy Thu Aug 11 18:26:16 2016 +0200
+++ b/src/Doc/Corec/Corec.thy Thu Aug 11 18:26:44 2016 +0200
@@ -127,7 +127,7 @@
text \<open>
The package is illustrated through concrete examples featuring different flavors
of corecursion. More examples can be found in the directory
-@{file "~~/src/HOL/Corec_Examples"}.
+@{dir "~~/src/HOL/Corec_Examples"}.
\<close>
--- a/src/Doc/Datatypes/Datatypes.thy Thu Aug 11 18:26:16 2016 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy Thu Aug 11 18:26:44 2016 +0200
@@ -163,7 +163,7 @@
text \<open>
Datatypes are illustrated through concrete examples featuring different flavors
of recursion. More examples can be found in the directory
-@{file "~~/src/HOL/Datatype_Examples"}.
+@{dir "~~/src/HOL/Datatype_Examples"}.
\<close>
@@ -1247,7 +1247,7 @@
text \<open>
Primitive recursion is illustrated through concrete examples based on the
datatypes defined in Section~\ref{ssec:datatype-introductory-examples}. More
-examples can be found in the directory @{file "~~/src/HOL/Datatype_Examples"}.
+examples can be found in the directory @{dir "~~/src/HOL/Datatype_Examples"}.
\<close>
@@ -1760,7 +1760,7 @@
Codatatypes can be specified using the @{command codatatype} command. The
command is first illustrated through concrete examples featuring different
flavors of corecursion. More examples can be found in the directory
-@{file "~~/src/HOL/Datatype_Examples"}. The \emph{Archive of Formal Proofs} also
+@{dir "~~/src/HOL/Datatype_Examples"}. The \emph{Archive of Formal Proofs} also
includes some useful codatatypes, notably for lazy lists @{cite
"lochbihler-2010"}.
\<close>
@@ -2038,7 +2038,7 @@
on @{command primcorec} and @{command primcorecursive}; \keyw{corec} and
\keyw{corecursive} are described in a separate tutorial
@{cite "isabelle-corec"}. More examples can be found in the directories
-@{file "~~/src/HOL/Datatype_Examples"} and @{file "~~/src/HOL/Corec_Examples"}.
+@{dir "~~/src/HOL/Datatype_Examples"} and @{dir "~~/src/HOL/Corec_Examples"}.
Whereas recursive functions consume datatypes one constructor at a time,
corecursive functions construct codatatypes one constructor at a time.
@@ -2082,7 +2082,7 @@
text \<open>
Primitive corecursion is illustrated through concrete examples based on the
codatatypes defined in Section~\ref{ssec:codatatype-introductory-examples}. More
-examples can be found in the directory @{file "~~/src/HOL/Datatype_Examples"}.
+examples can be found in the directory @{dir "~~/src/HOL/Datatype_Examples"}.
The code view is favored in the examples below. Sections
\ref{ssec:primrec-constructor-view} and \ref{ssec:primrec-destructor-view}
present the same examples expressed using the constructor and destructor views.
--- a/src/Doc/Isar_Ref/Document_Preparation.thy Thu Aug 11 18:26:16 2016 +0200
+++ b/src/Doc/Isar_Ref/Document_Preparation.thy Thu Aug 11 18:26:44 2016 +0200
@@ -195,8 +195,9 @@
@@{antiquotation emph} options @{syntax text} |
@@{antiquotation bold} options @{syntax text} |
@@{antiquotation verbatim} options @{syntax text} |
+ @@{antiquotation path} options @{syntax name} |
@@{antiquotation "file"} options @{syntax name} |
- @@{antiquotation file_unchecked} options @{syntax name} |
+ @@{antiquotation dir} options @{syntax name} |
@@{antiquotation url} options @{syntax embedded} |
@@{antiquotation cite} options @{syntax cartouche}? (@{syntax name} + @'and')
;
@@ -283,11 +284,13 @@
\<^descr> \<open>@{verbatim s}\<close> prints uninterpreted source text literally as ASCII
characters, using some type-writer font style.
- \<^descr> \<open>@{file path}\<close> checks that \<open>path\<close> refers to a file (or directory) and
- prints it verbatim.
+ \<^descr> \<open>@{path name}\<close> prints the file-system path name verbatim.
- \<^descr> \<open>@{file_unchecked path}\<close> is like \<open>@{file path}\<close>, but does not check the
- existence of the \<open>path\<close> within the file-system.
+ \<^descr> \<open>@{file name}\<close> is like \<open>@{path name}\<close>, but ensures that \<open>name\<close> refers to a
+ plain file.
+
+ \<^descr> \<open>@{dir name}\<close> is like \<open>@{path name}\<close>, but ensures that \<open>name\<close> refers to a
+ directory.
\<^descr> \<open>@{url name}\<close> produces markup for the given URL, which results in an
active hyperlink within the text.
--- a/src/Doc/Isar_Ref/Framework.thy Thu Aug 11 18:26:16 2016 +0200
+++ b/src/Doc/Isar_Ref/Framework.thy Thu Aug 11 18:26:44 2016 +0200
@@ -89,7 +89,7 @@
\<^medskip>
Concrete applications require another intermediate layer: an object-logic.
Isabelle/HOL @{cite "isa-tutorial"} (simply-typed set-theory) is most
- commonly used; elementary examples are given in the directory @{file
+ commonly used; elementary examples are given in the directory @{dir
"~~/src/HOL/Isar_Examples"}. Some examples demonstrate how to start a fresh
object-logic from Isabelle/Pure, and use Isar proofs from the very start,
despite the lack of advanced proof tools at such an early stage (e.g.\ see
@@ -524,7 +524,7 @@
may be populated later. The command \<^theory_text>\<open>method_setup\<close> allows to define proof
methods semantically in Isabelle/ML. The Eisbach language allows to define
proof methods symbolically, as recursive expressions over existing methods
- @{cite "Matichuk-et-al:2014"}; see also @{file "~~/src/HOL/Eisbach"}.
+ @{cite "Matichuk-et-al:2014"}; see also @{dir "~~/src/HOL/Eisbach"}.
Methods use the facts indicated by \<^theory_text>\<open>then\<close> or \<^theory_text>\<open>using\<close>, and then operate on
the goal state. Some basic methods are predefined in Pure: ``@{method "-"}''
--- a/src/Doc/Isar_Ref/HOL_Specific.thy Thu Aug 11 18:26:16 2016 +0200
+++ b/src/Doc/Isar_Ref/HOL_Specific.thy Thu Aug 11 18:26:44 2016 +0200
@@ -2088,7 +2088,7 @@
\<^descr> @{method (HOL) metis} combines ordered resolution and ordered
paramodulation to find first-order (or mildly higher-order) proofs. The
first optional argument specifies a type encoding; see the Sledgehammer
- manual @{cite "isabelle-sledgehammer"} for details. The directory @{file
+ manual @{cite "isabelle-sledgehammer"} for details. The directory @{dir
"~~/src/HOL/Metis_Examples"} contains several small theories developed to a
large extent using @{method (HOL) metis}.
\<close>
--- a/src/Doc/JEdit/JEdit.thy Thu Aug 11 18:26:16 2016 +0200
+++ b/src/Doc/JEdit/JEdit.thy Thu Aug 11 18:26:44 2016 +0200
@@ -166,12 +166,12 @@
Regular jEdit options are accessible via the dialogs \<^emph>\<open>Utilities~/ Global
Options\<close> or \<^emph>\<open>Plugins~/ Plugin Options\<close>, with a second chance to flip the
- two within the central options dialog. Changes are stored in
- @{file_unchecked "$ISABELLE_HOME_USER/jedit/properties"} and
- @{file_unchecked "$ISABELLE_HOME_USER/jedit/keymaps"}.
+ two within the central options dialog. Changes are stored in @{path
+ "$ISABELLE_HOME_USER/jedit/properties"} and @{path
+ "$ISABELLE_HOME_USER/jedit/keymaps"}.
Isabelle system options are managed by Isabelle/Scala and changes are stored
- in @{file_unchecked "$ISABELLE_HOME_USER/etc/preferences"}, independently of
+ in @{path "$ISABELLE_HOME_USER/etc/preferences"}, independently of
other jEdit properties. See also @{cite "isabelle-system"}, especially the
coverage of sessions and command-line tools like @{tool build} or @{tool
options}.
@@ -193,8 +193,8 @@
\<^medskip>
Options are usually loaded on startup and saved on shutdown of
- Isabelle/jEdit. Editing the machine-generated @{file_unchecked
- "$ISABELLE_HOME_USER/jedit/properties"} or @{file_unchecked
+ Isabelle/jEdit. Editing the machine-generated @{path
+ "$ISABELLE_HOME_USER/jedit/properties"} or @{path
"$ISABELLE_HOME_USER/etc/preferences"} manually while the application is
running is likely to cause surprise due to lost update!
\<close>
@@ -213,9 +213,8 @@
Isabelle/jEdit due to various fine-tuning of global defaults, with
additional keyboard shortcuts for Isabelle-specific functionality. Users may
change their keymap later, but need to copy some keyboard shortcuts manually
- (see also @{file_unchecked "$ISABELLE_HOME_USER/jedit/keymaps"} versus
- \<^verbatim>\<open>shortcut\<close> properties in @{file
- "$ISABELLE_HOME/src/Tools/jEdit/src/jEdit.props"}).
+ (see also @{path "$ISABELLE_HOME_USER/jedit/keymaps"} versus \<^verbatim>\<open>shortcut\<close>
+ properties in @{file "$ISABELLE_HOME/src/Tools/jEdit/src/jEdit.props"}).
\<close>
@@ -470,7 +469,7 @@
physically via Unicode glyphs, in order to show ``\<^verbatim>\<open>\<alpha>\<close>'' as ``\<open>\<alpha>\<close>'', for
example. This symbol interpretation is specified by the Isabelle system
distribution in @{file "$ISABELLE_HOME/etc/symbols"} and may be augmented by
- the user in @{file_unchecked "$ISABELLE_HOME_USER/etc/symbols"}.
+ the user in @{path "$ISABELLE_HOME_USER/etc/symbols"}.
The appendix of @{cite "isabelle-isar-ref"} gives an overview of the
standard interpretation of finitely many symbols from the infinite
@@ -660,9 +659,9 @@
platforms. Isabelle/ML on Windows uses Unix-style path notation, too, and
driver letter representation as in Cygwin (e.g.\ \<^verbatim>\<open>/cygdrive/c\<close>). Moreover,
environment variables from the Isabelle process may be used freely, e.g.\
- @{file "$ISABELLE_HOME/etc/symbols"} or @{file_unchecked
- "$POLYML_HOME/README"}. There are special shortcuts: @{file "~"} for @{file
- "$USER_HOME"} and @{file "~~"} for @{file "$ISABELLE_HOME"}.
+ @{file "$ISABELLE_HOME/etc/symbols"} or @{file "$POLYML_HOME/README"}. There
+ are special shortcuts: @{dir "~"} for @{dir "$USER_HOME"} and @{dir "~~"}
+ for @{dir "$ISABELLE_HOME"}.
\<^medskip>
Since jEdit happens to support environment variables within file
@@ -1242,7 +1241,7 @@
text \<open>
The completion tables for Isabelle symbols (\secref{sec:symbols}) are
determined statically from @{file "$ISABELLE_HOME/etc/symbols"} and
- @{file_unchecked "$ISABELLE_HOME_USER/etc/symbols"} for each symbol
+ @{path "$ISABELLE_HOME_USER/etc/symbols"} for each symbol
specification as follows:
\<^medskip>
@@ -1274,12 +1273,12 @@
\<^medskip>
Additional abbreviations may be specified in @{file
- "$ISABELLE_HOME/etc/abbrevs"} and @{file_unchecked
- "$ISABELLE_HOME_USER/etc/abbrevs"}. The file content follows general Isar
- outer syntax @{cite "isabelle-isar-ref"}. Abbreviations are specified as
+ "$ISABELLE_HOME/etc/abbrevs"} and @{path "$ISABELLE_HOME_USER/etc/abbrevs"}.
+ The file content follows general Isar outer syntax @{cite
+ "isabelle-isar-ref"}. Abbreviations are specified as
``\<open>abbrev\<close>~\<^verbatim>\<open>=\<close>~\<open>text\<close>'' pairs. The replacement \<open>text\<close> may consist of more
than just one symbol; otherwise the meaning is the same as a symbol
- specification ``\<open>sym\<close>~\<^verbatim>\<open>abbrev:\<close>~\<open>abbrev\<close>'' within @{file_unchecked
+ specification ``\<open>sym\<close>~\<^verbatim>\<open>abbrev:\<close>~\<open>abbrev\<close>'' within @{path
"etc/symbols"}.
\<close>
@@ -1544,7 +1543,7 @@
dictionary, taken from the colon-separated list in the settings variable
@{setting_def JORTHO_DICTIONARIES}. There are jEdit actions to specify local
updates to a dictionary, by including or excluding words. The result of
- permanent dictionary updates is stored in the directory @{file_unchecked
+ permanent dictionary updates is stored in the directory @{path
"$ISABELLE_HOME_USER/dictionaries"}, in a separate file for each dictionary.
\<^item> @{system_option_def spell_checker_elements} specifies a comma-separated
@@ -2003,7 +2002,7 @@
\<^bold>\<open>Workaround:\<close> Install \<^verbatim>\<open>IsabelleText\<close> and \<^verbatim>\<open>IsabelleTextBold\<close> on the system
with \<^emph>\<open>Font Book\<close>, despite the warnings in \secref{sec:symbols} against
- that! The \<^verbatim>\<open>.ttf\<close> font files reside in some directory @{file_unchecked
+ that! The \<^verbatim>\<open>.ttf\<close> font files reside in some directory @{path
"$ISABELLE_HOME/contrib/isabelle_fonts-XYZ"}.
\<^item> \<^bold>\<open>Problem:\<close> Some Linux/X11 input methods such as IBus tend to disrupt key
--- a/src/Doc/System/Environment.thy Thu Aug 11 18:26:16 2016 +0200
+++ b/src/Doc/System/Environment.thy Thu Aug 11 18:26:44 2016 +0200
@@ -44,7 +44,7 @@
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} tool. Symbolic links are admissible, but a
- plain copy of the @{file "$ISABELLE_HOME/bin"} files will not work!
+ plain copy of the @{dir "$ISABELLE_HOME/bin"} files will not work!
\<^enum> The file @{file "$ISABELLE_HOME/etc/settings"} is run as a
@{executable_ref bash} shell script with the auto-export option for
@@ -56,7 +56,7 @@
variables. When installing the system, only a few of these may have to be
adapted (probably @{setting ML_SYSTEM} etc.).
- \<^enum> The file @{file_unchecked "$ISABELLE_HOME_USER/etc/settings"} (if it
+ \<^enum> The file @{path "$ISABELLE_HOME_USER/etc/settings"} (if it
exists) is run in the same way as the site default settings. Note that the
variable @{setting ISABELLE_HOME_USER} has already been set before ---
usually to something like \<^verbatim>\<open>$USER_HOME/.isabelle/IsabelleXXXX\<close>.
@@ -101,8 +101,8 @@
On Unix systems this is usually the same as @{setting HOME}, but on Windows
it is the regular home directory of the user, not the one of within the
Cygwin root file-system.\<^footnote>\<open>Cygwin itself offers another choice whether its
- HOME should point to the @{file_unchecked "/home"} directory tree or the
- Windows user home.\<close>
+ HOME should point to the @{path "/home"} directory tree or the Windows user
+ home.\<close>
\<^descr>[@{setting_def ISABELLE_HOME}\<open>\<^sup>*\<close>] is the location of the top-level
Isabelle distribution directory. This is automatically determined from the
@@ -110,7 +110,7 @@
ISABELLE_HOME} yourself from the shell!
\<^descr>[@{setting_def ISABELLE_HOME_USER}] is the user-specific counterpart of
- @{setting ISABELLE_HOME}. The default value is relative to @{file_unchecked
+ @{setting ISABELLE_HOME}. The default value is relative to @{path
"$USER_HOME/.isabelle"}, under rare circumstances this may be changed in the
global setting file. Typically, the @{setting ISABELLE_HOME_USER} directory
mimics @{setting ISABELLE_HOME} to some extend. In particular, site-wide
@@ -138,7 +138,7 @@
\<^descr>[@{setting ISABELLE_TOOL}\<open>\<^sup>*\<close>] is automatically set to the full path name
of the @{executable isabelle} executable. Thus other tools and scripts need
- not assume that the @{file "$ISABELLE_HOME/bin"} directory is on the current
+ not assume that the @{dir "$ISABELLE_HOME/bin"} directory is on the current
search path of the shell.
\<^descr>[@{setting_def ISABELLE_IDENTIFIER}\<open>\<^sup>*\<close>] refers to the name of this
@@ -175,7 +175,7 @@
\<^descr>[@{setting_def ISABELLE_BROWSER_INFO}] is the directory where theory
browser information is stored as HTML and PDF (see also \secref{sec:info}).
- The default value is @{file_unchecked "$ISABELLE_HOME_USER/browser_info"}.
+ The default value is @{path "$ISABELLE_HOME_USER/browser_info"}.
\<^descr>[@{setting_def ISABELLE_LOGIC}] specifies the default logic to load if none
is given explicitely by the user. The default value is \<^verbatim>\<open>HOL\<close>.
@@ -234,12 +234,12 @@
The root of component initialization is @{setting ISABELLE_HOME} itself.
After initializing all of its sub-components recursively, @{setting
ISABELLE_HOME_USER} is included in the same manner (if that directory
- exists). This allows to install private components via @{file_unchecked
+ exists). This allows to install private components via @{path
"$ISABELLE_HOME_USER/etc/components"}, although it is often more convenient
to do that programmatically via the \<^verbatim>\<open>init_component\<close> shell function in the
\<^verbatim>\<open>etc/settings\<close> script of \<^verbatim>\<open>$ISABELLE_HOME_USER\<close> (or any other component
- directory). For example:
- @{verbatim [display] \<open>init_component "$HOME/screwdriver-2.0"\<close>}
+ directory). For example: @{verbatim [display] \<open>init_component
+ "$HOME/screwdriver-2.0"\<close>}
This is tolerant wrt.\ missing component directories, but might produce a
warning.
--- a/src/Doc/System/Presentation.thy Thu Aug 11 18:26:16 2016 +0200
+++ b/src/Doc/System/Presentation.thy Thu Aug 11 18:26:44 2016 +0200
@@ -69,7 +69,7 @@
The presentation output will appear in \<^verbatim>\<open>$ISABELLE_BROWSER_INFO/FOL/FOL\<close> as
reported by the above verbose invocation of the build process.
- Many Isabelle sessions (such as \<^verbatim>\<open>HOL-Library\<close> in @{file
+ Many Isabelle sessions (such as \<^verbatim>\<open>HOL-Library\<close> in @{dir
"~~/src/HOL/Library"}) also provide printable documents in PDF. These are
prepared automatically as well if enabled like this:
@{verbatim [display] \<open>isabelle build -o browser_info -o document=pdf -v -c HOL-Library\<close>}
--- a/src/Doc/System/Sessions.thy Thu Aug 11 18:26:16 2016 +0200
+++ b/src/Doc/System/Sessions.thy Thu Aug 11 18:26:44 2016 +0200
@@ -344,9 +344,9 @@
\<^medskip>
Option \<^verbatim>\<open>-s\<close> enables \<^emph>\<open>system mode\<close>, which means that resulting heap images
- and log files are stored in @{file_unchecked "$ISABELLE_HOME/heaps"} instead
- of the default location @{setting ISABELLE_OUTPUT} (which is normally in
- @{setting ISABELLE_HOME_USER}, i.e.\ the user's home directory).
+ and log files are stored in @{path "$ISABELLE_HOME/heaps"} instead of the
+ default location @{setting ISABELLE_OUTPUT} (which is normally in @{setting
+ ISABELLE_HOME_USER}, i.e.\ the user's home directory).
\<^medskip>
Option \<^verbatim>\<open>-v\<close> increases the general level of verbosity. Option \<^verbatim>\<open>-l\<close> lists
--- a/src/HOL/Isar_Examples/Hoare.thy Thu Aug 11 18:26:16 2016 +0200
+++ b/src/HOL/Isar_Examples/Hoare.thy Thu Aug 11 18:26:44 2016 +0200
@@ -16,7 +16,7 @@
The following abstract syntax and semantics of Hoare Logic over \<^verbatim>\<open>WHILE\<close>
programs closely follows the existing tradition in Isabelle/HOL of
formalizing the presentation given in @{cite \<open>\S6\<close> "Winskel:1993"}. See also
- @{file "~~/src/HOL/Hoare"} and @{cite "Nipkow:1998:Winskel"}.
+ @{dir "~~/src/HOL/Hoare"} and @{cite "Nipkow:1998:Winskel"}.
\<close>
type_synonym 'a bexp = "'a set"
@@ -358,7 +358,7 @@
text \<open>
We now load the \<^emph>\<open>original\<close> ML file for proof scripts and tactic definition
- for the Hoare Verification Condition Generator (see @{file
+ for the Hoare Verification Condition Generator (see @{dir
"~~/src/HOL/Hoare/"}). As far as we are concerned here, the result is a
proof method \<open>hoare\<close>, which may be applied to a Hoare Logic assertion to
extract purely logical verification conditions. It is important to note that
--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML Thu Aug 11 18:26:16 2016 +0200
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML Thu Aug 11 18:26:44 2016 +0200
@@ -199,10 +199,10 @@
(** invocation of Haskell interpreter **)
val narrowing_engine =
- File.read @{path "~~/src/HOL/Tools/Quickcheck/Narrowing_Engine.hs"}
+ File.read @{"file" "~~/src/HOL/Tools/Quickcheck/Narrowing_Engine.hs"}
val pnf_narrowing_engine =
- File.read @{path "~~/src/HOL/Tools/Quickcheck/PNF_Narrowing_Engine.hs"}
+ File.read @{"file" "~~/src/HOL/Tools/Quickcheck/PNF_Narrowing_Engine.hs"}
fun exec verbose code =
ML_Context.exec (fn () =>
--- a/src/Pure/PIDE/resources.ML Thu Aug 11 18:26:16 2016 +0200
+++ b/src/Pure/PIDE/resources.ML Thu Aug 11 18:26:44 2016 +0200
@@ -184,33 +184,25 @@
local
-fun check_path strict ctxt dir (name, pos) =
+fun err msg pos = error (msg ^ Position.here pos);
+
+fun check_path ctxt dir (name, pos) =
let
val _ = Context_Position.report ctxt pos Markup.language_path;
- val path = Path.append dir (Path.explode name)
- handle ERROR msg => error (msg ^ Position.here pos);
-
+ val path = Path.append dir (Path.explode name) handle ERROR msg => err msg pos;
+ val _ = Path.expand path handle ERROR msg => err msg pos;
val _ = Context_Position.report ctxt pos (Markup.path (Path.smart_implode path));
- val _ =
- if can Path.expand path andalso File.exists path then ()
- else
- let
- val path' = perhaps (try Path.expand) path;
- val msg = "Bad file: " ^ Path.print path' ^ Position.here pos;
- in
- if strict then error msg
- else if Context_Position.is_visible ctxt then
- Output.report
- [Markup.markup (Markup.bad |> Markup.properties (Position.properties_of pos)) msg]
- else ()
- end;
in path end;
-fun file_antiq strict ctxt (name, pos) =
+fun path_antiq check_file ctxt (name, pos) =
let
val dir = master_directory (Proof_Context.theory_of ctxt);
- val _ = check_path strict ctxt dir (name, pos);
+ val path = check_path ctxt dir (name, pos);
+ val _ =
+ (case check_file of
+ NONE => path
+ | SOME check => (check path handle ERROR msg => err msg pos));
in
space_explode "/" name
|> map Latex.output_ascii
@@ -221,13 +213,15 @@
in
val _ = Theory.setup
- (Thy_Output.antiquotation @{binding file} (Scan.lift (Parse.position Parse.path))
- (file_antiq true o #context) #>
- Thy_Output.antiquotation @{binding file_unchecked} (Scan.lift (Parse.position Parse.path))
- (file_antiq false o #context) #>
- ML_Antiquotation.value @{binding path}
+ (Thy_Output.antiquotation @{binding path} (Scan.lift (Parse.position Parse.path))
+ (path_antiq NONE o #context) #>
+ Thy_Output.antiquotation @{binding file} (Scan.lift (Parse.position Parse.path))
+ (path_antiq (SOME File.check_file) o #context) #>
+ Thy_Output.antiquotation @{binding dir} (Scan.lift (Parse.position Parse.path))
+ (path_antiq (SOME File.check_dir) o #context) #>
+ ML_Antiquotation.value @{binding file}
(Args.context -- Scan.lift (Parse.position Parse.path) >> (fn (ctxt, arg) =>
- let val path = check_path true ctxt Path.current arg
+ let val path = check_path ctxt Path.current arg |> File.check_file
in "Path.explode " ^ ML_Syntax.print_string (Path.implode path) end)));
end;
--- a/src/Pure/Tools/jedit.ML Thu Aug 11 18:26:16 2016 +0200
+++ b/src/Pure/Tools/jedit.ML Thu Aug 11 18:26:44 2016 +0200
@@ -24,13 +24,13 @@
val isabelle_jedit_actions =
Lazy.lazy (fn () =>
- (case XML.parse (File.read @{path "~~/src/Tools/jEdit/src/actions.xml"}) of
+ (case XML.parse (File.read @{file "~~/src/Tools/jEdit/src/actions.xml"}) of
XML.Elem (("ACTIONS", _), body) => maps (parse_named "ACTION") body
| _ => []));
val isabelle_jedit_dockables =
Lazy.lazy (fn () =>
- (case XML.parse (File.read @{path "~~/src/Tools/jEdit/src/dockables.xml"}) of
+ (case XML.parse (File.read @{file "~~/src/Tools/jEdit/src/dockables.xml"}) of
XML.Elem (("DOCKABLES", _), body) => maps (parse_named "DOCKABLE") body
| _ => []));