1236 |
1236 |
1237 |
1237 |
1238 subsection {* Input events \label{sec:completion-input} *} |
1238 subsection {* Input events \label{sec:completion-input} *} |
1239 |
1239 |
1240 text {* |
1240 text {* |
1241 FIXME |
1241 Completion is triggered by certain events produced by the user, with |
1242 |
1242 optional delay after keyboard input according to @{system_option |
1243 \paragraph{Explicit completion} is triggered by the keyboard |
1243 jedit_completion_delay}. |
1244 shortcut @{verbatim "C+b"} (action @{action "isabelle.complete"}). |
1244 |
1245 This overrides the original jEdit binding for action @{verbatim |
1245 \begin{description} |
1246 "complete-word"}, but the latter is used as fall-back for |
1246 |
1247 non-Isabelle edit modes. It is also possible to restore the |
1247 \item[Explicit completion] via action @{action_ref "isabelle.complete"} |
|
1248 with keyboard shortcut @{verbatim "C+b"}. This overrides the shortcut for |
|
1249 @{verbatim "complete-word"} in jEdit. It is also possible to restore the |
1248 original jEdit keyboard mapping of @{verbatim "complete-word"} via |
1250 original jEdit keyboard mapping of @{verbatim "complete-word"} via |
1249 \emph{Global Options / Shortcuts}. |
1251 \emph{Global Options / Shortcuts}, and invent a different one for @{action |
1250 |
1252 "isabelle.complete"}. |
1251 Replacement text is inserted immediately into the buffer, unless |
1253 |
1252 ambiguous results demand an explicit popup. |
1254 \item[Explicit spell-checker completion] via @{action_ref |
1253 |
1255 "isabelle.complete-word"}, which is exposed in the jEdit context menu, if |
1254 \paragraph{Implicit completion} is triggered by regular keyboard input |
1256 the mouse points to a word that the spell-checker can complete. |
1255 events during of the editing process in the main jEdit text area (and a few |
1257 |
1256 additional text fields like the ones of the the \emph{Query} panel, see |
1258 \item[Implicit completion] via regular keyboard input of the editor. This |
1257 \secref{sec:query}). Implicit completion depends on on further |
1259 depends on further side-conditions: |
1258 side-conditions: |
|
1259 |
1260 |
1260 \begin{enumerate} |
1261 \begin{enumerate} |
1261 |
1262 |
1262 \item The system option @{system_option_ref jedit_completion} needs to |
1263 \item The system option @{system_option_ref jedit_completion} needs to |
1263 be enabled (default). |
1264 be enabled (default). |
1264 |
1265 |
1265 \item Completion of syntax keywords requires at least 3 relevant |
1266 \item Completion of syntax keywords requires at least 3 relevant |
1266 characters in the text. |
1267 characters in the text. |
1267 |
1268 |
1268 \item The system option @{system_option_ref jedit_completion_delay} |
1269 \item The system option @{system_option_ref jedit_completion_delay} |
1269 determines an additional delay (0.5 by default), before opening a |
1270 determines an additional delay (0.5 by default), before opening a completion |
1270 completion popup. |
1271 popup. The delay gives the prover a chance to provide semantic completion |
|
1272 information, notably the context (\secref{sec:completion-context}). |
1271 |
1273 |
1272 \item The system option @{system_option_ref jedit_completion_immediate} |
1274 \item The system option @{system_option_ref jedit_completion_immediate} |
1273 (disabled by default) controls whether replacement text should be |
1275 (disabled by default) controls whether replacement text should be inserted |
1274 inserted immediately without popup. This is restricted to Isabelle |
1276 immediately without popup, regardless of @{system_option |
1275 symbols and their abbreviations (\secref{sec:symbols}) --- plain |
1277 jedit_completion_delay}. This aggressive mode of completion is restricted to |
1276 keywords always demand a popup for clarity. |
1278 Isabelle symbols and their abbreviations (\secref{sec:symbols}). |
1277 |
1279 |
1278 \item Completion of symbol abbreviations with only one relevant |
1280 \item Completion of symbol abbreviations with only one relevant |
1279 character in the text always enforces an explicit popup, |
1281 character in the text always enforces an explicit popup, |
1280 independently of @{system_option_ref jedit_completion_immediate}. |
1282 regardless of @{system_option_ref jedit_completion_immediate}. |
1281 |
1283 |
1282 \end{enumerate} |
1284 \end{enumerate} |
1283 |
1285 |
1284 In contrast, more aggressive completion works via @{system_option |
1286 \end{description} |
1285 jedit_completion_delay}~@{verbatim "= 0.0"} and @{system_option |
|
1286 jedit_completion_immediate}~@{verbatim "= true"}. Thus the editing |
|
1287 process becomes dependent on the system guessing correctly what the |
|
1288 user had in mind. It requires some practice (and study of the |
|
1289 symbol abbreviation tables) to become productive in this advanced |
|
1290 mode. |
|
1291 *} |
1287 *} |
1292 |
1288 |
1293 |
1289 |
1294 subsection {* Completion popup \label{sec:completion-popup} *} |
1290 subsection {* Completion popup \label{sec:completion-popup} *} |
1295 |
1291 |
1337 |
1333 |
1338 subsection {* Options \label{sec:completion-options} *} |
1334 subsection {* Options \label{sec:completion-options} *} |
1339 |
1335 |
1340 text {* |
1336 text {* |
1341 This is a summary of Isabelle/Scala system options that are relevant for |
1337 This is a summary of Isabelle/Scala system options that are relevant for |
1342 completion. |
1338 completion. They may be configured in \emph{Plugin Options / Isabelle / |
1343 |
1339 General} as usual. |
1344 FIXME |
1340 |
|
1341 \begin{itemize} |
|
1342 |
|
1343 \item @{system_option_def completion_limit} specifies the limit of |
|
1344 name-space entries exposed in semantic completion by the prover. |
|
1345 |
|
1346 \item @{system_option_def jedit_completion} guards implicit completion via |
|
1347 regular jEdit keyboard input events (\secref{sec:completion-input}). |
|
1348 |
|
1349 \item @{system_option_def jedit_completion_context} specifies whether the |
|
1350 language context provided by the prover should be used. Disabling that |
|
1351 option makes completion less ``semantic''. Note that incomplete or broken |
|
1352 input may cause some disagreement of the prover and the user about the |
|
1353 intended language context. |
|
1354 |
|
1355 \item @{system_option_def jedit_completion_delay} FIXME |
|
1356 |
|
1357 \item @{system_option_def jedit_completion_immediate} specifies whether |
|
1358 |
|
1359 \item @{system_option_def jedit_completion_path_ignore} specifies ``glob'' |
|
1360 patterns to ignore in file-system path completion (separated by colons). |
|
1361 |
|
1362 \item @{system_option_def spell_checker} FIXME |
|
1363 |
|
1364 \item @{system_option_def spell_checker_dictionary} FIXME |
|
1365 |
|
1366 \item @{system_option_def spell_checker_elements} FIXME |
|
1367 |
|
1368 \end{itemize} |
1345 *} |
1369 *} |
1346 |
1370 |
1347 |
1371 |
1348 section {* Automatically tried tools \label{sec:auto-tools} *} |
1372 section {* Automatically tried tools \label{sec:auto-tools} *} |
1349 |
1373 |