author | wenzelm |
Sat, 21 Sep 2013 15:23:31 +0200 | |
changeset 53770 | db362319d766 |
parent 53769 | 036e80175bdd |
child 53771 | 17e93676670b |
permissions | -rw-r--r-- |
53769 | 1 |
theory JEdit |
2 |
imports Base |
|
3 |
begin |
|
4 |
||
5 |
chapter {* Introduction *} |
|
6 |
||
53770
db362319d766
added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents:
53769
diff
changeset
|
7 |
section {* Concepts and terminology *} |
db362319d766
added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents:
53769
diff
changeset
|
8 |
|
53769 | 9 |
text {* FIXME |
10 |
||
11 |
parallel proof checking \cite{Wenzel:2009} \cite{Wenzel:2013:ITP} |
|
12 |
||
53770
db362319d766
added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents:
53769
diff
changeset
|
13 |
asynchronous user interaction \cite{Wenzel:2010}, |
db362319d766
added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents:
53769
diff
changeset
|
14 |
\cite{Wenzel:2012:UITP-EPTCS} |
db362319d766
added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents:
53769
diff
changeset
|
15 |
|
db362319d766
added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents:
53769
diff
changeset
|
16 |
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
|
17 |
\cite{Wenzel:2012} |
db362319d766
added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents:
53769
diff
changeset
|
18 |
|
db362319d766
added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents:
53769
diff
changeset
|
19 |
\begin{description} |
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 |
\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
|
22 |
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
|
23 |
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
|
24 |
that is implemented in Isabelle/ML. |
db362319d766
added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents:
53769
diff
changeset
|
25 |
|
db362319d766
added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents:
53769
diff
changeset
|
26 |
\item [jEdit] is a sophisticated text editor \url{http://www.jedit.org} |
db362319d766
added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents:
53769
diff
changeset
|
27 |
implemented in Java. It is easily extensible by plugins written in any |
db362319d766
added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents:
53769
diff
changeset
|
28 |
language that works on the JVM, e.g.\ Scala. |
db362319d766
added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents:
53769
diff
changeset
|
29 |
|
db362319d766
added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents:
53769
diff
changeset
|
30 |
\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
|
31 |
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
|
32 |
experts alike. |
db362319d766
added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents:
53769
diff
changeset
|
33 |
|
db362319d766
added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents:
53769
diff
changeset
|
34 |
\end{description} |
db362319d766
added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents:
53769
diff
changeset
|
35 |
*} |
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 |
|
db362319d766
added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents:
53769
diff
changeset
|
38 |
section {* The Isabelle/jEdit Prover IDE *} |
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 |
text {* |
db362319d766
added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents:
53769
diff
changeset
|
41 |
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
|
42 |
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
|
43 |
principles. |
db362319d766
added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents:
53769
diff
changeset
|
44 |
|
db362319d766
added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents:
53769
diff
changeset
|
45 |
\begin{itemize} |
53769 | 46 |
|
53770
db362319d766
added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents:
53769
diff
changeset
|
47 |
\item The original jEdit look-and-feel is generally preserved, although |
db362319d766
added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents:
53769
diff
changeset
|
48 |
some default properties have been changed to accommodate Isabelle (e.g. |
db362319d766
added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents:
53769
diff
changeset
|
49 |
the text area font). |
db362319d766
added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents:
53769
diff
changeset
|
50 |
|
db362319d766
added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents:
53769
diff
changeset
|
51 |
\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
|
52 |
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
|
53 |
locking portions of the buffer. |
db362319d766
added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents:
53769
diff
changeset
|
54 |
|
db362319d766
added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents:
53769
diff
changeset
|
55 |
\item Prover feedback works via colors, boxes, squiggly underline, |
db362319d766
added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents:
53769
diff
changeset
|
56 |
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
|
57 |
markup produced by Isabelle in the background. |
db362319d766
added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents:
53769
diff
changeset
|
58 |
|
db362319d766
added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents:
53769
diff
changeset
|
59 |
\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
|
60 |
(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
|
61 |
formal content via tooltips and/or hyperlinks. |
53769 | 62 |
|
53770
db362319d766
added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents:
53769
diff
changeset
|
63 |
\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
|
64 |
independent windows by jEdit, which also allows multiple instances. |
db362319d766
added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents:
53769
diff
changeset
|
65 |
|
db362319d766
added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents:
53769
diff
changeset
|
66 |
\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
|
67 |
the same techniques as in the editor source buffer. |
db362319d766
added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents:
53769
diff
changeset
|
68 |
|
db362319d766
added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents:
53769
diff
changeset
|
69 |
\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
|
70 |
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
|
71 |
Isabelle/Scala. |
db362319d766
added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents:
53769
diff
changeset
|
72 |
|
db362319d766
added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents:
53769
diff
changeset
|
73 |
\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
|
74 |
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
|
75 |
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
|
76 |
|
db362319d766
added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents:
53769
diff
changeset
|
77 |
\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
|
78 |
Isabelle/jEdit, but this requires restart. The new image is provided |
db362319d766
added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents:
53769
diff
changeset
|
79 |
automatically by the Isabelle build process. |
db362319d766
added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents:
53769
diff
changeset
|
80 |
|
db362319d766
added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents:
53769
diff
changeset
|
81 |
\end{itemize} |
53769 | 82 |
*} |
83 |
||
53770
db362319d766
added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents:
53769
diff
changeset
|
84 |
|
db362319d766
added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents:
53769
diff
changeset
|
85 |
chapter {* Prover IDE functionality *} |
db362319d766
added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents:
53769
diff
changeset
|
86 |
|
db362319d766
added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents:
53769
diff
changeset
|
87 |
section {* Isabelle symbols and fonts *} |
db362319d766
added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents:
53769
diff
changeset
|
88 |
|
db362319d766
added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents:
53769
diff
changeset
|
89 |
text {* |
db362319d766
added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents:
53769
diff
changeset
|
90 |
Isabelle supports infinitely many symbols: |
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 |
\medskip |
db362319d766
added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents:
53769
diff
changeset
|
93 |
\begin{tabular}{l} |
db362319d766
added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents:
53769
diff
changeset
|
94 |
@{text "\<alpha>"}, @{text "\<beta>"}, @{text "\<gamma>"}, @{text "\<dots>"} \\ |
db362319d766
added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents:
53769
diff
changeset
|
95 |
@{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
|
96 |
@{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
|
97 |
@{text "\<aleph>"}, @{text "\<triangle>"}, @{text "\<nabla>"}, @{text "\<dots>"} \\ |
db362319d766
added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents:
53769
diff
changeset
|
98 |
@{verbatim "\<foo>"}, @{verbatim "\<bar>"}, @{verbatim "\<baz>"}, @{text "\<dots>"} \\ |
db362319d766
added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents:
53769
diff
changeset
|
99 |
\end{tabular} |
db362319d766
added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents:
53769
diff
changeset
|
100 |
\medskip |
db362319d766
added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents:
53769
diff
changeset
|
101 |
|
db362319d766
added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents:
53769
diff
changeset
|
102 |
A default mapping relates some Isabelle symbols to Unicode points (see |
db362319d766
added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents:
53769
diff
changeset
|
103 |
@{file "~~/etc/symbols"} and @{verbatim |
db362319d766
added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents:
53769
diff
changeset
|
104 |
"$ISABELLE_HOME_USER/etc/symbols"}. |
db362319d766
added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents:
53769
diff
changeset
|
105 |
|
db362319d766
added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents:
53769
diff
changeset
|
106 |
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
|
107 |
on the screen (or printer). |
db362319d766
added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents:
53769
diff
changeset
|
108 |
|
db362319d766
added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents:
53769
diff
changeset
|
109 |
\medskip |
db362319d766
added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents:
53769
diff
changeset
|
110 |
Input methods: |
db362319d766
added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents:
53769
diff
changeset
|
111 |
\begin{enumerate} |
db362319d766
added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents:
53769
diff
changeset
|
112 |
\item use the \emph{Symbols} dockable window |
db362319d766
added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents:
53769
diff
changeset
|
113 |
\item copy/paste from decoded source files |
db362319d766
added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents:
53769
diff
changeset
|
114 |
\item copy/paste from prover output |
db362319d766
added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents:
53769
diff
changeset
|
115 |
\item completion provided by Isabelle plugin, e.g. |
db362319d766
added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents:
53769
diff
changeset
|
116 |
|
db362319d766
added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents:
53769
diff
changeset
|
117 |
\medskip |
db362319d766
added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents:
53769
diff
changeset
|
118 |
\begin{tabular}{lll} |
db362319d766
added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents:
53769
diff
changeset
|
119 |
\textbf{backslash escape} & \textbf{abbreviation} & \textbf{symbol} \\[1ex] |
db362319d766
added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents:
53769
diff
changeset
|
120 |
|
db362319d766
added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents:
53769
diff
changeset
|
121 |
@{verbatim "\\lambda"} & @{verbatim "%"} & @{text "\<lambda>"} \\ |
db362319d766
added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents:
53769
diff
changeset
|
122 |
@{verbatim "\\Rightarrow"} & @{verbatim "=>"} & @{text "\<Rightarrow>"} \\ |
db362319d766
added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents:
53769
diff
changeset
|
123 |
@{verbatim "\\Longrightarrow"} & @{verbatim "==>"} & @{text "\<Longrightarrow>"} \\ |
db362319d766
added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents:
53769
diff
changeset
|
124 |
|
db362319d766
added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents:
53769
diff
changeset
|
125 |
@{verbatim "\\And"} & @{verbatim "!!"} & @{text "\<And>"} \\ |
db362319d766
added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents:
53769
diff
changeset
|
126 |
@{verbatim "\\equiv"} & @{verbatim "=="} & @{text "\<equiv>"} \\ |
db362319d766
added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents:
53769
diff
changeset
|
127 |
|
db362319d766
added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents:
53769
diff
changeset
|
128 |
@{verbatim "\\forall"} & @{verbatim "!"} & @{text "\<forall>"} \\ |
db362319d766
added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents:
53769
diff
changeset
|
129 |
@{verbatim "\\exists"} & @{verbatim "?"} & @{text "\<exists>"} \\ |
db362319d766
added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents:
53769
diff
changeset
|
130 |
@{verbatim "\\longrightarrow"} & @{verbatim "-->"} & @{text "\<longrightarrow>"} \\ |
db362319d766
added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents:
53769
diff
changeset
|
131 |
@{verbatim "\\and"} & @{verbatim "&"} & @{text "\<and>"} \\ |
db362319d766
added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents:
53769
diff
changeset
|
132 |
@{verbatim "\\or"} & @{verbatim "|"} & @{text "\<or>"} \\ |
db362319d766
added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents:
53769
diff
changeset
|
133 |
@{verbatim "\\not"} & @{verbatim "~"} & @{text "\<not>"} \\ |
db362319d766
added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents:
53769
diff
changeset
|
134 |
@{verbatim "\\noteq"} & @{verbatim "~="} & @{text "\<noteq>"} \\ |
db362319d766
added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents:
53769
diff
changeset
|
135 |
@{verbatim "\\in"} & @{verbatim ":"} & @{text "\<in>"} \\ |
db362319d766
added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents:
53769
diff
changeset
|
136 |
@{verbatim "\\notin"} & @{verbatim "~:"} & @{text "\<notin>"} \\ |
db362319d766
added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents:
53769
diff
changeset
|
137 |
\end{tabular} |
db362319d766
added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents:
53769
diff
changeset
|
138 |
|
db362319d766
added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents:
53769
diff
changeset
|
139 |
\end{enumerate} |
db362319d766
added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents:
53769
diff
changeset
|
140 |
|
db362319d766
added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents:
53769
diff
changeset
|
141 |
\paragraph{Notes:} |
db362319d766
added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents:
53769
diff
changeset
|
142 |
\begin{itemize} |
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 |
\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
|
145 |
notation provides ASCII alternatives that often coincide, but deviate |
db362319d766
added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents:
53769
diff
changeset
|
146 |
occasionally. |
db362319d766
added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents:
53769
diff
changeset
|
147 |
|
db362319d766
added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents:
53769
diff
changeset
|
148 |
\item Generic jEdit abbreviations or plugins perform similar source |
db362319d766
added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents:
53769
diff
changeset
|
149 |
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
|
150 |
sequences coincide with the symbol mapping. |
db362319d766
added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents:
53769
diff
changeset
|
151 |
|
db362319d766
added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents:
53769
diff
changeset
|
152 |
\item Raw Unicode characters within prover source files should be |
db362319d766
added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents:
53769
diff
changeset
|
153 |
restricted to informal parts, e.g. to write text in non-latin alphabets. |
db362319d766
added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents:
53769
diff
changeset
|
154 |
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
|
155 |
|
db362319d766
added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents:
53769
diff
changeset
|
156 |
\end{itemize} |
db362319d766
added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents:
53769
diff
changeset
|
157 |
|
db362319d766
added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents:
53769
diff
changeset
|
158 |
\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
|
159 |
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
|
160 |
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
|
161 |
\emph{Symbols} dockable window or keyboard shortcuts. |
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 |
\medskip |
db362319d766
added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents:
53769
diff
changeset
|
164 |
\begin{tabular}{lll} |
db362319d766
added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents:
53769
diff
changeset
|
165 |
\textbf{symbol} & style & keyboard shortcure \\ |
db362319d766
added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents:
53769
diff
changeset
|
166 |
@{verbatim "\<sup>"} & superscript & @{verbatim "C+e UP"} \\ |
db362319d766
added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents:
53769
diff
changeset
|
167 |
@{verbatim "\<sub>"} & subscript & @{verbatim "C+e DOWN"} \\ |
db362319d766
added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents:
53769
diff
changeset
|
168 |
@{verbatim "\<bold>"} & bold face & @{verbatim "C+e RIGHT"} \\ |
db362319d766
added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents:
53769
diff
changeset
|
169 |
& reset & @{verbatim "C+e LEFT"} \\ |
db362319d766
added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents:
53769
diff
changeset
|
170 |
\end{tabular} |
db362319d766
added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents:
53769
diff
changeset
|
171 |
*} |
db362319d766
added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents:
53769
diff
changeset
|
172 |
|
db362319d766
added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents:
53769
diff
changeset
|
173 |
|
db362319d766
added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents:
53769
diff
changeset
|
174 |
section {* Text completion *} |
53769 | 175 |
|
176 |
text {* FIXME *} |
|
177 |
||
53770
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 |
chapter {* Known problems and workarounds *} |
db362319d766
added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents:
53769
diff
changeset
|
180 |
|
db362319d766
added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents:
53769
diff
changeset
|
181 |
text {* |
db362319d766
added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents:
53769
diff
changeset
|
182 |
\begin{itemize} |
db362319d766
added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents:
53769
diff
changeset
|
183 |
|
db362319d766
added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents:
53769
diff
changeset
|
184 |
\item \textbf{Problem:} Keyboard shortcuts @{verbatim "C+PLUS"} and |
db362319d766
added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents:
53769
diff
changeset
|
185 |
@{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
|
186 |
platform details and national keyboards. |
db362319d766
added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents:
53769
diff
changeset
|
187 |
|
db362319d766
added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents:
53769
diff
changeset
|
188 |
\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
|
189 |
jEdit Shortcuts options dialog. |
db362319d766
added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents:
53769
diff
changeset
|
190 |
|
db362319d766
added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents:
53769
diff
changeset
|
191 |
\item \textbf{Problem:} Lack of dependency management for auxiliary files |
db362319d766
added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents:
53769
diff
changeset
|
192 |
that contribute to a theory (e.g. @{command ML_file}). |
db362319d766
added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents:
53769
diff
changeset
|
193 |
|
db362319d766
added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents:
53769
diff
changeset
|
194 |
\textbf{Workaround:} Re-load files manually within the prover. |
db362319d766
added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents:
53769
diff
changeset
|
195 |
|
db362319d766
added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents:
53769
diff
changeset
|
196 |
\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
|
197 |
global side-effects, like writing a physical file. |
db362319d766
added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents:
53769
diff
changeset
|
198 |
|
db362319d766
added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents:
53769
diff
changeset
|
199 |
\textbf{Workaround:} Avoid such commands. |
db362319d766
added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents:
53769
diff
changeset
|
200 |
|
db362319d766
added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents:
53769
diff
changeset
|
201 |
\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
|
202 |
collection of theories. |
db362319d766
added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents:
53769
diff
changeset
|
203 |
|
db362319d766
added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents:
53769
diff
changeset
|
204 |
\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
|
205 |
situation. |
db362319d766
added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents:
53769
diff
changeset
|
206 |
|
db362319d766
added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents:
53769
diff
changeset
|
207 |
\item \textbf{Problem:} Linux: some desktop environments with extreme |
db362319d766
added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents:
53769
diff
changeset
|
208 |
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
|
209 |
focus. |
db362319d766
added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents:
53769
diff
changeset
|
210 |
|
db362319d766
added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents:
53769
diff
changeset
|
211 |
\textbf{Workaround:} Disable such effects. |
db362319d766
added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents:
53769
diff
changeset
|
212 |
|
db362319d766
added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents:
53769
diff
changeset
|
213 |
\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
|
214 |
``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
|
215 |
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
|
216 |
``@{verbatim awesome}'' or ``@{verbatim xmonad}''. |
db362319d766
added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents:
53769
diff
changeset
|
217 |
|
db362319d766
added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents:
53769
diff
changeset
|
218 |
\textbf{Workaround:} Use regular re-parenting window manager. |
db362319d766
added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents:
53769
diff
changeset
|
219 |
|
db362319d766
added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents:
53769
diff
changeset
|
220 |
\item \textbf{Problem:} Mac OS X: the native MacOSX plugin for jEdit tends |
db362319d766
added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents:
53769
diff
changeset
|
221 |
to be disruptive and is off by default. Enabling it might or might not |
db362319d766
added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents:
53769
diff
changeset
|
222 |
improve the user experience. |
db362319d766
added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents:
53769
diff
changeset
|
223 |
|
db362319d766
added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents:
53769
diff
changeset
|
224 |
\textbf{Workaround:} Disable @{verbatim MacOSX} plugin. |
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:} 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
|
227 |
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
|
228 |
although with a small risk of instabilities. |
db362319d766
added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents:
53769
diff
changeset
|
229 |
|
db362319d766
added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents:
53769
diff
changeset
|
230 |
\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
|
231 |
|
db362319d766
added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents:
53769
diff
changeset
|
232 |
\end{itemize} |
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 |
|
53769 | 235 |
end |