480 markup is less detailed. *} |
480 markup is less detailed. *} |
481 |
481 |
482 |
482 |
483 section {* Text completion \label{sec:completion} *} |
483 section {* Text completion \label{sec:completion} *} |
484 |
484 |
485 text {* |
485 text {* \paragraph{Completion tables} are determined statically from |
486 Text completion works via some light-weight GUI popup, which is triggered by |
486 the ``outer syntax'' of the underlying edit mode (for theory files |
487 keyboard events during the normal editing process in the main jEdit text |
487 this is the syntax of Isar commands) and specifications of Isabelle |
488 area and a few additional text fields. The popup interprets special keys: |
488 symbols (see also \secref{sec:symbols}). |
489 @{verbatim TAB}, @{verbatim ESCAPE}, @{verbatim UP}, @{verbatim DOWN}, |
489 |
490 @{verbatim PAGE_UP}, @{verbatim PAGE_DOWN}. All other key events are passed |
490 Symbols are completed in backslashed forms, e.g.\ @{verbatim |
491 to the jEdit text area --- this allows to ignore unwanted completions most |
491 "\\"}@{verbatim "forall"} or @{verbatim "\<forall>"} that both produce the |
492 of the time and continue typing quickly. |
492 Isabelle symbol @{text "\<forall>"} in its Unicode rendering.\footnote{The |
493 |
493 extra backslash avoids overlap with keywords of the buffer syntax, |
494 Various Isabelle plugin options control the popup behavior and immediate |
494 and facilitates to produce Isabelle symbols in arbitrary syntactic |
495 insertion into buffer. |
495 contexts.} Alternatively, symbol abbreviations may be used as |
496 |
496 specified in @{file "$ISABELLE_HOME/etc/symbols"}. |
497 Isabelle Symbols are completed in backslashed forms, e.g.\ @{verbatim |
497 |
498 "\\"}@{verbatim "forall"} or @{verbatim "\<forall>"} that both produce the Isabelle |
498 \paragraph{Completion popups} are required in situations of |
499 symbol @{text "\<forall>"} in its Unicode rendering. Alternatively, symbol |
499 ambiguous completion results or where explicit confirmation is |
500 abbreviations may be used as specified in @{file |
500 demanded before inserting completed text into the buffer. |
501 "$ISABELLE_HOME/etc/symbols"}. |
501 |
502 |
502 The popup is some minimally invasive GUI component over the text |
503 \emph{Explicit completion} works via standard jEdit shortcut @{verbatim |
503 area. It interprets special keys @{verbatim TAB}, @{verbatim |
504 "C+b"}, which is remapped to action @{verbatim "isabelle.complete"}, with a |
504 ESCAPE}, @{verbatim UP}, @{verbatim DOWN}, @{verbatim PAGE_UP}, |
505 fall-back on regular @{verbatim "complete-word"} for non-Isabelle buffers. |
505 @{verbatim PAGE_DOWN}, but all other key events are passed to the |
506 |
506 underlying text area. This allows to ignore unwanted completions |
507 \emph{Implicit completion} works via keyboard input on text area, with popup |
507 most of the time and continue typing quickly. |
508 or immediate insertion into buffer. Plain words require at least 3 |
508 |
509 characters to be completed. |
509 The meaning of special keys is as follows: |
510 |
510 |
511 \emph{Immediate completion} means the (unique) replacement text is inserted |
511 \medskip |
512 into the buffer without popup. This mode ignores plain words and requires |
512 \begin{tabular}{ll} |
513 more than one characters for symbol abbreviations. Otherwise it falls back |
513 @{verbatim "TAB"} & select completion \\ |
514 on completion popup. |
514 @{verbatim "ESCAPE"} & dismiss popup \\ |
|
515 @{verbatim "UP"} & move up one item \\ |
|
516 @{verbatim "DOWN"} & move down one item \\ |
|
517 @{verbatim "PAGE_UP"} & move up one page of items \\ |
|
518 @{verbatim "PAGE_DOWN"} & move down one page of items \\ |
|
519 \end{tabular} |
|
520 \medskip |
|
521 |
|
522 Movement within the popup is only active for multiple items. |
|
523 Otherwise the corresponding key event retains its standard meaning |
|
524 within the underlying text area. |
|
525 |
|
526 \paragraph{Explicit completion} is triggered by the keyword shortcut |
|
527 @{verbatim "C+b"} for action @{verbatim "isabelle.complete"}. This |
|
528 overrides the original jEdit action @{verbatim "complete-word"} on |
|
529 that key sequence, but the latter is used as fall-back for |
|
530 non-Isabelle edit modes. It is also possible to restore the |
|
531 original jEdit keyboard mapping of @{verbatim "complete-word"}. |
|
532 |
|
533 Replacement text is inserted immediately into the buffer, unless |
|
534 ambiguous results demand an explicit popup. |
|
535 |
|
536 \paragraph{Implicit completion} is triggered by regular keyboard |
|
537 input events during of the editing process in the main jEdit text |
|
538 area (and a few additional text fields like the search criterium of |
|
539 the Find panel, see \secref{sec:find}). Implicit completion depends |
|
540 on on further side-conditions: |
|
541 |
|
542 \begin{enumerate} |
|
543 |
|
544 \item The system option @{system_option jedit_completion} needs to |
|
545 be enabled (default). |
|
546 |
|
547 \item Completion of syntax keywords requires at least 3 characters |
|
548 in the text. |
|
549 |
|
550 \item The system option @{system_option jedit_completion} determines |
|
551 an additional delay (0.0 by default), before opening a completion |
|
552 popup. |
|
553 |
|
554 \item The system option @{system_option jedit_completion_immediate} |
|
555 (disabled by default) controls whether replacement text should be |
|
556 inserted immediately without popup, if possible. This only works |
|
557 for Isabelle symbols (\secref{sec:symbols}). |
|
558 |
|
559 \item Completion of symbol abbreviations with only 1 character in |
|
560 the text always enforces and explicit popup, independently of |
|
561 @{system_option jedit_completion_immediate}. |
|
562 |
|
563 \end{enumerate} |
|
564 |
|
565 These completion options may be configured in \emph{Plugin Options / |
|
566 Isabelle / General / Completion}. The default is quite moderate in |
|
567 showing occasional popups and refraining from immediate insertion. |
|
568 An additional of e.g.\ 0.3 seconds will make it even less ambitious. |
|
569 |
|
570 A more aggressive configuration is @{system_option |
|
571 jedit_completion_delay}~@{verbatim "= 0.0"} and @{system_option |
|
572 jedit_completion_immediate}~@{verbatim "= true"}. Thus the editing |
|
573 process becomes more dependent on the system guessing correctly what |
|
574 the user had in mind. It requires some practice and study of the |
|
575 symbol abbreviation tables to be productive in this mode. |
|
576 |
|
577 Unintended completions can be reverted by the regular @{verbatim |
|
578 undo} operation of jEdit. When editing embedded languages such as |
|
579 ML works, it is better to disable either @{system_option |
|
580 jedit_completion} or @{system_option jedit_completion_immediate} |
|
581 temporarily. |
515 *} |
582 *} |
516 |
583 |
517 |
584 |
518 section {* Isabelle symbols *} |
585 section {* Isabelle symbols \label{sec:symbols} *} |
519 |
586 |
520 text {* Isabelle sources consist of \emph{symbols} that extend plain |
587 text {* Isabelle sources consist of \emph{symbols} that extend plain |
521 ASCII to allow infinitely many mathematical symbols within the |
588 ASCII to allow infinitely many mathematical symbols within the |
522 formal sources. This works without depending on particular |
589 formal sources. This works without depending on particular |
523 encodings or varying Unicode standards |
590 encodings or varying Unicode standards |