src/Pure/Pure.thy
changeset 66757 e32750d7acb4
parent 66251 cd935b7cb3fb
child 67013 335a7dce7cb3
     1.1 --- a/src/Pure/Pure.thy	Mon Oct 02 18:35:51 2017 +0200
     1.2 +++ b/src/Pure/Pure.thy	Mon Oct 02 19:28:18 2017 +0200
     1.3 @@ -20,6 +20,7 @@
     1.4      "definition" "abbreviation" "type_notation" "no_type_notation" "notation"
     1.5      "no_notation" "axiomatization" "alias" "type_alias" "lemmas" "declare"
     1.6      "hide_class" "hide_type" "hide_const" "hide_fact" :: thy_decl
     1.7 +  and "external_file" :: thy_load
     1.8    and "ML_file" "ML_file_debug" "ML_file_no_debug" :: thy_load % "ML"
     1.9    and "SML_file" "SML_file_debug" "SML_file_no_debug" :: thy_load % "ML"
    1.10    and "SML_import" "SML_export" :: thy_decl % "ML"
    1.11 @@ -107,6 +108,20 @@
    1.12  
    1.13  section \<open>Isar commands\<close>
    1.14  
    1.15 +subsection \<open>External file dependencies\<close>
    1.16 +
    1.17 +ML \<open>
    1.18 +  Outer_Syntax.command @{command_keyword external_file} "formal dependency on external file"
    1.19 +    (Parse.position Parse.path >> (fn (s, pos) => Toplevel.keep (fn st =>
    1.20 +      let
    1.21 +        val ctxt = Toplevel.context_of st;
    1.22 +        val _ = Context_Position.report ctxt pos Markup.language_path;
    1.23 +        val path = Path.explode s;
    1.24 +        val _ = Context_Position.report ctxt pos (Markup.path (Path.smart_implode path));
    1.25 +      in () end)));
    1.26 +\<close>
    1.27 +
    1.28 +
    1.29  subsection \<open>Embedded ML text\<close>
    1.30  
    1.31  ML \<open>