Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
lib/Tools/codegen
changeset 30494 c150e6fa4e0d
parent 30242 aea5d7fa7ef5 
--- a/lib/Tools/codegen	Wed Mar 11 20:42:16 2009 +0100
+++ b/lib/Tools/codegen	Thu Mar 12 18:01:25 2009 +0100
@@ -33,8 +33,8 @@
 
 ## main
 
-THY=$(echo $THY | sed -e 's/\\/\\\\"/g; s/"/\\\"/g')
-ISAR="theory Codegen imports \"$THY\" begin export_code $CMD end"
+CODE_CMD=$(echo $CMD | perl -pe 's/\\/\\\\/g; s/"/\\\"/g')
+CTXT_CMD="ML_Context.eval_in (SOME (ProofContext.init (theory \"HOL\"))) false Position.none \"Code_Target.shell_command thyname cmd\";"
+FULL_CMD="val thyname = \"$THY\"; val cmd = \"$CODE_CMD\"; $CTXT_CMD"
 
-echo "$ISAR" | "$ISABELLE_PROCESS" -I "$IMAGE"
-exit ${PIPESTATUS[1]}
+"$ISABELLE" -q -e "$FULL_CMD" "$IMAGE" || exit 1
isabelle