lib/Tools/usedir
changeset 3636 3f2e55e5bacc
parent 3504 8493dbe2f009
child 3747 cd9b6c86926c
equal deleted inserted replaced
3635:8e6faf192cea 3636:3f2e55e5bacc
    73 
    73 
    74 LOGIC="$1"; shift
    74 LOGIC="$1"; shift
    75 NAME="$1"; shift
    75 NAME="$1"; shift
    76 
    76 
    77 
    77 
       
    78 # prepare directories for html and graph output
       
    79 
       
    80 if [ $HTML = "true" -o $GRAPH = "true" ]; then
       
    81   if [ ! -d $ISABELLE_BROWSER_INFO/gif ]; then
       
    82     mkdir -p $ISABELLE_BROWSER_INFO/gif
       
    83     cp $ISABELLE_HOME/lib/images/*.gif $ISABELLE_BROWSER_INFO/gif
       
    84   fi
       
    85 fi
       
    86 
       
    87 if [ $HTML = "true" -a ! -d $ISABELLE_BROWSER_INFO/html ]; then
       
    88   mkdir -p $ISABELLE_BROWSER_INFO/html
       
    89   cp $ISABELLE_HOME/lib/html/index1.html $ISABELLE_BROWSER_INFO/html/index.html
       
    90 fi
       
    91 
       
    92 if [ $GRAPH = "true" -a ! -d $ISABELLE_BROWSER_INFO/graph ]; then
       
    93   mkdir -p $ISABELLE_BROWSER_INFO/graph
       
    94   cp $ISABELLE_HOME/lib/html/index2.html $ISABELLE_BROWSER_INFO/graph/index.html
       
    95   mkdir $ISABELLE_BROWSER_INFO/graph/GraphBrowser
       
    96   mkdir $ISABELLE_BROWSER_INFO/graph/awtUtilities
       
    97   cp $ISABELLE_HOME/lib/browser/G*/*.class $ISABELLE_BROWSER_INFO/graph/G*
       
    98   cp $ISABELLE_HOME/lib/browser/a*/*.class $ISABELLE_BROWSER_INFO/graph/a*
       
    99 fi
       
   100 
    78 
   101 
    79 ## main
   102 ## main
    80 
   103 
    81 [ -z "$SESSION" ] && SESSION=$(basename $NAME)
   104 [ -z "$SESSION" ] && SESSION=$(basename $NAME)
    82 
   105 
    83 if [ -n "$BUILD" ]; then
   106 if [ -n "$BUILD" ]; then
    84   exec $ISABELLE \
   107   exec $ISABELLE \
    85     -e "make_html := $HTML; set_session\"$SESSION\"; exit_use_dir\".\"; make_html := false;" \
   108     -e "make_html := $HTML; make_graph := $GRAPH; output_dir := \"$ISABELLE_BROWSER_INFO\"; home_path := \"$HOME\"; set_session\"$SESSION\"; exit_use_dir\".\"; make_html := false; make_graph := false;" \
    86     -q -w $LOGIC $NAME
   109     -q -w $LOGIC $NAME
    87 else
   110 else
    88   exec $ISABELLE \
   111   exec $ISABELLE \
    89     -e "make_html := $HTML; set_session\"$SESSION\"; exit_use_dir\"$NAME\"; make_html := false; quit();" \
   112     -e "make_html := $HTML; make_graph := $GRAPH; output_dir := \"$ISABELLE_BROWSER_INFO\"; home_path := \"$HOME\"; set_session\"$SESSION\"; exit_use_dir\"$NAME\"; make_html := false; make_graph := false; quit();" \
    90     -r -q $LOGIC
   113     -r -q $LOGIC
    91 fi
   114 fi