--- a/NEWS Mon Dec 09 12:27:18 2013 +0100
+++ b/NEWS Mon Dec 09 20:16:12 2013 +0100
@@ -9,6 +9,9 @@
* Document antiquotation @{url} produces markup for the given URL,
which results in an active hyperlink within the text.
+* Document antiquotation @{file_unchecked} is like @{file}, but does
+not check existence within the file-system.
+
*** Prover IDE -- Isabelle/Scala/jEdit ***
--- a/src/Doc/IsarRef/Document_Preparation.thy Mon Dec 09 12:27:18 2013 +0100
+++ b/src/Doc/IsarRef/Document_Preparation.thy Mon Dec 09 20:16:12 2013 +0100
@@ -177,6 +177,7 @@
@@{antiquotation ML_type} options @{syntax name} |
@@{antiquotation ML_struct} options @{syntax name} |
@@{antiquotation \"file\"} options @{syntax name} |
+ @@{antiquotation file_unchecked} options @{syntax name} |
@@{antiquotation url} options @{syntax name}
;
options: '[' (option * ',') ']'
@@ -269,6 +270,10 @@
\item @{text "@{file path}"} checks that @{text "path"} refers to a
file (or directory) and prints it verbatim.
+ \item @{text "@{file_unchecked path}"} is like @{text "@{file
+ path}"}, but does not check the existence of the @{text "path"}
+ within the file-system.
+
\item @{text "@{url name}"} produces markup for the given URL, which
results in an active hyperlink within the text.
--- a/src/Doc/System/Basics.thy Mon Dec 09 12:27:18 2013 +0100
+++ b/src/Doc/System/Basics.thy Mon Dec 09 20:16:12 2013 +0100
@@ -95,7 +95,7 @@
of these may have to be adapted (probably @{setting ML_SYSTEM}
etc.).
- \item The file @{verbatim "$ISABELLE_HOME_USER/etc/settings"} (if it
+ \item The file @{file_unchecked "$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
@@ -166,7 +166,7 @@
\item[@{setting_def ISABELLE_HOME_USER}] is the user-specific
counterpart of @{setting ISABELLE_HOME}. The default value is
- relative to @{verbatim "$USER_HOME/.isabelle"}, under rare
+ relative to @{file_unchecked "$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
@@ -247,7 +247,7 @@
\item[@{setting_def ISABELLE_BROWSER_INFO}] is the directory where
theory browser information (HTML text, graph data, and printable
documents) is stored (see also \secref{sec:info}). The default
- value is @{verbatim "$ISABELLE_HOME_USER/browser_info"}.
+ value is @{file_unchecked "$ISABELLE_HOME_USER/browser_info"}.
\item[@{setting_def ISABELLE_LOGIC}] specifies the default logic to
load if none is given explicitely by the user. The default value is
@@ -277,7 +277,7 @@
\item[@{setting_def ISABELLE_TMP_PREFIX}@{text "\<^sup>*"}] is the
prefix from which any running @{executable "isabelle-process"}
derives an individual directory for temporary files. The default is
- somewhere in @{verbatim "/tmp"}.
+ somewhere in @{file_unchecked "/tmp"}.
\end{description}
*}
@@ -325,7 +325,7 @@
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 @{verbatim "$ISABELLE_HOME_USER/etc/components"}, although it is
+ via @{file_unchecked "$ISABELLE_HOME_USER/etc/components"}, although it is
often more convenient to do that programmatically via the
\verb,init_component, shell function in the \verb,etc/settings,
script of \verb,$ISABELLE_HOME_USER, (or any other component
--- a/src/Doc/System/Sessions.thy Mon Dec 09 12:27:18 2013 +0100
+++ b/src/Doc/System/Sessions.thy Mon Dec 09 20:16:12 2013 +0100
@@ -356,7 +356,7 @@
\medskip Option @{verbatim "-s"} enables \emph{system mode}, which
means that resulting heap images and log files are stored in
- @{verbatim "$ISABELLE_HOME/heaps"} instead of the default location
+ @{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).
--- a/src/Doc/antiquote_setup.ML Mon Dec 09 12:27:18 2013 +0100
+++ b/src/Doc/antiquote_setup.ML Mon Dec 09 20:16:12 2013 +0100
@@ -47,22 +47,6 @@
(K (split_lines #> map verbatim #> space_implode "\\isasep\\isanewline%\n"));
-(* unchecked file *)
-
-val file_unchecked_setup =
- Thy_Output.antiquotation @{binding file_unchecked} (Scan.lift (Parse.position Parse.path))
- (fn {context = ctxt, ...} => fn (name, pos) =>
- let
- val dir = Thy_Load.master_directory (Proof_Context.theory_of ctxt);
- val path = Path.append dir (Path.explode name);
- val _ = Position.report pos (Markup.path name);
- in
- space_explode "/" name
- |> map Thy_Output.verb_text
- |> space_implode (Thy_Output.verb_text "/" ^ "\\discretionary{}{}{}")
- end);
-
-
(* ML text *)
local
@@ -249,7 +233,6 @@
val setup =
verbatim_setup #>
- file_unchecked_setup #>
index_ml_setup #>
named_thms_setup #>
thy_file_setup #>
--- a/src/Pure/Thy/thy_load.ML Mon Dec 09 12:27:18 2013 +0100
+++ b/src/Pure/Thy/thy_load.ML Mon Dec 09 20:16:12 2013 +0100
@@ -192,20 +192,24 @@
(* document antiquotation *)
+fun file_antiq do_check ctxt (name, pos) =
+ let
+ val dir = master_directory (Proof_Context.theory_of ctxt);
+ val path = Path.append dir (Path.explode name);
+ val _ =
+ if not do_check orelse File.exists path then ()
+ else error ("Bad file: " ^ Path.print (Path.expand path) ^ Position.here pos);
+ val _ = Position.report pos (Markup.path name);
+ in
+ space_explode "/" name
+ |> map Thy_Output.verb_text
+ |> space_implode (Thy_Output.verb_text "/" ^ "\\discretionary{}{}{}")
+ end;
+
val _ = Theory.setup
(Thy_Output.antiquotation (Binding.name "file") (Scan.lift (Parse.position Parse.path))
- (fn {context = ctxt, ...} => fn (name, pos) =>
- let
- val dir = master_directory (Proof_Context.theory_of ctxt);
- val path = Path.append dir (Path.explode name);
- val _ =
- if File.exists path then ()
- else error ("Bad file: " ^ Path.print (Path.expand path) ^ Position.here pos);
- val _ = Position.report pos (Markup.path name);
- in
- space_explode "/" name
- |> map Thy_Output.verb_text
- |> space_implode (Thy_Output.verb_text "/" ^ "\\discretionary{}{}{}")
- end));
+ (file_antiq true o #context) #>
+ (Thy_Output.antiquotation (Binding.name "file_unchecked") (Scan.lift (Parse.position Parse.path))
+ (file_antiq false o #context)));
end;