lib/scripts/getfunctions
changeset 71736 a2afc7ed2c68
parent 71733 6c470c918aad
child 72162 5894859c5c84
equal deleted inserted replaced
71735:9644811b5b0a 71736:a2afc7ed2c68
   110     fi
   110     fi
   111   done
   111   done
   112   export ISABELLE_CLASSPATH
   112   export ISABELLE_CLASSPATH
   113 }
   113 }
   114 export -f classpath
   114 export -f classpath
   115 
       
   116 #Isabelle/Scala tools
       
   117 function isabelle_scala_tools ()
       
   118 {
       
   119   local X=""
       
   120   for X in "$@"
       
   121   do
       
   122     if [ -z "$ISABELLE_SCALA_TOOLS" ]; then
       
   123       ISABELLE_SCALA_TOOLS="$X"
       
   124     else
       
   125       ISABELLE_SCALA_TOOLS="$ISABELLE_SCALA_TOOLS:$X"
       
   126     fi
       
   127   done
       
   128   export ISABELLE_SCALA_TOOLS
       
   129 }
       
   130 export -f isabelle_scala_tools
       
   131 
   115 
   132 #Isabelle fonts
   116 #Isabelle fonts
   133 function isabelle_fonts ()
   117 function isabelle_fonts ()
   134 {
   118 {
   135   local X=""
   119   local X=""