equal
deleted
inserted
replaced
48 CODE_EXPR=$(echo "$1" | perl -pe 's/\\/\\\\/g; s/"/\\\"/g') |
48 CODE_EXPR=$(echo "$1" | perl -pe 's/\\/\\\\/g; s/"/\\\"/g') |
49 |
49 |
50 |
50 |
51 ## invoke code generation |
51 ## invoke code generation |
52 |
52 |
53 FORMAL_CMD="Toplevel.program (fn () => (use_thy thyname; ML_Context.eval_text_in \ |
53 FORMAL_CMD="Runtime.toplevel_program (fn () => (use_thy thyname; ML_Context.eval_source_in \ |
54 (SOME (Proof_Context.init_global (Thy_Info.get_theory thyname))) false Position.none ml_cmd)) \ |
54 (SOME (Proof_Context.init_global (Thy_Info.get_theory thyname))) \ |
|
55 ML_Compiler.flags \ |
|
56 {delimited=true, text=ml_cmd, pos=Position.none})) \ |
55 handle _ => exit 1;" |
57 handle _ => exit 1;" |
56 |
58 |
57 ACTUAL_CMD="val thyname = \"$THYNAME\"; \ |
59 ACTUAL_CMD="val thyname = \"$THYNAME\"; \ |
58 val cmd_expr = \"$CODE_EXPR\"; \ |
60 val cmd_expr = \"$CODE_EXPR\"; \ |
59 val ml_cmd = \"Code_Target.codegen_tool thyname cmd_expr\"; \ |
61 val ml_cmd = \"Code_Target.codegen_tool thyname cmd_expr\"; \ |