scripts/tty/terminal_titler.sh

   1 #!/bin/bash
   2
   3 source "$FEISTY_MEOW_SCRIPTS/core/functions.sh"
   4 source "$FEISTY_MEOW_SCRIPTS/core/common.alias"
   5
   6 # uncomment this to get extra noisy debugging.
   7 #export DEBUG_TERM_TITLE=true
   8
   9 ##############
  10
  11 # puts a specific textual label on the terminal title bar.
  12 # this doesn't consider any previous titles; it just labels the terminal.
  13 # the title may not be visible in some window managers.
  14 function apply_title_to_terminal()
  15 {
  16   title="$*"
  17   # if we weren't given a title, then use just the hostname.  this is the degraded functionality.
  18   if [ -z "${title}" ]; then
  19     title="$(hostname)"
  20   fi
  21
  22   if [ "${TERM}" != "dumb" -a -z "$PBS_ENVIRONMENT" -a \
  23         ! -z "$PS1" -a "${TERM}" != "linux" ]; then
  24     echo -n -e "\033]0;${title}\007"
  25   else
  26     # not running interactively, so just echo the title.
  27     sep
  28     echo "${title}"
  29     sep
  30   fi
  31 }
  32
  33 ##############
  34
  35 # records the current terminal title, pushing it down on the stack of titles,
  36 # possibly prior to a new one being used.
  37 function save_terminal_title()
  38 {
  39   local title="$*"
  40
  41   if [ -z "$title" ]; then
  42     if [ ! -z "$DEBUG_TERM_TITLE" ]; then
  43       echo "terminal_titler: empty title: pushing current title again"
  44     fi
  45     peek_title_stack
  46     title="$LAST_TITLE"
  47     if [ -z "$title" ]; then
  48       log_feisty_meow_event "terminal_titler: there was no saved title, so we're ignoring the save attempt."
  49       return 1
  50     fi
  51   fi
  52
  53 #hmmm: need a validation step here to remove bad chars that conflict with our title compression scheme.
  54
  55   # only slap a comma after the existing value if it wasn't empty.
  56   if [ -z "$TERMINAL_TITLE_STACK" ]; then
  57     export TERMINAL_TITLE_STACK="\"$title\""
  58   else
  59     export TERMINAL_TITLE_STACK="$TERMINAL_TITLE_STACK,\"$title\""
  60   fi
  61
  62   if [ ! -z "$DEBUG_TERM_TITLE" ]; then
  63     echo "terminal_titler: new terminal title stack is:"
  64     echo "$TERMINAL_TITLE_STACK"
  65   fi
  66 }
  67
  68 # takes a terminal title off the stack and sets the LAST_TITLE variable.
  69 function pop_title_stack()
  70 {
  71   # whack our output variable, just in case.
  72   unset LAST_TITLE
  73   # get our stack top.
  74   peek_title_stack
  75   # trim the popped item out of the stack.
  76   if [ ! -z "$TERMINAL_TITLE_STACK" ]; then
  77     TERMINAL_TITLE_STACK="$(echo $TERMINAL_TITLE_STACK | sed -n -e 's/\(.*\),[^,]*$/\1/p')"
  78   fi
  79 }
  80
  81 # like pop, but does not change the stack, effectively handing you the most
  82 # recently set title.
  83 function peek_title_stack()
  84 {
  85   # whack our output variable, just in case.
  86   unset LAST_TITLE
  87
  88   if [ ! -z "$TERMINAL_TITLE_STACK" ]; then
  89     LAST_TITLE="$(echo $TERMINAL_TITLE_STACK | sed -n -e 's/.*","\([^,]*\)"$/\1/p')"
  90     if [ -z "$LAST_TITLE" ]; then
  91       LAST_TITLE="$(echo $TERMINAL_TITLE_STACK | sed -n -e 's/"//gp')"
  92     fi
  93   fi
  94 }
  95
  96 # using our stored terminal title, this replaces the title on the terminal.
  97 function restore_terminal_title()
  98 {
  99   # run the terminal labeller to restore the prior title, if there was one.
 100   pop_title_stack
 101
 102   if [ ! -z "$LAST_TITLE" ]; then
 103     if [ ! -z "$DEBUG_TERM_TITLE" ]; then
 104       echo "terminal_titler: restoring prior terminal title of '$LAST_TITLE'"
 105       echo "terminal_titler: while new title stack is: $TERMINAL_TITLE_STACK"
 106     fi
 107     apply_title_to_terminal "$LAST_TITLE"
 108   fi
 109 }
 110
 111 # sets a title for the terminal with the hostname and other details.
 112 function label_terminal_with_info()
 113 {
 114   # we only label the terminal anew if there's no saved title.
 115   if [ -z "$TERMINAL_TITLE_STACK" ]; then
 116     if [ ! -z "$DEBUG_TERM_TITLE" ]; then
 117       echo "terminal_titler: showing new generated title since prior title was empty"
 118     fi
 119     pruned_host=$(echo $HOSTNAME | sed -e 's/^\([^\.]*\)\..*$/\1/')
 120     date_string=$(date +"%Y %b %e @ %T")
 121     user="$(fm_username)"
 122     if [ -z "$user" ]; then
 123       # try snagging the windoze name.
 124       user=$USERNAME
 125     fi
 126     new_title="-- $user@$pruned_host -- [$date_string]"
 127     apply_title_to_terminal "$new_title"
 128     save_terminal_title "$new_title"
 129   else
 130     # use the former title; paste it back up there just in case.
 131     peek_title_stack
 132     apply_title_to_terminal "$LAST_TITLE"
 133   fi
 134 }
 135
 136 ##############
 137
 138 # user friendly version sets the terminal title and saves the title being added.
 139 function set_terminal_title()
 140 {
 141   apply_title_to_terminal $*
 142   save_terminal_title $*
 143 }
 144
 145 ##############
 146
 147