src/Pure/Pure.thy
changeset 66757 e32750d7acb4
parent 66251 cd935b7cb3fb
child 67013 335a7dce7cb3
equal deleted inserted replaced
66756:a1b2ea991ad1 66757:e32750d7acb4
    18   and "typedecl" "type_synonym" "nonterminal" "judgment"
    18   and "typedecl" "type_synonym" "nonterminal" "judgment"
    19     "consts" "syntax" "no_syntax" "translations" "no_translations"
    19     "consts" "syntax" "no_syntax" "translations" "no_translations"
    20     "definition" "abbreviation" "type_notation" "no_type_notation" "notation"
    20     "definition" "abbreviation" "type_notation" "no_type_notation" "notation"
    21     "no_notation" "axiomatization" "alias" "type_alias" "lemmas" "declare"
    21     "no_notation" "axiomatization" "alias" "type_alias" "lemmas" "declare"
    22     "hide_class" "hide_type" "hide_const" "hide_fact" :: thy_decl
    22     "hide_class" "hide_type" "hide_const" "hide_fact" :: thy_decl
       
    23   and "external_file" :: thy_load
    23   and "ML_file" "ML_file_debug" "ML_file_no_debug" :: thy_load % "ML"
    24   and "ML_file" "ML_file_debug" "ML_file_no_debug" :: thy_load % "ML"
    24   and "SML_file" "SML_file_debug" "SML_file_no_debug" :: thy_load % "ML"
    25   and "SML_file" "SML_file_debug" "SML_file_no_debug" :: thy_load % "ML"
    25   and "SML_import" "SML_export" :: thy_decl % "ML"
    26   and "SML_import" "SML_export" :: thy_decl % "ML"
    26   and "ML_prf" :: prf_decl % "proof"  (* FIXME % "ML" ?? *)
    27   and "ML_prf" :: prf_decl % "proof"  (* FIXME % "ML" ?? *)
    27   and "ML_val" "ML_command" :: diag % "ML"
    28   and "ML_val" "ML_command" :: diag % "ML"
   105   "realizability" = ""
   106   "realizability" = ""
   106 begin
   107 begin
   107 
   108 
   108 section \<open>Isar commands\<close>
   109 section \<open>Isar commands\<close>
   109 
   110 
       
   111 subsection \<open>External file dependencies\<close>
       
   112 
       
   113 ML \<open>
       
   114   Outer_Syntax.command @{command_keyword external_file} "formal dependency on external file"
       
   115     (Parse.position Parse.path >> (fn (s, pos) => Toplevel.keep (fn st =>
       
   116       let
       
   117         val ctxt = Toplevel.context_of st;
       
   118         val _ = Context_Position.report ctxt pos Markup.language_path;
       
   119         val path = Path.explode s;
       
   120         val _ = Context_Position.report ctxt pos (Markup.path (Path.smart_implode path));
       
   121       in () end)));
       
   122 \<close>
       
   123 
       
   124 
   110 subsection \<open>Embedded ML text\<close>
   125 subsection \<open>Embedded ML text\<close>
   111 
   126 
   112 ML \<open>
   127 ML \<open>
   113 local
   128 local
   114 
   129