added command 'external_file';
authorwenzelm
Mon Oct 02 19:28:18 2017 +0200 (20 months ago)
changeset 66757e32750d7acb4
parent 66756 a1b2ea991ad1
child 66758 9312ce5a938d
added command 'external_file';
NEWS
src/Doc/Isar_Ref/Spec.thy
src/Pure/Pure.thy
     1.1 --- a/NEWS	Mon Oct 02 18:35:51 2017 +0200
     1.2 +++ b/NEWS	Mon Oct 02 19:28:18 2017 +0200
     1.3 @@ -14,6 +14,10 @@
     1.4  INCOMPATIBILITY for old developments that have not been updated to
     1.5  Isabelle2017 yet (using the "isabelle imports" tool).
     1.6  
     1.7 +* Command 'external_file' declares the formal dependency on the given
     1.8 +file name, such that the Isabelle build process knows about it, but
     1.9 +without specific Prover IDE management.
    1.10 +
    1.11  
    1.12  *** HOL ***
    1.13  
     2.1 --- a/src/Doc/Isar_Ref/Spec.thy	Mon Oct 02 18:35:51 2017 +0200
     2.2 +++ b/src/Doc/Isar_Ref/Spec.thy	Mon Oct 02 19:28:18 2017 +0200
     2.3 @@ -1177,6 +1177,23 @@
     2.4  \<close>
     2.5  
     2.6  
     2.7 +section \<open>External file dependencies\<close>
     2.8 +
     2.9 +text \<open>
    2.10 +  \begin{matharray}{rcl}
    2.11 +    @{command_def "external_file"} & : & \<open>any \<rightarrow> any\<close> \\
    2.12 +  \end{matharray}
    2.13 +
    2.14 +  @{rail \<open>@@{command external_file} @{syntax name} ';'?\<close>}
    2.15 +
    2.16 +  \<^descr> \<^theory_text>\<open>external_file name\<close> declares the formal dependency on the given file
    2.17 +  name, such that the Isabelle build process knows about it (see also @{cite
    2.18 +  "isabelle-system"}). The file can be read e.g.\ in Isabelle/ML via @{ML
    2.19 +  File.read}, without specific management by the Prover IDE.
    2.20 +\<close>
    2.21 +
    2.22 +
    2.23 +
    2.24  section \<open>Primitive specification elements\<close>
    2.25  
    2.26  subsection \<open>Sorts\<close>
     3.1 --- a/src/Pure/Pure.thy	Mon Oct 02 18:35:51 2017 +0200
     3.2 +++ b/src/Pure/Pure.thy	Mon Oct 02 19:28:18 2017 +0200
     3.3 @@ -20,6 +20,7 @@
     3.4      "definition" "abbreviation" "type_notation" "no_type_notation" "notation"
     3.5      "no_notation" "axiomatization" "alias" "type_alias" "lemmas" "declare"
     3.6      "hide_class" "hide_type" "hide_const" "hide_fact" :: thy_decl
     3.7 +  and "external_file" :: thy_load
     3.8    and "ML_file" "ML_file_debug" "ML_file_no_debug" :: thy_load % "ML"
     3.9    and "SML_file" "SML_file_debug" "SML_file_no_debug" :: thy_load % "ML"
    3.10    and "SML_import" "SML_export" :: thy_decl % "ML"
    3.11 @@ -107,6 +108,20 @@
    3.12  
    3.13  section \<open>Isar commands\<close>
    3.14  
    3.15 +subsection \<open>External file dependencies\<close>
    3.16 +
    3.17 +ML \<open>
    3.18 +  Outer_Syntax.command @{command_keyword external_file} "formal dependency on external file"
    3.19 +    (Parse.position Parse.path >> (fn (s, pos) => Toplevel.keep (fn st =>
    3.20 +      let
    3.21 +        val ctxt = Toplevel.context_of st;
    3.22 +        val _ = Context_Position.report ctxt pos Markup.language_path;
    3.23 +        val path = Path.explode s;
    3.24 +        val _ = Context_Position.report ctxt pos (Markup.path (Path.smart_implode path));
    3.25 +      in () end)));
    3.26 +\<close>
    3.27 +
    3.28 +
    3.29  subsection \<open>Embedded ML text\<close>
    3.30  
    3.31  ML \<open>