342 Context.>> (Context.map_theory |
342 Context.>> (Context.map_theory |
343 (ML_Context.add_antiq @{binding code} (fn _ => Args.term >> ml_code_antiq))); |
343 (ML_Context.add_antiq @{binding code} (fn _ => Args.term >> ml_code_antiq))); |
344 |
344 |
345 local |
345 local |
346 |
346 |
347 val datatypesK = "datatypes"; |
|
348 val functionsK = "functions"; |
|
349 val fileK = "file"; |
|
350 val andK = "and" |
|
351 |
|
352 val parse_datatype = |
347 val parse_datatype = |
353 Parse.name --| Parse.$$$ "=" -- |
348 Parse.name --| @{keyword "="} -- |
354 (((Parse.sym_ident || Parse.string) >> (fn "_" => NONE | _ => Scan.fail ())) |
349 (((Parse.sym_ident || Parse.string) >> (fn "_" => NONE | _ => Scan.fail ())) |
355 || ((Parse.term ::: (Scan.repeat (Parse.$$$ "|" |-- Parse.term))) >> SOME)); |
350 || ((Parse.term ::: (Scan.repeat (@{keyword "|"} |-- Parse.term))) >> SOME)); |
356 |
351 |
357 in |
352 in |
358 |
353 |
359 val _ = |
354 val _ = |
360 Outer_Syntax.command "code_reflect" "enrich runtime environment with generated code" |
355 Outer_Syntax.command "code_reflect" "enrich runtime environment with generated code" |
361 Keyword.thy_decl (Parse.name -- Scan.optional (Parse.$$$ datatypesK |-- (parse_datatype |
356 Keyword.thy_decl (Parse.name -- Scan.optional (@{keyword "datatypes"} |-- (parse_datatype |
362 ::: Scan.repeat (Parse.$$$ andK |-- parse_datatype))) [] |
357 ::: Scan.repeat (@{keyword "and"} |-- parse_datatype))) [] |
363 -- Scan.optional (Parse.$$$ functionsK |-- Scan.repeat1 Parse.name) [] |
358 -- Scan.optional (@{keyword "functions"} |-- Scan.repeat1 Parse.name) [] |
364 -- Scan.option (Parse.$$$ fileK |-- Parse.name) |
359 -- Scan.option (@{keyword "file"} |-- Parse.name) |
365 >> (fn (((module_name, raw_datatypes), raw_functions), some_file) => Toplevel.theory |
360 >> (fn (((module_name, raw_datatypes), raw_functions), some_file) => Toplevel.theory |
366 (code_reflect_cmd raw_datatypes raw_functions module_name some_file))); |
361 (code_reflect_cmd raw_datatypes raw_functions module_name some_file))); |
367 |
362 |
368 end; (*local*) |
363 end; (*local*) |
369 |
364 |