equal
deleted
inserted
replaced
355 in |
355 in |
356 |
356 |
357 val _ = |
357 val _ = |
358 Outer_Syntax.command @{command_spec "code_reflect"} |
358 Outer_Syntax.command @{command_spec "code_reflect"} |
359 "enrich runtime environment with generated code" |
359 "enrich runtime environment with generated code" |
360 (Parse.name -- Scan.optional (@{keyword "datatypes"} |-- (parse_datatype |
360 (Parse.name -- Scan.optional (@{keyword "datatypes"} |-- Parse.!!! (parse_datatype |
361 ::: Scan.repeat (@{keyword "and"} |-- parse_datatype))) [] |
361 ::: Scan.repeat (@{keyword "and"} |-- parse_datatype))) [] |
362 -- Scan.optional (@{keyword "functions"} |-- Scan.repeat1 Parse.name) [] |
362 -- Scan.optional (@{keyword "functions"} |-- Parse.!!! (Scan.repeat1 Parse.name)) [] |
363 -- Scan.option (@{keyword "file"} |-- Parse.name) |
363 -- Scan.option (@{keyword "file"} |-- Parse.!!! Parse.name) |
364 >> (fn (((module_name, raw_datatypes), raw_functions), some_file) => Toplevel.theory |
364 >> (fn (((module_name, raw_datatypes), raw_functions), some_file) => Toplevel.theory |
365 (code_reflect_cmd raw_datatypes raw_functions module_name some_file))); |
365 (code_reflect_cmd raw_datatypes raw_functions module_name some_file))); |
366 |
366 |
367 end; (*local*) |
367 end; (*local*) |
368 |
368 |