equal
deleted
inserted
replaced
86 ITEM="RAW" |
86 ITEM="RAW" |
87 echo "Building $ITEM ..." |
87 echo "Building $ITEM ..." |
88 LOG="$LOGDIR/$ITEM" |
88 LOG="$LOGDIR/$ITEM" |
89 |
89 |
90 "$ISABELLE_PROCESS" \ |
90 "$ISABELLE_PROCESS" \ |
91 -e "val ml_system = \"$ML_SYSTEM\";" \ |
|
92 -e "val ml_platform = \"$ML_PLATFORM\";" \ |
|
93 -e "use\"$COMPAT\" handle _ => exit 1;" \ |
91 -e "use\"$COMPAT\" handle _ => exit 1;" \ |
94 -e "structure Isar = struct fun main () = () end;" \ |
92 -e "structure Isar = struct fun main () = () end;" \ |
95 -e "ml_prompts \"ML> \" \"ML# \";" \ |
93 -e "ml_prompts \"ML> \" \"ML# \";" \ |
96 -q -w RAW_ML_SYSTEM RAW > "$LOG" 2>&1 |
94 -q -w RAW_ML_SYSTEM RAW > "$LOG" 2>&1 |
97 RC="$?" |
95 RC="$?" |
108 ITEM="Pure" |
106 ITEM="Pure" |
109 echo "Building $ITEM ..." |
107 echo "Building $ITEM ..." |
110 LOG="$LOGDIR/$ITEM" |
108 LOG="$LOGDIR/$ITEM" |
111 |
109 |
112 "$ISABELLE_PROCESS" \ |
110 "$ISABELLE_PROCESS" \ |
113 -e "val ml_system = \"$ML_SYSTEM\";" \ |
|
114 -e "val ml_platform = \"$ML_PLATFORM\";" \ |
|
115 -e "(use\"$COMPAT\"; use\"ROOT.ML\") handle _ => exit 1;" \ |
111 -e "(use\"$COMPAT\"; use\"ROOT.ML\") handle _ => exit 1;" \ |
116 -e "ml_prompts \"ML> \" \"ML# \";" \ |
112 -e "ml_prompts \"ML> \" \"ML# \";" \ |
117 -f -q -w RAW_ML_SYSTEM Pure > "$LOG" 2>&1 |
113 -f -q -w RAW_ML_SYSTEM Pure > "$LOG" 2>&1 |
118 RC="$?" |
114 RC="$?" |
119 fi |
115 fi |