src/Doc/JEdit/JEdit.thy
changeset 64514 27914a4f8c70
parent 64513 56972c755027
child 64515 29f0b8d2f952
     1.1 --- a/src/Doc/JEdit/JEdit.thy	Sun Nov 20 19:08:14 2016 +0100
     1.2 +++ b/src/Doc/JEdit/JEdit.thy	Sun Nov 20 20:12:42 2016 +0100
     1.3 @@ -1170,6 +1170,40 @@
     1.4  \<close>
     1.5  
     1.6  
     1.7 +section \<open>Formal scopes and semantic selection\<close>
     1.8 +
     1.9 +text \<open>
    1.10 +  Formal entities are semantically annotated in the source text as explained
    1.11 +  in \secref{sec:tooltips-hyperlinks}. A \<^emph>\<open>formal scope\<close> consists of the
    1.12 +  defining position with all its referencing positions. This correspondence is
    1.13 +  highlighted in the text according to the cursor position, see also
    1.14 +  \figref{fig:scope1}. Here the referencing positions are rendered with an
    1.15 +  additional border, in reminiscence to a hyperlink: clicking there moves the
    1.16 +  cursor to the original defining position.
    1.17 +
    1.18 +  \begin{figure}[!htb]
    1.19 +  \begin{center}
    1.20 +  \includegraphics[scale=0.5]{scope1}
    1.21 +  \end{center}
    1.22 +  \caption{Scope of formal entity: defining vs.\ referencing positions}
    1.23 +  \label{fig:scope1}
    1.24 +  \end{figure}
    1.25 +
    1.26 +  The action @{action_def "isabelle.select-entity"} (shortcut \<^verbatim>\<open>CS+ENTER\<close>)
    1.27 +  supports semantic selection of all occurrences of the formal entity at the
    1.28 +  caret position. This facilitates systematic renaming, using regular jEdit
    1.29 +  editing of a multi-selection, see also \figref{fig:scope2}.
    1.30 +
    1.31 +  \begin{figure}[!htb]
    1.32 +  \begin{center}
    1.33 +  \includegraphics[scale=0.5]{scope2}
    1.34 +  \end{center}
    1.35 +  \caption{The result of semantic selection and systematic renaming}
    1.36 +  \label{fig:scope2}
    1.37 +  \end{figure}
    1.38 +\<close>
    1.39 +
    1.40 +
    1.41  section \<open>Completion \label{sec:completion}\<close>
    1.42  
    1.43  text \<open>