diff -r 2c0af1c2e723 -r ab66951166f3 lib/scripts/getfunctions
--- a/lib/scripts/getfunctions	Thu Nov 29 15:07:18 2018 +0100
+++ b/lib/scripts/getfunctions	Thu Nov 29 15:17:51 2018 +0100
@@ -141,6 +141,21 @@
 }
 export -f isabelle_fonts
 
+function isabelle_fonts_hidden ()
+{
+  local X=""
+  for X in "$@"
+  do
+    if [ -z "$ISABELLE_FONTS_HIDDEN" ]; then
+      ISABELLE_FONTS_HIDDEN="$X"
+    else
+      ISABELLE_FONTS_HIDDEN="$ISABELLE_FONTS_HIDDEN:$X"
+    fi
+  done
+  export ISABELLE_FONTS_HIDDEN
+}
+export -f isabelle_fonts_hidden
+
 #file formats
 function isabelle_file_format ()
 {