reconsider 'export_code' as "thy_decl" command due to its global side-effect on the file-system;
authorwenzelm
Mon Feb 25 13:31:02 2013 +0100 (2013-02-25)
changeset 512753928173409e4
parent 51274 cfc83ad52571
child 51276 05522141d244
reconsider 'export_code' as "thy_decl" command due to its global side-effect on the file-system;
etc/isar-keywords.el
src/Tools/Code_Generator.thy
     1.1 --- a/etc/isar-keywords.el	Mon Feb 25 13:29:19 2013 +0100
     1.2 +++ b/etc/isar-keywords.el	Mon Feb 25 13:31:02 2013 +0100
     1.3 @@ -383,7 +383,6 @@
     1.4      "code_deps"
     1.5      "code_thms"
     1.6      "display_drafts"
     1.7 -    "export_code"
     1.8      "find_consts"
     1.9      "find_theorems"
    1.10      "find_unused_assms"
    1.11 @@ -510,6 +509,7 @@
    1.12      "domain_isomorphism"
    1.13      "domaindef"
    1.14      "equivariance"
    1.15 +    "export_code"
    1.16      "extract"
    1.17      "extract_type"
    1.18      "fixrec"
     2.1 --- a/src/Tools/Code_Generator.thy	Mon Feb 25 13:29:19 2013 +0100
     2.2 +++ b/src/Tools/Code_Generator.thy	Mon Feb 25 13:31:02 2013 +0100
     2.3 @@ -7,8 +7,8 @@
     2.4  theory Code_Generator
     2.5  imports Pure
     2.6  keywords
     2.7 -  "value" "print_codeproc" "code_thms" "code_deps" "export_code" :: diag and
     2.8 -  "code_class" "code_instance" "code_type"
     2.9 +  "value" "print_codeproc" "code_thms" "code_deps" :: diag and
    2.10 +  "export_code" "code_class" "code_instance" "code_type"
    2.11      "code_const" "code_reserved" "code_include" "code_modulename"
    2.12      "code_abort" "code_monad" "code_reflect" :: thy_decl and
    2.13    "datatypes" "functions" "module_name" "file" "checking"