Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-06-16 22:21:25 -0700 (Wed, 16 Jun 2004)
Revision: 5913
Log message:
Centralized the shell handling of the "display method" data (including
display mode, display base, display width and display destination).
In partucilar:
- The set_dfmode function now takes effect immediatelly (no need to
cd "/";; cd "/back/where/we/were";; after a set_dfmode).
- The bug with "prl" mode output in "-browser" sessions seems to be gone!
- The separation between display modes ("prl"/"src"/"html"/"tex"/"raw"/etc)
and display "types" (i.e. destinations - Tex/Text/Browser) is now more
complete (in fact we now _never_ convert modes into types).
- The code for handling the display method data is no longer duplicated 5 times
(now all code is in shell_core and proof_edit).