equal
deleted
inserted
replaced
958 |
958 |
959 val _ = |
959 val _ = |
960 Outer_Syntax.command @{command_keyword code_thms} |
960 Outer_Syntax.command @{command_keyword code_thms} |
961 "print system of code equations for code" |
961 "print system of code equations for code" |
962 (Scan.repeat1 Parse.term >> (fn cs => |
962 (Scan.repeat1 Parse.term >> (fn cs => |
963 Toplevel.unknown_context o |
963 Toplevel.keep (fn st => code_thms_cmd (Toplevel.context_of st) cs))); |
964 Toplevel.keep (fn state => code_thms_cmd (Toplevel.context_of state) cs))); |
|
965 |
964 |
966 val _ = |
965 val _ = |
967 Outer_Syntax.command @{command_keyword code_deps} |
966 Outer_Syntax.command @{command_keyword code_deps} |
968 "visualize dependencies of code equations for code" |
967 "visualize dependencies of code equations for code" |
969 (Scan.repeat1 Parse.term >> (fn cs => |
968 (Scan.repeat1 Parse.term >> (fn cs => |
970 Toplevel.unknown_context o |
|
971 Toplevel.keep (fn st => code_deps_cmd (Toplevel.context_of st) cs))); |
969 Toplevel.keep (fn st => code_deps_cmd (Toplevel.context_of st) cs))); |
972 |
970 |
973 end; |
971 end; |
974 |
972 |
975 end; (*struct*) |
973 end; (*struct*) |