wenzelm@55118
|
1 |
(*:wrap=hard:maxLineLen=78:*)
|
wenzelm@55118
|
2 |
|
wenzelm@54906
|
3 |
theory JEdit
|
wenzelm@54906
|
4 |
imports Base
|
wenzelm@54906
|
5 |
begin
|
wenzelm@54906
|
6 |
|
wenzelm@54906
|
7 |
chapter {* Introduction *}
|
wenzelm@54906
|
8 |
|
wenzelm@54907
|
9 |
section {* Concepts and terminology *}
|
wenzelm@54907
|
10 |
|
wenzelm@54906
|
11 |
text {* FIXME
|
wenzelm@54906
|
12 |
|
wenzelm@54906
|
13 |
parallel proof checking \cite{Wenzel:2009} \cite{Wenzel:2013:ITP}
|
wenzelm@54906
|
14 |
|
wenzelm@54907
|
15 |
asynchronous user interaction \cite{Wenzel:2010},
|
wenzelm@54907
|
16 |
\cite{Wenzel:2012:UITP-EPTCS}
|
wenzelm@54906
|
17 |
|
wenzelm@54907
|
18 |
document-oriented proof processing and Prover IDE \cite{Wenzel:2011:CICM}
|
wenzelm@54907
|
19 |
\cite{Wenzel:2012}
|
wenzelm@54906
|
20 |
|
wenzelm@54907
|
21 |
\begin{description}
|
wenzelm@54907
|
22 |
|
wenzelm@54907
|
23 |
\item [PIDE] is a general framework for Prover IDEs based on the
|
wenzelm@54907
|
24 |
Isabelle/Scala. It is built around a concept of \emph{asynchronous document
|
wenzelm@54907
|
25 |
processing}, which is supported natively by the \emph{parallel proof engine}
|
wenzelm@54907
|
26 |
that is implemented in Isabelle/ML.
|
wenzelm@54907
|
27 |
|
wenzelm@54907
|
28 |
\item [jEdit] is a sophisticated text editor \url{http://www.jedit.org}
|
wenzelm@54907
|
29 |
implemented in Java. It is easily extensible by plugins written in any
|
wenzelm@54907
|
30 |
language that works on the JVM, e.g.\ Scala.
|
wenzelm@54907
|
31 |
|
wenzelm@54907
|
32 |
\item [Isabelle/jEdit] is the main example application of the PIDE framework
|
wenzelm@54907
|
33 |
and the default user-interface for Isabelle. It is targeted at beginners and
|
wenzelm@54907
|
34 |
experts alike.
|
wenzelm@54907
|
35 |
|
wenzelm@54907
|
36 |
\end{description}
|
wenzelm@54906
|
37 |
*}
|
wenzelm@54906
|
38 |
|
wenzelm@54907
|
39 |
|
wenzelm@54907
|
40 |
section {* The Isabelle/jEdit Prover IDE *}
|
wenzelm@54907
|
41 |
|
wenzelm@54907
|
42 |
text {*
|
wenzelm@54910
|
43 |
\includegraphics[width=\textwidth]{isabelle-jedit}
|
wenzelm@54910
|
44 |
|
wenzelm@54907
|
45 |
Isabelle/jEdit consists of some plugins for the well-known jEdit text
|
wenzelm@54907
|
46 |
editor \url{http://www.jedit.org}, according to the following
|
wenzelm@54907
|
47 |
principles.
|
wenzelm@54907
|
48 |
|
wenzelm@54907
|
49 |
\begin{itemize}
|
wenzelm@54907
|
50 |
|
wenzelm@54907
|
51 |
\item The original jEdit look-and-feel is generally preserved, although
|
wenzelm@54908
|
52 |
some default properties have been changed to accommodate Isabelle (e.g.\
|
wenzelm@54907
|
53 |
the text area font).
|
wenzelm@54907
|
54 |
|
wenzelm@54907
|
55 |
\item Formal Isabelle/Isar text is checked asynchronously while editing.
|
wenzelm@54907
|
56 |
The user is in full command of the editor, and the prover refrains from
|
wenzelm@54907
|
57 |
locking portions of the buffer.
|
wenzelm@54907
|
58 |
|
wenzelm@54907
|
59 |
\item Prover feedback works via colors, boxes, squiggly underline,
|
wenzelm@54907
|
60 |
hyperlinks, popup windows, icons, clickable output, all based on semantic
|
wenzelm@54907
|
61 |
markup produced by Isabelle in the background.
|
wenzelm@54907
|
62 |
|
wenzelm@54907
|
63 |
\item Using the mouse together with the modifier key @{verbatim CONTROL}
|
wenzelm@54907
|
64 |
(Linux, Windows) or @{verbatim COMMAND} (Mac OS X) exposes additional
|
wenzelm@54907
|
65 |
formal content via tooltips and/or hyperlinks.
|
wenzelm@54907
|
66 |
|
wenzelm@54907
|
67 |
\item Dockable panels (e.g. \emph{Output}, \emph{Symbols}) are managed as
|
wenzelm@54907
|
68 |
independent windows by jEdit, which also allows multiple instances.
|
wenzelm@54907
|
69 |
|
wenzelm@54907
|
70 |
\item Formal output (in popups etc.) may be explored recursively, using
|
wenzelm@54907
|
71 |
the same techniques as in the editor source buffer.
|
wenzelm@54907
|
72 |
|
wenzelm@54907
|
73 |
\item The prover process and source files are managed on the editor side.
|
wenzelm@54907
|
74 |
The prover operates on timeless and stateless document content via
|
wenzelm@54907
|
75 |
Isabelle/Scala.
|
wenzelm@54907
|
76 |
|
wenzelm@54907
|
77 |
\item Plugin options of jEdit (for the \emph{Isabelle} plugin) give access
|
wenzelm@54907
|
78 |
to a selection of Isabelle/Scala options and its persistence preferences,
|
wenzelm@54907
|
79 |
usually with immediate effect on the prover back-end or editor front-end.
|
wenzelm@54907
|
80 |
|
wenzelm@54907
|
81 |
\item The logic image of the prover session may be specified within
|
wenzelm@54907
|
82 |
Isabelle/jEdit, but this requires restart. The new image is provided
|
wenzelm@54907
|
83 |
automatically by the Isabelle build process.
|
wenzelm@54907
|
84 |
|
wenzelm@54907
|
85 |
\end{itemize}
|
wenzelm@54907
|
86 |
*}
|
wenzelm@54907
|
87 |
|
wenzelm@54907
|
88 |
|
wenzelm@54907
|
89 |
chapter {* Prover IDE functionality *}
|
wenzelm@54907
|
90 |
|
wenzelm@54907
|
91 |
section {* Isabelle symbols and fonts *}
|
wenzelm@54907
|
92 |
|
wenzelm@54907
|
93 |
text {*
|
wenzelm@54907
|
94 |
Isabelle supports infinitely many symbols:
|
wenzelm@54907
|
95 |
|
wenzelm@54907
|
96 |
\medskip
|
wenzelm@54907
|
97 |
\begin{tabular}{l}
|
wenzelm@54907
|
98 |
@{text "\<alpha>"}, @{text "\<beta>"}, @{text "\<gamma>"}, @{text "\<dots>"} \\
|
wenzelm@54907
|
99 |
@{text "\<forall>"}, @{text "\<exists>"}, @{text "\<or>"}, @{text "\<and>"}, @{text "\<longrightarrow>"}, @{text "\<longleftrightarrow>"}, @{text "\<dots>"} \\
|
wenzelm@54907
|
100 |
@{text "\<le>"}, @{text "\<ge>"}, @{text "\<sqinter>"}, @{text "\<squnion>"}, @{text "\<dots>"} \\
|
wenzelm@54907
|
101 |
@{text "\<aleph>"}, @{text "\<triangle>"}, @{text "\<nabla>"}, @{text "\<dots>"} \\
|
wenzelm@54907
|
102 |
@{verbatim "\<foo>"}, @{verbatim "\<bar>"}, @{verbatim "\<baz>"}, @{text "\<dots>"} \\
|
wenzelm@54907
|
103 |
\end{tabular}
|
wenzelm@54907
|
104 |
\medskip
|
wenzelm@54907
|
105 |
|
wenzelm@54907
|
106 |
A default mapping relates some Isabelle symbols to Unicode points (see
|
wenzelm@55119
|
107 |
@{file "$ISABELLE_HOME/etc/symbols"} and @{verbatim
|
wenzelm@54907
|
108 |
"$ISABELLE_HOME_USER/etc/symbols"}.
|
wenzelm@54907
|
109 |
|
wenzelm@54907
|
110 |
The \emph{IsabelleText} font ensures that Unicode points are actually seen
|
wenzelm@54907
|
111 |
on the screen (or printer).
|
wenzelm@54907
|
112 |
|
wenzelm@54907
|
113 |
\medskip
|
wenzelm@54907
|
114 |
Input methods:
|
wenzelm@54907
|
115 |
\begin{enumerate}
|
wenzelm@54907
|
116 |
\item use the \emph{Symbols} dockable window
|
wenzelm@54907
|
117 |
\item copy/paste from decoded source files
|
wenzelm@54907
|
118 |
\item copy/paste from prover output
|
wenzelm@54908
|
119 |
\item completion provided by Isabelle plugin, e.g.\
|
wenzelm@54907
|
120 |
|
wenzelm@54907
|
121 |
\medskip
|
wenzelm@54907
|
122 |
\begin{tabular}{lll}
|
wenzelm@54908
|
123 |
\textbf{symbol} & \textbf{abbreviation} & \textbf{backslash escape} \\[1ex]
|
wenzelm@54907
|
124 |
|
wenzelm@54908
|
125 |
@{text "\<lambda>"} & @{verbatim "%"} & @{verbatim "\\lambda"} \\
|
wenzelm@54908
|
126 |
@{text "\<Rightarrow>"} & @{verbatim "=>"} & @{verbatim "\\Rightarrow"} \\
|
wenzelm@54908
|
127 |
@{text "\<Longrightarrow>"} & @{verbatim "==>"} & @{verbatim "\\Longrightarrow"} \\
|
wenzelm@54907
|
128 |
|
wenzelm@54908
|
129 |
@{text "\<And>"} & @{verbatim "!!"} & @{verbatim "\\And"} \\
|
wenzelm@54908
|
130 |
@{text "\<equiv>"} & @{verbatim "=="} & @{verbatim "\\equiv"} \\
|
wenzelm@54907
|
131 |
|
wenzelm@54908
|
132 |
@{text "\<forall>"} & @{verbatim "!"} & @{verbatim "\\forall"} \\
|
wenzelm@54908
|
133 |
@{text "\<exists>"} & @{verbatim "?"} & @{verbatim "\\exists"} \\
|
wenzelm@54908
|
134 |
@{text "\<longrightarrow>"} & @{verbatim "-->"} & @{verbatim "\\longrightarrow"} \\
|
wenzelm@54908
|
135 |
@{text "\<and>"} & @{verbatim "&"} & @{verbatim "\\and"} \\
|
wenzelm@54908
|
136 |
@{text "\<or>"} & @{verbatim "|"} & @{verbatim "\\or"} \\
|
wenzelm@54908
|
137 |
@{text "\<not>"} & @{verbatim "~"} & @{verbatim "\\not"} \\
|
wenzelm@54908
|
138 |
@{text "\<noteq>"} & @{verbatim "~="} & @{verbatim "\\noteq"} \\
|
wenzelm@54908
|
139 |
@{text "\<in>"} & @{verbatim ":"} & @{verbatim "\\in"} \\
|
wenzelm@54908
|
140 |
@{text "\<notin>"} & @{verbatim "~:"} & @{verbatim "\\notin"} \\
|
wenzelm@54907
|
141 |
\end{tabular}
|
wenzelm@54907
|
142 |
|
wenzelm@54907
|
143 |
\end{enumerate}
|
wenzelm@54907
|
144 |
|
wenzelm@54907
|
145 |
\paragraph{Notes:}
|
wenzelm@54907
|
146 |
\begin{itemize}
|
wenzelm@54907
|
147 |
|
wenzelm@54907
|
148 |
\item The above abbreviations refer to the input method. The logical
|
wenzelm@54907
|
149 |
notation provides ASCII alternatives that often coincide, but deviate
|
wenzelm@54907
|
150 |
occasionally.
|
wenzelm@54907
|
151 |
|
wenzelm@54907
|
152 |
\item Generic jEdit abbreviations or plugins perform similar source
|
wenzelm@54907
|
153 |
replacement operations; this works for Isabelle as long as the Unicode
|
wenzelm@54907
|
154 |
sequences coincide with the symbol mapping.
|
wenzelm@54907
|
155 |
|
wenzelm@54907
|
156 |
\item Raw Unicode characters within prover source files should be
|
wenzelm@54908
|
157 |
restricted to informal parts, e.g.\ to write text in non-latin alphabets.
|
wenzelm@54907
|
158 |
Mathematical symbols should be defined via the official rendering tables.
|
wenzelm@54907
|
159 |
|
wenzelm@54907
|
160 |
\end{itemize}
|
wenzelm@54907
|
161 |
|
wenzelm@54907
|
162 |
\paragraph{Control symbols.} There are some special control symbols to
|
wenzelm@54907
|
163 |
modify the style of a \emph{single} symbol (without nesting). Control
|
wenzelm@54907
|
164 |
symbols may be applied to a region of selected text, either using the
|
wenzelm@54907
|
165 |
\emph{Symbols} dockable window or keyboard shortcuts.
|
wenzelm@54907
|
166 |
|
wenzelm@54907
|
167 |
\medskip
|
wenzelm@54907
|
168 |
\begin{tabular}{lll}
|
wenzelm@54907
|
169 |
\textbf{symbol} & style & keyboard shortcure \\
|
wenzelm@54907
|
170 |
@{verbatim "\<sup>"} & superscript & @{verbatim "C+e UP"} \\
|
wenzelm@54907
|
171 |
@{verbatim "\<sub>"} & subscript & @{verbatim "C+e DOWN"} \\
|
wenzelm@54907
|
172 |
@{verbatim "\<bold>"} & bold face & @{verbatim "C+e RIGHT"} \\
|
wenzelm@54907
|
173 |
& reset & @{verbatim "C+e LEFT"} \\
|
wenzelm@54907
|
174 |
\end{tabular}
|
wenzelm@54907
|
175 |
*}
|
wenzelm@54907
|
176 |
|
wenzelm@54907
|
177 |
|
wenzelm@54907
|
178 |
section {* Text completion *}
|
wenzelm@54906
|
179 |
|
wenzelm@55118
|
180 |
text {*
|
wenzelm@55118
|
181 |
Text completion works via some light-weight GUI popup, which is triggered by
|
wenzelm@55118
|
182 |
keyboard events during the normal editing process in the main jEdit text
|
wenzelm@55118
|
183 |
area and a few additional text fields. The popup interprets special keys:
|
wenzelm@55118
|
184 |
@{verbatim TAB}, @{verbatim ESCAPE}, @{verbatim UP}, @{verbatim DOWN},
|
wenzelm@55118
|
185 |
@{verbatim PAGE_UP}, @{verbatim PAGE_DOWN}. All other key events are passed
|
wenzelm@55118
|
186 |
to the jEdit text area --- this allows to ignore unwanted completions most
|
wenzelm@55118
|
187 |
of the time and continue typing quickly.
|
wenzelm@55118
|
188 |
|
wenzelm@55118
|
189 |
Various Isabelle plugin options control the popup behavior and immediate
|
wenzelm@55118
|
190 |
insertion into buffer.
|
wenzelm@55118
|
191 |
|
wenzelm@55118
|
192 |
Isabelle Symbols are completed in backslashed forms, e.g. @{verbatim
|
wenzelm@55118
|
193 |
"\\"}@{verbatim "forall"} or @{verbatim "\<forall>"} that both produce the Isabelle
|
wenzelm@55119
|
194 |
symbol @{text "\<forall>"} in its Unicode rendering. Alternatively, symbol
|
wenzelm@55119
|
195 |
abbreviations may be used as specified in @{file
|
wenzelm@55119
|
196 |
"$ISABELLE_HOME/etc/symbols"}.
|
wenzelm@55118
|
197 |
|
wenzelm@55118
|
198 |
\emph{Explicit completion} works via standard jEdit shortcut @{verbatim
|
wenzelm@55118
|
199 |
"C+b"}, which is remapped to action @{verbatim "isabelle.complete"}, with a
|
wenzelm@55118
|
200 |
fall-back on regular @{verbatim "complete-word"} for non-Isabelle buffers.
|
wenzelm@55118
|
201 |
|
wenzelm@55118
|
202 |
\emph{Implicit completion} works via keyboard input on text area, with popup
|
wenzelm@55118
|
203 |
or immediate insertion into buffer. Plain words require at least 3
|
wenzelm@55118
|
204 |
characters to be completed.
|
wenzelm@55118
|
205 |
|
wenzelm@55118
|
206 |
\emph{Immediate completion} means the (unique) replacement text is inserted
|
wenzelm@55118
|
207 |
into the buffer without popup. This mode ignores plain words and requires
|
wenzelm@55118
|
208 |
more than one characters for symbol abbreviations. Otherwise it falls back
|
wenzelm@55118
|
209 |
on completion popup.
|
wenzelm@55118
|
210 |
*}
|
wenzelm@54906
|
211 |
|
wenzelm@54907
|
212 |
|
wenzelm@54907
|
213 |
chapter {* Known problems and workarounds *}
|
wenzelm@54907
|
214 |
|
wenzelm@54907
|
215 |
text {*
|
wenzelm@54907
|
216 |
\begin{itemize}
|
wenzelm@54907
|
217 |
|
wenzelm@54907
|
218 |
\item \textbf{Problem:} Keyboard shortcuts @{verbatim "C+PLUS"} and
|
wenzelm@54907
|
219 |
@{verbatim "C+MINUS"} for adjusting the editor font size depend on
|
wenzelm@54907
|
220 |
platform details and national keyboards.
|
wenzelm@54907
|
221 |
|
wenzelm@54907
|
222 |
\textbf{Workaround:} Use numeric keypad or rebind keys in the
|
wenzelm@54907
|
223 |
jEdit Shortcuts options dialog.
|
wenzelm@54907
|
224 |
|
wenzelm@54907
|
225 |
\item \textbf{Problem:} Lack of dependency management for auxiliary files
|
wenzelm@54908
|
226 |
that contribute to a theory (e.g.\ @{command ML_file}).
|
wenzelm@54907
|
227 |
|
wenzelm@54907
|
228 |
\textbf{Workaround:} Re-load files manually within the prover.
|
wenzelm@54907
|
229 |
|
wenzelm@54907
|
230 |
\item \textbf{Problem:} Odd behavior of some diagnostic commands with
|
wenzelm@54907
|
231 |
global side-effects, like writing a physical file.
|
wenzelm@54907
|
232 |
|
wenzelm@54907
|
233 |
\textbf{Workaround:} Avoid such commands.
|
wenzelm@54907
|
234 |
|
wenzelm@54907
|
235 |
\item \textbf{Problem:} No way to delete document nodes from the overall
|
wenzelm@54907
|
236 |
collection of theories.
|
wenzelm@54907
|
237 |
|
wenzelm@54907
|
238 |
\textbf{Workaround:} Restart whole Isabelle/jEdit session in worst-case
|
wenzelm@54907
|
239 |
situation.
|
wenzelm@54907
|
240 |
|
wenzelm@54907
|
241 |
\item \textbf{Problem:} Linux: some desktop environments with extreme
|
wenzelm@54907
|
242 |
animation effects may disrupt Java 7 window placement and/or keyboard
|
wenzelm@54907
|
243 |
focus.
|
wenzelm@54907
|
244 |
|
wenzelm@54907
|
245 |
\textbf{Workaround:} Disable such effects.
|
wenzelm@54907
|
246 |
|
wenzelm@54907
|
247 |
\item \textbf{Problem:} Linux: some X11 window managers that are not
|
wenzelm@54907
|
248 |
``re-parenting'' cause problems with additional windows opened by the Java
|
wenzelm@54907
|
249 |
VM. This affects either historic or neo-minimalistic window managers like
|
wenzelm@54907
|
250 |
``@{verbatim awesome}'' or ``@{verbatim xmonad}''.
|
wenzelm@54907
|
251 |
|
wenzelm@54907
|
252 |
\textbf{Workaround:} Use regular re-parenting window manager.
|
wenzelm@54907
|
253 |
|
wenzelm@55023
|
254 |
\item \textbf{Problem:} The Mac OS X keyboard shortcut @{verbatim
|
wenzelm@55023
|
255 |
"COMMAND+COMMA"} for Preferences is in conflict with the jEdit default
|
wenzelm@55023
|
256 |
binding for @{verbatim "quick-search"}.
|
wenzelm@54907
|
257 |
|
wenzelm@55023
|
258 |
\textbf{Workaround:} Remap in jEdit manually according to national
|
wenzelm@55023
|
259 |
keyboard, e.g.\ @{verbatim "COMMAND+SLASH"} on English ones.
|
wenzelm@54907
|
260 |
|
wenzelm@54907
|
261 |
\item \textbf{Problem:} Mac OS X: Java 7 is officially supported on Lion
|
wenzelm@54907
|
262 |
and Mountain Lion, but not Snow Leopard. It usually works on the latter,
|
wenzelm@54907
|
263 |
although with a small risk of instabilities.
|
wenzelm@54907
|
264 |
|
wenzelm@54907
|
265 |
\textbf{Workaround:} Update to OS X Mountain Lion, or later.
|
wenzelm@54907
|
266 |
|
wenzelm@54907
|
267 |
\end{itemize}
|
wenzelm@54907
|
268 |
*}
|
wenzelm@54907
|
269 |
|
wenzelm@54906
|
270 |
end |