src/Tools/Code/lib/Tools/codegen
changeset 57851 33b7372e87ad
parent 54563 7fa522b213a8
equal deleted inserted replaced
57850:34382a1f37d6 57851:33b7372e87ad
    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\"; \