equal
deleted
inserted
replaced
273 |
273 |
274 val _ = |
274 val _ = |
275 OuterSyntax.command codeK "generate executable code for constants" |
275 OuterSyntax.command codeK "generate executable code for constants" |
276 K.diag (P.!!! (code_exprP code_cmd) >> (fn f => Toplevel.keep (f o Toplevel.theory_of))); |
276 K.diag (P.!!! (code_exprP code_cmd) >> (fn f => Toplevel.keep (f o Toplevel.theory_of))); |
277 |
277 |
278 fun codegen_shell_command thyname cmd = Isar.toplevel (fn _ => |
278 fun codegen_shell_command thyname cmd = Toplevel.program (fn _ => |
279 (use_thy thyname; case Scan.read OuterLex.stopper (P.!!! (code_exprP code_cmd)) ((filter OuterLex.is_proper o OuterSyntax.scan) cmd) |
279 (use_thy thyname; case Scan.read OuterLex.stopper (P.!!! (code_exprP code_cmd)) ((filter OuterLex.is_proper o OuterSyntax.scan) cmd) |
280 of SOME f => (writeln "Now generating code..."; f (theory thyname)) |
280 of SOME f => (writeln "Now generating code..."; f (theory thyname)) |
281 | NONE => error ("Bad directive " ^ quote cmd))) |
281 | NONE => error ("Bad directive " ^ quote cmd))) |
282 handle TOPLEVEL_ERROR => OS.Process.exit OS.Process.failure; |
282 handle TOPLEVEL_ERROR => OS.Process.exit OS.Process.failure; |
283 |
283 |