# HG changeset patch # User haftmann # Date 1235978763 -3600 # Node ID 391e10b42889eddaef4d031b901c07fd27bc4031 # Parent 51e3e0e821c5b61e8caa1798ebfbb0de0bba2116 using plain ISABELLE_PROCESS diff -r 51e3e0e821c5 -r 391e10b42889 lib/Tools/codegen --- a/lib/Tools/codegen Mon Mar 02 08:15:54 2009 +0100 +++ b/lib/Tools/codegen Mon Mar 02 08:26:03 2009 +0100 @@ -36,6 +36,5 @@ THY=$(echo $THY | sed -e 's/\\/\\\\"/g; s/"/\\\"/g') ISAR="theory Codegen imports \"$THY\" begin export_code $CMD end" -export ISABELLE_LINE_EDITOR="" -echo "$ISAR" | "$ISABELLE_TOOL" tty -l "$IMAGE" +echo "$ISAR" | "$ISABELLE_PROCESS" -I "$IMAGE" exit ${PIPESTATUS[1]}