# HG changeset patch
# User wenzelm
# Date 1506965298 -7200
# Node ID e32750d7acb42091326c063b2e0337edc4e1c59f
# Parent  a1b2ea991ad18999e3b2ca641b031afbb27b6ba1
added command 'external_file';

diff -r a1b2ea991ad1 -r e32750d7acb4 NEWS
--- a/NEWS	Mon Oct 02 18:35:51 2017 +0200
+++ b/NEWS	Mon Oct 02 19:28:18 2017 +0200
@@ -14,6 +14,10 @@
 INCOMPATIBILITY for old developments that have not been updated to
 Isabelle2017 yet (using the "isabelle imports" tool).
 
+* Command 'external_file' declares the formal dependency on the given
+file name, such that the Isabelle build process knows about it, but
+without specific Prover IDE management.
+
 
 *** HOL ***
 
diff -r a1b2ea991ad1 -r e32750d7acb4 src/Doc/Isar_Ref/Spec.thy
--- a/src/Doc/Isar_Ref/Spec.thy	Mon Oct 02 18:35:51 2017 +0200
+++ b/src/Doc/Isar_Ref/Spec.thy	Mon Oct 02 19:28:18 2017 +0200
@@ -1177,6 +1177,23 @@
 \<close>
 
 
+section \<open>External file dependencies\<close>
+
+text \<open>
+  \begin{matharray}{rcl}
+    @{command_def "external_file"} & : & \<open>any \<rightarrow> any\<close> \\
+  \end{matharray}
+
+  @{rail \<open>@@{command external_file} @{syntax name} ';'?\<close>}
+
+  \<^descr> \<^theory_text>\<open>external_file name\<close> declares the formal dependency on the given file
+  name, such that the Isabelle build process knows about it (see also @{cite
+  "isabelle-system"}). The file can be read e.g.\ in Isabelle/ML via @{ML
+  File.read}, without specific management by the Prover IDE.
+\<close>
+
+
+
 section \<open>Primitive specification elements\<close>
 
 subsection \<open>Sorts\<close>
diff -r a1b2ea991ad1 -r e32750d7acb4 src/Pure/Pure.thy
--- a/src/Pure/Pure.thy	Mon Oct 02 18:35:51 2017 +0200
+++ b/src/Pure/Pure.thy	Mon Oct 02 19:28:18 2017 +0200
@@ -20,6 +20,7 @@
     "definition" "abbreviation" "type_notation" "no_type_notation" "notation"
     "no_notation" "axiomatization" "alias" "type_alias" "lemmas" "declare"
     "hide_class" "hide_type" "hide_const" "hide_fact" :: thy_decl
+  and "external_file" :: thy_load
   and "ML_file" "ML_file_debug" "ML_file_no_debug" :: thy_load % "ML"
   and "SML_file" "SML_file_debug" "SML_file_no_debug" :: thy_load % "ML"
   and "SML_import" "SML_export" :: thy_decl % "ML"
@@ -107,6 +108,20 @@
 
 section \<open>Isar commands\<close>
 
+subsection \<open>External file dependencies\<close>
+
+ML \<open>
+  Outer_Syntax.command @{command_keyword external_file} "formal dependency on external file"
+    (Parse.position Parse.path >> (fn (s, pos) => Toplevel.keep (fn st =>
+      let
+        val ctxt = Toplevel.context_of st;
+        val _ = Context_Position.report ctxt pos Markup.language_path;
+        val path = Path.explode s;
+        val _ = Context_Position.report ctxt pos (Markup.path (Path.smart_implode path));
+      in () end)));
+\<close>
+
+
 subsection \<open>Embedded ML text\<close>
 
 ML \<open>