--- 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 ***
--- 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>
--- 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>