5 # DESCRIPTION: build object-logic or run examples
15 echo "Usage: $PRG LOGIC NAME"
18 echo " -b build mode (output heap image, using current dir)"
19 echo " -i BOOL generate theory browsing information,"
20 echo " i.e. HTML / graph data (default false)"
21 echo " -r reset session path"
22 echo " -s NAME override session NAME"
24 echo " Build object-logic or run examples. Also creates browsing"
25 echo " information (HTML etc.) according to settings."
31 ## process command line
43 while getopts "bi:rs:" OPT
65 getoptions $ISABELLE_USEDIR_OPTIONS
68 shift $(($OPTIND - 1))
78 [ -z "$SESSION" ] && SESSION=$(basename $NAME)
84 # prepare browser info dir
86 if [ "$INFO" = "true" -a ! -f $ISABELLE_BROWSER_INFO/index.html ]; then
88 mkdir -p $ISABELLE_BROWSER_INFO/gif
89 cp $ISABELLE_HOME/lib/images/blue_arrow.gif $ISABELLE_BROWSER_INFO/gif
90 cp $ISABELLE_HOME/lib/images/red_arrow.gif $ISABELLE_BROWSER_INFO/gif
91 cp $ISABELLE_HOME/lib/logo/isabelle.gif $ISABELLE_BROWSER_INFO/gif/isabelle.gif
92 cp $ISABELLE_HOME/lib/html/index1.html $ISABELLE_BROWSER_INFO/index.html
94 mkdir -p $ISABELLE_BROWSER_INFO/graph
95 cp $ISABELLE_HOME/lib/html/index2.html $ISABELLE_BROWSER_INFO/graph/index.html
96 mkdir $ISABELLE_BROWSER_INFO/graph/GraphBrowser
97 mkdir $ISABELLE_BROWSER_INFO/graph/awtUtilities
98 cp $ISABELLE_HOME/lib/browser/GraphBrowser/*.class $ISABELLE_BROWSER_INFO/graph/GraphBrowser
99 cp $ISABELLE_HOME/lib/browser/awtUtilities/*.class $ISABELLE_BROWSER_INFO/graph/awtUtilities
106 LOGDIR="$ISABELLE_OUTPUT/log"
114 PARENT=$(basename "$LOGIC")
116 if [ -n "$BUILD" ]; then
118 echo -n "Building $ITEM ... "
122 -e "Session.use_dir $RESET $INFO \"$PARENT\" \"$SESSION\";" \
123 -q -w $LOGIC $NAME > $LOG 2>&1
126 ITEM=$(basename $LOGIC)-"$SESSION"
127 echo -n "Running $ITEM ... "
132 -e "Session.use_dir $RESET $INFO \"$PARENT\" \"$SESSION\"; quit();" \
133 -r -q $LOGIC > $LOG 2>&1
138 ELAPSED=$($ISABELLE_HOME/lib/scripts/showtime $SECONDS)
143 if [ $RC -eq 0 ]; then
144 echo "OK ($ELAPSED elapsed time)"
148 echo "(see also $LOG)"
149 echo; tail $LOG; echo