lib/scripts/getfunctions
changeset 69255 800b1ce96fce
parent 69157 22ae1d926f96
child 69267 517655a528fe
equal deleted inserted replaced
69254:9f8d26b8c731 69255:800b1ce96fce
   106     fi
   106     fi
   107   done
   107   done
   108   export ISABELLE_CLASSPATH
   108   export ISABELLE_CLASSPATH
   109 }
   109 }
   110 export -f classpath
   110 export -f classpath
       
   111 
       
   112 #file formats
       
   113 function isabelle_file_format ()
       
   114 {
       
   115   local X=""
       
   116   for X in "$@"
       
   117   do
       
   118     if [ -z "$ISABELLE_CLASSES_FILE_FORMAT" ]; then
       
   119       ISABELLE_CLASSES_FILE_FORMAT="$X"
       
   120     else
       
   121       ISABELLE_CLASSES_FILE_FORMAT="$ISABELLE_CLASSES_FILE_FORMAT:$X"
       
   122     fi
       
   123   done
       
   124   export ISABELLE_CLASSES_FILE_FORMAT
       
   125 }
       
   126 export -f isabelle_file_format
   111 
   127 
   112 #administrative build
   128 #administrative build
   113 if [ -e "$ISABELLE_HOME/Admin/build" ]; then
   129 if [ -e "$ISABELLE_HOME/Admin/build" ]; then
   114   function isabelle_admin_build ()
   130   function isabelle_admin_build ()
   115   {
   131   {