# HG changeset patch
# User wenzelm
# Date 1479669162 -3600
# Node ID 27914a4f8c70e3e79bde470c1e137b3a4e039ab5
# Parent  56972c75502766f7b8c9b4dca6425f7e719b5225
more on "Formal scopes and semantic selection";

diff -r 56972c755027 -r 27914a4f8c70 NEWS
--- a/NEWS	Sun Nov 20 19:08:14 2016 +0100
+++ b/NEWS	Sun Nov 20 20:12:42 2016 +0100
@@ -95,7 +95,7 @@
 * Highlighting of entity def/ref positions wrt. cursor.
 
 * Action "isabelle.select-entity" (shortcut CS+ENTER) selects all
-occurences of the formal entity at the caret position. This facilitates
+occurrences of the formal entity at the caret position. This facilitates
 systematic renaming.
 
 * PIDE document markup works across multiple Isar commands, e.g. the
diff -r 56972c755027 -r 27914a4f8c70 src/Doc/JEdit/JEdit.thy
--- a/src/Doc/JEdit/JEdit.thy	Sun Nov 20 19:08:14 2016 +0100
+++ b/src/Doc/JEdit/JEdit.thy	Sun Nov 20 20:12:42 2016 +0100
@@ -1170,6 +1170,40 @@
 \<close>
 
 
+section \<open>Formal scopes and semantic selection\<close>
+
+text \<open>
+  Formal entities are semantically annotated in the source text as explained
+  in \secref{sec:tooltips-hyperlinks}. A \<^emph>\<open>formal scope\<close> consists of the
+  defining position with all its referencing positions. This correspondence is
+  highlighted in the text according to the cursor position, see also
+  \figref{fig:scope1}. Here the referencing positions are rendered with an
+  additional border, in reminiscence to a hyperlink: clicking there moves the
+  cursor to the original defining position.
+
+  \begin{figure}[!htb]
+  \begin{center}
+  \includegraphics[scale=0.5]{scope1}
+  \end{center}
+  \caption{Scope of formal entity: defining vs.\ referencing positions}
+  \label{fig:scope1}
+  \end{figure}
+
+  The action @{action_def "isabelle.select-entity"} (shortcut \<^verbatim>\<open>CS+ENTER\<close>)
+  supports semantic selection of all occurrences of the formal entity at the
+  caret position. This facilitates systematic renaming, using regular jEdit
+  editing of a multi-selection, see also \figref{fig:scope2}.
+
+  \begin{figure}[!htb]
+  \begin{center}
+  \includegraphics[scale=0.5]{scope2}
+  \end{center}
+  \caption{The result of semantic selection and systematic renaming}
+  \label{fig:scope2}
+  \end{figure}
+\<close>
+
+
 section \<open>Completion \label{sec:completion}\<close>
 
 text \<open>
diff -r 56972c755027 -r 27914a4f8c70 src/Doc/JEdit/document/scope1.png
Binary file src/Doc/JEdit/document/scope1.png has changed
diff -r 56972c755027 -r 27914a4f8c70 src/Doc/JEdit/document/scope2.png
Binary file src/Doc/JEdit/document/scope2.png has changed
diff -r 56972c755027 -r 27914a4f8c70 src/Doc/ROOT
--- a/src/Doc/ROOT	Sun Nov 20 19:08:14 2016 +0100
+++ b/src/Doc/ROOT	Sun Nov 20 20:12:42 2016 +0100
@@ -234,6 +234,8 @@
     "popup2.png"
     "query.png"
     "root.tex"
+    "scope1.png"
+    "scope2.png"
     "sidekick-document.png"
     "sidekick.png"
     "sledgehammer.png"