# HG changeset patch
# User wenzelm
# Date 1386616572 -3600
# Node ID 0dff3326d12a7824860e680079850b6bd64d34db
# Parent  ea71549629e21c1e0446d3ce93083f224ee2af76
provide @{file_unchecked} in Isabelle/Pure;

diff -r ea71549629e2 -r 0dff3326d12a NEWS
--- 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 ***
 
diff -r ea71549629e2 -r 0dff3326d12a src/Doc/IsarRef/Document_Preparation.thy
--- 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.
 
diff -r ea71549629e2 -r 0dff3326d12a src/Doc/System/Basics.thy
--- 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
diff -r ea71549629e2 -r 0dff3326d12a src/Doc/System/Sessions.thy
--- 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).
 
diff -r ea71549629e2 -r 0dff3326d12a src/Doc/antiquote_setup.ML
--- 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 #>
diff -r ea71549629e2 -r 0dff3326d12a src/Pure/Thy/thy_load.ML
--- 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;