Admin/makebin
changeset 17575 c45677c1aea0
parent 17573 4de614cc6509
child 17660 94bbe14c088e
equal deleted inserted replaced
17574:aa9d8483cabc 17575:c45677c1aea0
   100 with_path ".." use_thy "HOL4Syntax";
   100 with_path ".." use_thy "HOL4Syntax";
   101 use_thy "HOL4Prob";
   101 use_thy "HOL4Prob";
   102 use_thy "HOL4";
   102 use_thy "HOL4";
   103 EOF
   103 EOF
   104 
   104 
       
   105 perl -pi \
       
   106   -e 's:^ISABELLE_USEDIR_OPTIONS=.*$:ISABELLE_USEDIR_OPTIONS="-p 1":;' \
       
   107   -e 's:^HOL_USEDIR_OPTIONS=.*$:HOL_USEDIR_OPTIONS="-p 2":;' \
       
   108   etc/settings
       
   109 
   105 if [ -n "$DO_LIBRARY" ]; then
   110 if [ -n "$DO_LIBRARY" ]; then
   106   perl -pi -e 's:^ISABELLE_USEDIR_OPTIONS=.*$:ISABELLE_USEDIR_OPTIONS="-i true -d pdf -V outline=/proof,/ML":' \
   111   perl -pi -e 's:^ISABELLE_USEDIR_OPTIONS=.*$:ISABELLE_USEDIR_OPTIONS="-p 1 -i true -d pdf -V outline=/proof,/ML":;' \
   107     etc/settings
       
   108 else
       
   109   perl -pi -e 's:^ISABELLE_USEDIR_OPTIONS=.*$:ISABELLE_USEDIR_OPTIONS="-p 2":' \
       
   110     etc/settings
   112     etc/settings
   111 fi
   113 fi
   112 
   114 
   113 ISABELLE_HOME_USER=$(./bin/isatool getenv -b ISABELLE_HOME_USER)
   115 ISABELLE_HOME_USER=$(./bin/isatool getenv -b ISABELLE_HOME_USER)
   114 [ -f "$ISABELLE_HOME_USER/etc/settings" ] && \
   116 [ -f "$ISABELLE_HOME_USER/etc/settings" ] && \
   130   mkdir browser_info
   132   mkdir browser_info
   131 elif [ -n "$DO_LIBRARY" ]; then
   133 elif [ -n "$DO_LIBRARY" ]; then
   132   ./build -bait
   134   ./build -bait
   133 else
   135 else
   134   ./build -b -m HOL-Complex HOL
   136   ./build -b -m HOL-Complex HOL
       
   137   ./build -b -m HOL4 HOL
   135   ./build -b ZF
   138   ./build -b ZF
   136   perl -pi -e 's/^ISABELLE_USEDIR_OPTIONS=.*$/ISABELLE_USEDIR_OPTIONS="-p 1"/' \
       
   137     etc/settings
       
   138   ./build -b -m HOL4 HOL
       
   139   rm -f "heaps/$COMPILER/Pure" "heaps/$COMPILER/FOL"
   139   rm -f "heaps/$COMPILER/Pure" "heaps/$COMPILER/FOL"
   140 fi
   140 fi
   141 
   141 
   142 
   142 
   143 # prepare result
   143 # prepare result