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