more on "Formal scopes and semantic selection";
authorwenzelm
Sun Nov 20 20:12:42 2016 +0100 (2016-11-20)
changeset 6451427914a4f8c70
parent 64513 56972c755027
child 64515 29f0b8d2f952
more on "Formal scopes and semantic selection";
NEWS
src/Doc/JEdit/JEdit.thy
src/Doc/JEdit/document/scope1.png
src/Doc/JEdit/document/scope2.png
src/Doc/ROOT
     1.1 --- a/NEWS	Sun Nov 20 19:08:14 2016 +0100
     1.2 +++ b/NEWS	Sun Nov 20 20:12:42 2016 +0100
     1.3 @@ -95,7 +95,7 @@
     1.4  * Highlighting of entity def/ref positions wrt. cursor.
     1.5  
     1.6  * Action "isabelle.select-entity" (shortcut CS+ENTER) selects all
     1.7 -occurences of the formal entity at the caret position. This facilitates
     1.8 +occurrences of the formal entity at the caret position. This facilitates
     1.9  systematic renaming.
    1.10  
    1.11  * PIDE document markup works across multiple Isar commands, e.g. the
     2.1 --- a/src/Doc/JEdit/JEdit.thy	Sun Nov 20 19:08:14 2016 +0100
     2.2 +++ b/src/Doc/JEdit/JEdit.thy	Sun Nov 20 20:12:42 2016 +0100
     2.3 @@ -1170,6 +1170,40 @@
     2.4  \<close>
     2.5  
     2.6  
     2.7 +section \<open>Formal scopes and semantic selection\<close>
     2.8 +
     2.9 +text \<open>
    2.10 +  Formal entities are semantically annotated in the source text as explained
    2.11 +  in \secref{sec:tooltips-hyperlinks}. A \<^emph>\<open>formal scope\<close> consists of the
    2.12 +  defining position with all its referencing positions. This correspondence is
    2.13 +  highlighted in the text according to the cursor position, see also
    2.14 +  \figref{fig:scope1}. Here the referencing positions are rendered with an
    2.15 +  additional border, in reminiscence to a hyperlink: clicking there moves the
    2.16 +  cursor to the original defining position.
    2.17 +
    2.18 +  \begin{figure}[!htb]
    2.19 +  \begin{center}
    2.20 +  \includegraphics[scale=0.5]{scope1}
    2.21 +  \end{center}
    2.22 +  \caption{Scope of formal entity: defining vs.\ referencing positions}
    2.23 +  \label{fig:scope1}
    2.24 +  \end{figure}
    2.25 +
    2.26 +  The action @{action_def "isabelle.select-entity"} (shortcut \<^verbatim>\<open>CS+ENTER\<close>)
    2.27 +  supports semantic selection of all occurrences of the formal entity at the
    2.28 +  caret position. This facilitates systematic renaming, using regular jEdit
    2.29 +  editing of a multi-selection, see also \figref{fig:scope2}.
    2.30 +
    2.31 +  \begin{figure}[!htb]
    2.32 +  \begin{center}
    2.33 +  \includegraphics[scale=0.5]{scope2}
    2.34 +  \end{center}
    2.35 +  \caption{The result of semantic selection and systematic renaming}
    2.36 +  \label{fig:scope2}
    2.37 +  \end{figure}
    2.38 +\<close>
    2.39 +
    2.40 +
    2.41  section \<open>Completion \label{sec:completion}\<close>
    2.42  
    2.43  text \<open>
     3.1 Binary file src/Doc/JEdit/document/scope1.png has changed
     4.1 Binary file src/Doc/JEdit/document/scope2.png has changed
     5.1 --- a/src/Doc/ROOT	Sun Nov 20 19:08:14 2016 +0100
     5.2 +++ b/src/Doc/ROOT	Sun Nov 20 20:12:42 2016 +0100
     5.3 @@ -234,6 +234,8 @@
     5.4      "popup2.png"
     5.5      "query.png"
     5.6      "root.tex"
     5.7 +    "scope1.png"
     5.8 +    "scope2.png"
     5.9      "sidekick-document.png"
    5.10      "sidekick.png"
    5.11      "sledgehammer.png"