provide @{file_unchecked} in Isabelle/Pure;
authorwenzelm
Mon Dec 09 20:16:12 2013 +0100 (2013-12-09 ago)
changeset 547050dff3326d12a
parent 54704 ea71549629e2
child 54706 d3c656f0b7ab
provide @{file_unchecked} in Isabelle/Pure;
NEWS
src/Doc/IsarRef/Document_Preparation.thy
src/Doc/System/Basics.thy
src/Doc/System/Sessions.thy
src/Doc/antiquote_setup.ML
src/Pure/Thy/thy_load.ML
     1.1 --- a/NEWS	Mon Dec 09 12:27:18 2013 +0100
     1.2 +++ b/NEWS	Mon Dec 09 20:16:12 2013 +0100
     1.3 @@ -9,6 +9,9 @@
     1.4  * Document antiquotation @{url} produces markup for the given URL,
     1.5  which results in an active hyperlink within the text.
     1.6  
     1.7 +* Document antiquotation @{file_unchecked} is like @{file}, but does
     1.8 +not check existence within the file-system.
     1.9 +
    1.10  
    1.11  *** Prover IDE -- Isabelle/Scala/jEdit ***
    1.12  
     2.1 --- a/src/Doc/IsarRef/Document_Preparation.thy	Mon Dec 09 12:27:18 2013 +0100
     2.2 +++ b/src/Doc/IsarRef/Document_Preparation.thy	Mon Dec 09 20:16:12 2013 +0100
     2.3 @@ -177,6 +177,7 @@
     2.4        @@{antiquotation ML_type} options @{syntax name} |
     2.5        @@{antiquotation ML_struct} options @{syntax name} |
     2.6        @@{antiquotation \"file\"} options @{syntax name} |
     2.7 +      @@{antiquotation file_unchecked} options @{syntax name} |
     2.8        @@{antiquotation url} options @{syntax name}
     2.9      ;
    2.10      options: '[' (option * ',') ']'
    2.11 @@ -269,6 +270,10 @@
    2.12    \item @{text "@{file path}"} checks that @{text "path"} refers to a
    2.13    file (or directory) and prints it verbatim.
    2.14  
    2.15 +  \item @{text "@{file_unchecked path}"} is like @{text "@{file
    2.16 +  path}"}, but does not check the existence of the @{text "path"}
    2.17 +  within the file-system.
    2.18 +
    2.19    \item @{text "@{url name}"} produces markup for the given URL, which
    2.20    results in an active hyperlink within the text.
    2.21  
     3.1 --- a/src/Doc/System/Basics.thy	Mon Dec 09 12:27:18 2013 +0100
     3.2 +++ b/src/Doc/System/Basics.thy	Mon Dec 09 20:16:12 2013 +0100
     3.3 @@ -95,7 +95,7 @@
     3.4    of these may have to be adapted (probably @{setting ML_SYSTEM}
     3.5    etc.).
     3.6    
     3.7 -  \item The file @{verbatim "$ISABELLE_HOME_USER/etc/settings"} (if it
     3.8 +  \item The file @{file_unchecked "$ISABELLE_HOME_USER/etc/settings"} (if it
     3.9    exists) is run in the same way as the site default settings. Note
    3.10    that the variable @{setting ISABELLE_HOME_USER} has already been set
    3.11    before --- usually to something like @{verbatim
    3.12 @@ -166,7 +166,7 @@
    3.13    
    3.14    \item[@{setting_def ISABELLE_HOME_USER}] is the user-specific
    3.15    counterpart of @{setting ISABELLE_HOME}. The default value is
    3.16 -  relative to @{verbatim "$USER_HOME/.isabelle"}, under rare
    3.17 +  relative to @{file_unchecked "$USER_HOME/.isabelle"}, under rare
    3.18    circumstances this may be changed in the global setting file.
    3.19    Typically, the @{setting ISABELLE_HOME_USER} directory mimics
    3.20    @{setting ISABELLE_HOME} to some extend. In particular, site-wide
    3.21 @@ -247,7 +247,7 @@
    3.22    \item[@{setting_def ISABELLE_BROWSER_INFO}] is the directory where
    3.23    theory browser information (HTML text, graph data, and printable
    3.24    documents) is stored (see also \secref{sec:info}).  The default
    3.25 -  value is @{verbatim "$ISABELLE_HOME_USER/browser_info"}.
    3.26 +  value is @{file_unchecked "$ISABELLE_HOME_USER/browser_info"}.
    3.27    
    3.28    \item[@{setting_def ISABELLE_LOGIC}] specifies the default logic to
    3.29    load if none is given explicitely by the user.  The default value is
    3.30 @@ -277,7 +277,7 @@
    3.31    \item[@{setting_def ISABELLE_TMP_PREFIX}@{text "\<^sup>*"}] is the
    3.32    prefix from which any running @{executable "isabelle-process"}
    3.33    derives an individual directory for temporary files.  The default is
    3.34 -  somewhere in @{verbatim "/tmp"}.
    3.35 +  somewhere in @{file_unchecked "/tmp"}.
    3.36    
    3.37    \end{description}
    3.38  *}
    3.39 @@ -325,7 +325,7 @@
    3.40    itself.  After initializing all of its sub-components recursively,
    3.41    @{setting ISABELLE_HOME_USER} is included in the same manner (if
    3.42    that directory exists).  This allows to install private components
    3.43 -  via @{verbatim "$ISABELLE_HOME_USER/etc/components"}, although it is
    3.44 +  via @{file_unchecked "$ISABELLE_HOME_USER/etc/components"}, although it is
    3.45    often more convenient to do that programmatically via the
    3.46    \verb,init_component, shell function in the \verb,etc/settings,
    3.47    script of \verb,$ISABELLE_HOME_USER, (or any other component
     4.1 --- a/src/Doc/System/Sessions.thy	Mon Dec 09 12:27:18 2013 +0100
     4.2 +++ b/src/Doc/System/Sessions.thy	Mon Dec 09 20:16:12 2013 +0100
     4.3 @@ -356,7 +356,7 @@
     4.4  
     4.5    \medskip Option @{verbatim "-s"} enables \emph{system mode}, which
     4.6    means that resulting heap images and log files are stored in
     4.7 -  @{verbatim "$ISABELLE_HOME/heaps"} instead of the default location
     4.8 +  @{file_unchecked "$ISABELLE_HOME/heaps"} instead of the default location
     4.9    @{setting ISABELLE_OUTPUT} (which is normally in @{setting
    4.10    ISABELLE_HOME_USER}, i.e.\ the user's home directory).
    4.11  
     5.1 --- a/src/Doc/antiquote_setup.ML	Mon Dec 09 12:27:18 2013 +0100
     5.2 +++ b/src/Doc/antiquote_setup.ML	Mon Dec 09 20:16:12 2013 +0100
     5.3 @@ -47,22 +47,6 @@
     5.4      (K (split_lines #> map verbatim #> space_implode "\\isasep\\isanewline%\n"));
     5.5  
     5.6  
     5.7 -(* unchecked file *)
     5.8 -
     5.9 -val file_unchecked_setup =
    5.10 -  Thy_Output.antiquotation @{binding file_unchecked} (Scan.lift (Parse.position Parse.path))
    5.11 -    (fn {context = ctxt, ...} => fn (name, pos) =>
    5.12 -      let
    5.13 -        val dir = Thy_Load.master_directory (Proof_Context.theory_of ctxt);
    5.14 -        val path = Path.append dir (Path.explode name);
    5.15 -        val _ = Position.report pos (Markup.path name);
    5.16 -      in
    5.17 -        space_explode "/" name
    5.18 -        |> map Thy_Output.verb_text
    5.19 -        |> space_implode (Thy_Output.verb_text "/" ^ "\\discretionary{}{}{}")
    5.20 -      end);
    5.21 -
    5.22 -
    5.23  (* ML text *)
    5.24  
    5.25  local
    5.26 @@ -249,7 +233,6 @@
    5.27  
    5.28  val setup =
    5.29    verbatim_setup #>
    5.30 -  file_unchecked_setup #>
    5.31    index_ml_setup #>
    5.32    named_thms_setup #>
    5.33    thy_file_setup #>
     6.1 --- a/src/Pure/Thy/thy_load.ML	Mon Dec 09 12:27:18 2013 +0100
     6.2 +++ b/src/Pure/Thy/thy_load.ML	Mon Dec 09 20:16:12 2013 +0100
     6.3 @@ -192,20 +192,24 @@
     6.4  
     6.5  (* document antiquotation *)
     6.6  
     6.7 +fun file_antiq do_check ctxt (name, pos) =
     6.8 +  let
     6.9 +    val dir = master_directory (Proof_Context.theory_of ctxt);
    6.10 +    val path = Path.append dir (Path.explode name);
    6.11 +    val _ =
    6.12 +      if not do_check orelse File.exists path then ()
    6.13 +      else error ("Bad file: " ^ Path.print (Path.expand path) ^ Position.here pos);
    6.14 +    val _ = Position.report pos (Markup.path name);
    6.15 +  in
    6.16 +    space_explode "/" name
    6.17 +    |> map Thy_Output.verb_text
    6.18 +    |> space_implode (Thy_Output.verb_text "/" ^ "\\discretionary{}{}{}")
    6.19 +  end;
    6.20 +
    6.21  val _ = Theory.setup
    6.22    (Thy_Output.antiquotation (Binding.name "file") (Scan.lift (Parse.position Parse.path))
    6.23 -    (fn {context = ctxt, ...} => fn (name, pos) =>
    6.24 -      let
    6.25 -        val dir = master_directory (Proof_Context.theory_of ctxt);
    6.26 -        val path = Path.append dir (Path.explode name);
    6.27 -        val _ =
    6.28 -          if File.exists path then ()
    6.29 -          else error ("Bad file: " ^ Path.print (Path.expand path) ^ Position.here pos);
    6.30 -        val _ = Position.report pos (Markup.path name);
    6.31 -      in
    6.32 -        space_explode "/" name
    6.33 -        |> map Thy_Output.verb_text
    6.34 -        |> space_implode (Thy_Output.verb_text "/" ^ "\\discretionary{}{}{}")
    6.35 -      end));
    6.36 +    (file_antiq true o #context) #>
    6.37 +  (Thy_Output.antiquotation (Binding.name "file_unchecked") (Scan.lift (Parse.position Parse.path))
    6.38 +    (file_antiq false o #context)));
    6.39  
    6.40  end;