\chapter{Preliminaries}

 %############################################################################

 \subsection{General}

 %----------------------------------------------------------------------------

 {\bf\UR{The screen-reader superimposes the Braille display \label{sreader-braille}}} in the software hierarchy, i.e. the former determines output of the latter.

 \subsection{Specify Phase}

 %----------------------------------------------------------------------------

 \subsection{Terms}

 %----------------------------------------------------------------------------

 {\bf\UR{Terms are presented as strings in Braille format\label{term-str}}} for 

 the blind user and as Isabelle strings for other users at the same time --- 

 for the purpose of inclusive learning in front of one and the same screen. 

 ?TODO is this reasonable?

 {\bf\UR{The Braille-format can be changed\label{braille-format}}} to different 

 standards.

 {\bf\UR{Sub-terms are presented as strings\label{sub-term-str}}} the same way 

 as whole terms. The location within the whole term is indicated by ?TODO?

 {\bf\UR{A term can be shown as a tree\label{term-tree}}} if requested by a 

 special key, TODO. The key followed by an integer argument determines the 

 depth of the tree. For instance $<$TODO 1$>$ displays the term 

 $\frac{\frac{1}{x}}{\frac{2}{y}}$ 

 \begin{tabbing}

 with argument \=$/$ \=1 / x 1234567890\=$/$ \=$/$ \=\=\kill

 with argument \>$1$ \>                \>$2$       \\

               \>$/$ \>                \>$/$       \\

               \>    \> 1 / x          \>\>$/$     \\

               \>    \> 2 / y          \>\>\> 1    \\

               \>    \>                \>\>\> x    \\

               \>    \>                \>\>$/$     \\

               \>    \>                \>\>\> 2    \\

               \>    \>                \>\>\> y

 \end{tabbing}

 TODO?: ``Dann eine Taste definieren, durch deren Dr\"ucken das Innere des 

 ersten Klammerpaares - Z\"ahler - genauer angezeigt wird, sobald sich der 

 Cursor auf einer der begrenzenden Klammern befindet.

 Umgekehrt: Stehe ich irgendwo im Z\"ahler eines Bruches, dann soll es eine 

 Taste geben, mit der sich der Z\"ahler zu einem geschweiften Klammerpaar 

 verdichtet, vielleicht sogar eine Taste, mit der der Nenner das gleichzeitig 

 auch tut.''

 {\bf\UR{Navigation through sub-terms is hierarchical\label{navi-sub-terms}}} 

 and supported by a special key combined with the arrow keys as follows:

 \begin{compactenum}

 \item $<$STRG$>$ $<\rightarrow>$ next element right on the same level; 

 acoustical indication at the end of the level.

 \item $<$STRG$>$ $<\leftarrow>$ next element left on the same level; 

 acoustical indication at the end of the level.

 \item $<$STRG$>$ $<\uparrow>$ next element on the higher level; acoustical 

 indication at the root.

 \item $<$STRG$>$ $<\downarrow>$ next element on the lower level; acoustical 

 indication at the bottom.

 \end{compactenum}

 {\bf\UR{Semantic information is available for all elements of 

 terms.\label{term-semantic}}} Such information is:

 \begin{compactenum}

 \item the type for constants and variables by a pop-up.

 \item the scope of a variable by (TODO ``internal'' and ``global'' seems to 

 coarse).

 \item the definition of constants and variables by jumping to the respective 

 location, probably in another file.

 \end{compactenum}