7 chapter \<open>Introduction\<close> |
7 chapter \<open>Introduction\<close> |
8 |
8 |
9 section \<open>Concepts and terminology\<close> |
9 section \<open>Concepts and terminology\<close> |
10 |
10 |
11 text \<open> |
11 text \<open> |
12 Isabelle/jEdit is a Prover IDE that integrates \<^emph>\<open>parallel proof |
12 Isabelle/jEdit is a Prover IDE that integrates \<^emph>\<open>parallel proof checking\<close> |
13 checking\<close> @{cite "Wenzel:2009" and "Wenzel:2013:ITP"} with |
13 @{cite "Wenzel:2009" and "Wenzel:2013:ITP"} with \<^emph>\<open>asynchronous user |
14 \<^emph>\<open>asynchronous user interaction\<close> @{cite "Wenzel:2010" and |
14 interaction\<close> @{cite "Wenzel:2010" and "Wenzel:2012:UITP-EPTCS" and |
15 "Wenzel:2012:UITP-EPTCS" and "Wenzel:2014:ITP-PIDE" and "Wenzel:2014:UITP"}, |
15 "Wenzel:2014:ITP-PIDE" and "Wenzel:2014:UITP"}, based on a document-oriented |
16 based on a document-oriented approach to \<^emph>\<open>continuous proof processing\<close> |
16 approach to \<^emph>\<open>continuous proof processing\<close> @{cite "Wenzel:2011:CICM" and |
17 @{cite "Wenzel:2011:CICM" and "Wenzel:2012"}. Many concepts and system |
17 "Wenzel:2012"}. Many concepts and system components are fit together in |
18 components are fit together in order to make this work. The main building |
18 order to make this work. The main building blocks are as follows. |
19 blocks are as follows. |
19 |
20 |
20 \<^descr>[PIDE] is a general framework for Prover IDEs based on Isabelle/Scala. It |
21 \<^descr>[PIDE] is a general framework for Prover IDEs based on Isabelle/Scala. |
21 is built around a concept of parallel and asynchronous document |
22 It is built around a concept of parallel and asynchronous document |
22 processing, which is supported natively by the parallel proof engine that |
23 processing, which is supported natively by the parallel proof engine that is |
23 is implemented in Isabelle/ML. The traditional prover command loop is |
24 implemented in Isabelle/ML. The traditional prover command loop is given up; |
24 given up; instead there is direct support for editing of source text, with |
25 instead there is direct support for editing of source text, with rich formal |
25 rich formal markup for GUI rendering. |
26 markup for GUI rendering. |
26 |
27 |
27 \<^descr>[Isabelle/ML] is the implementation and extension language of Isabelle, |
28 \<^descr>[Isabelle/ML] is the implementation and extension language of |
28 see also @{cite "isabelle-implementation"}. It is integrated into the |
29 Isabelle, see also @{cite "isabelle-implementation"}. It is integrated |
29 logical context of Isabelle/Isar and allows to manipulate logical entities |
30 into the logical context of Isabelle/Isar and allows to manipulate |
30 directly. Arbitrary add-on tools may be implemented for object-logics such |
31 logical entities directly. Arbitrary add-on tools may be implemented |
31 as Isabelle/HOL. |
32 for object-logics such as Isabelle/HOL. |
32 |
33 |
33 \<^descr>[Isabelle/Scala] is the system programming language of Isabelle. It |
34 \<^descr>[Isabelle/Scala] is the system programming language of |
34 extends the pure logical environment of Isabelle/ML towards the ``real |
35 Isabelle. It extends the pure logical environment of Isabelle/ML |
35 world'' of graphical user interfaces, text editors, IDE frameworks, web |
36 towards the ``real world'' of graphical user interfaces, text |
36 services etc. Special infrastructure allows to transfer algebraic |
37 editors, IDE frameworks, web services etc. Special infrastructure |
37 datatypes and formatted text easily between ML and Scala, using |
38 allows to transfer algebraic datatypes and formatted text easily |
38 asynchronous protocol commands. |
39 between ML and Scala, using asynchronous protocol commands. |
39 |
40 |
40 \<^descr>[jEdit] is a sophisticated text editor implemented in Java.\<^footnote>\<open>@{url |
41 \<^descr>[jEdit] is a sophisticated text editor implemented in |
41 "http://www.jedit.org"}\<close> It is easily extensible by plugins written in |
42 Java.\<^footnote>\<open>@{url "http://www.jedit.org"}\<close> It is easily extensible |
42 languages that work on the JVM, e.g.\ Scala\<^footnote>\<open>@{url |
43 by plugins written in languages that work on the JVM, e.g.\ |
43 "http://www.scala-lang.org"}\<close>. |
44 Scala\<^footnote>\<open>@{url "http://www.scala-lang.org"}\<close>. |
44 |
45 |
45 \<^descr>[Isabelle/jEdit] is the main example application of the PIDE framework |
46 \<^descr>[Isabelle/jEdit] is the main example application of the PIDE |
46 and the default user-interface for Isabelle. It targets both beginners and |
47 framework and the default user-interface for Isabelle. It targets |
47 experts. Technically, Isabelle/jEdit combines a slightly modified version |
48 both beginners and experts. Technically, Isabelle/jEdit combines a |
48 of the jEdit code base with a special plugin for Isabelle, integrated as |
49 slightly modified version of the jEdit code base with a special |
49 standalone application for the main operating system platforms: Linux, |
50 plugin for Isabelle, integrated as standalone application for the |
50 Windows, Mac OS X. |
51 main operating system platforms: Linux, Windows, Mac OS X. |
51 |
52 |
52 The subtle differences of Isabelle/ML versus Standard ML, Isabelle/Scala |
53 |
53 versus Scala, Isabelle/jEdit versus jEdit need to be taken into account when |
54 The subtle differences of Isabelle/ML versus Standard ML, |
54 discussing any of these PIDE building blocks in public forums, mailing |
55 Isabelle/Scala versus Scala, Isabelle/jEdit versus jEdit need to be |
55 lists, or even scientific publications. |
56 taken into account when discussing any of these PIDE building blocks |
|
57 in public forums, mailing lists, or even scientific publications. |
|
58 \<close> |
56 \<close> |
59 |
57 |
60 |
58 |
61 section \<open>The Isabelle/jEdit Prover IDE\<close> |
59 section \<open>The Isabelle/jEdit Prover IDE\<close> |
62 |
60 |
71 |
69 |
72 Isabelle/jEdit (\figref{fig:isabelle-jedit}) consists of some plugins for |
70 Isabelle/jEdit (\figref{fig:isabelle-jedit}) consists of some plugins for |
73 the jEdit text editor, while preserving its general look-and-feel as far as |
71 the jEdit text editor, while preserving its general look-and-feel as far as |
74 possible. The main plugin is called ``Isabelle'' and has its own menu |
72 possible. The main plugin is called ``Isabelle'' and has its own menu |
75 \<^emph>\<open>Plugins~/ Isabelle\<close> with access to several panels (see also |
73 \<^emph>\<open>Plugins~/ Isabelle\<close> with access to several panels (see also |
76 \secref{sec:dockables}), as well as \<^emph>\<open>Plugins~/ Plugin Options~/ |
74 \secref{sec:dockables}), as well as \<^emph>\<open>Plugins~/ Plugin Options~/ Isabelle\<close> |
77 Isabelle\<close> (see also \secref{sec:options}). |
75 (see also \secref{sec:options}). |
78 |
76 |
79 The options allow to specify a logic session name --- the same selector is |
77 The options allow to specify a logic session name --- the same selector is |
80 accessible in the \<^emph>\<open>Theories\<close> panel (\secref{sec:theories}). On |
78 accessible in the \<^emph>\<open>Theories\<close> panel (\secref{sec:theories}). On application |
81 application startup, the selected logic session image is provided |
79 startup, the selected logic session image is provided automatically by the |
82 automatically by the Isabelle build tool @{cite "isabelle-system"}: if it is |
80 Isabelle build tool @{cite "isabelle-system"}: if it is absent or outdated |
83 absent or outdated wrt.\ its sources, the build process updates it before |
81 wrt.\ its sources, the build process updates it before entering the Prover |
84 entering the Prover IDE. Change of the logic session within Isabelle/jEdit |
82 IDE. Change of the logic session within Isabelle/jEdit requires a restart of |
85 requires a restart of the whole application. |
83 the whole application. |
86 |
84 |
87 \<^medskip> |
85 \<^medskip> |
88 The main job of the Prover IDE is to manage sources and their |
86 The main job of the Prover IDE is to manage sources and their changes, |
89 changes, taking the logical structure as a formal document into account (see |
87 taking the logical structure as a formal document into account (see also |
90 also \secref{sec:document-model}). The editor and the prover are connected |
88 \secref{sec:document-model}). The editor and the prover are connected |
91 asynchronously in a lock-free manner. The prover is free to organize the |
89 asynchronously in a lock-free manner. The prover is free to organize the |
92 checking of the formal text in parallel on multiple cores, and provides |
90 checking of the formal text in parallel on multiple cores, and provides |
93 feedback via markup, which is rendered in the editor via colors, boxes, |
91 feedback via markup, which is rendered in the editor via colors, boxes, |
94 squiggly underlines, hyperlinks, popup windows, icons, clickable output etc. |
92 squiggly underlines, hyperlinks, popup windows, icons, clickable output etc. |
95 |
93 |
96 Using the mouse together with the modifier key \<^verbatim>\<open>CONTROL\<close> (Linux, |
94 Using the mouse together with the modifier key \<^verbatim>\<open>CONTROL\<close> (Linux, Windows) |
97 Windows) or \<^verbatim>\<open>COMMAND\<close> (Mac OS X) exposes additional formal content |
95 or \<^verbatim>\<open>COMMAND\<close> (Mac OS X) exposes additional formal content via tooltips |
98 via tooltips and/or hyperlinks (see also \secref{sec:tooltips-hyperlinks}). |
96 and/or hyperlinks (see also \secref{sec:tooltips-hyperlinks}). Output (in |
99 Output (in popups etc.) may be explored recursively, using the same |
97 popups etc.) may be explored recursively, using the same techniques as in |
100 techniques as in the editor source buffer. |
98 the editor source buffer. |
101 |
99 |
102 Thus the Prover IDE gives an impression of direct access to formal content |
100 Thus the Prover IDE gives an impression of direct access to formal content |
103 of the prover within the editor, but in reality only certain aspects are |
101 of the prover within the editor, but in reality only certain aspects are |
104 exposed, according to the possibilities of the prover and its many add-on |
102 exposed, according to the possibilities of the prover and its many add-on |
105 tools. |
103 tools. |
127 |
124 |
128 |
125 |
129 subsection \<open>Plugins\<close> |
126 subsection \<open>Plugins\<close> |
130 |
127 |
131 text \<open> |
128 text \<open> |
132 The \<^emph>\<open>Plugin Manager\<close> of jEdit allows to augment editor functionality by |
129 The \<^emph>\<open>Plugin Manager\<close> of jEdit allows to augment editor functionality by JVM |
133 JVM modules (jars) that are provided by the central plugin repository, which |
130 modules (jars) that are provided by the central plugin repository, which is |
134 is accessible via various mirror sites. |
131 accessible via various mirror sites. |
135 |
132 |
136 Connecting to the plugin server-infrastructure of the jEdit project allows |
133 Connecting to the plugin server-infrastructure of the jEdit project allows |
137 to update bundled plugins or to add further functionality. This needs to be |
134 to update bundled plugins or to add further functionality. This needs to be |
138 done with the usual care for such an open bazaar of contributions. Arbitrary |
135 done with the usual care for such an open bazaar of contributions. Arbitrary |
139 combinations of add-on features are apt to cause problems. It is advisable |
136 combinations of add-on features are apt to cause problems. It is advisable |
140 to start with the default configuration of Isabelle/jEdit and develop some |
137 to start with the default configuration of Isabelle/jEdit and develop some |
141 understanding how it is supposed to work, before loading additional plugins |
138 understanding how it is supposed to work, before loading additional plugins |
142 at a grand scale. |
139 at a grand scale. |
143 |
140 |
144 \<^medskip> |
141 \<^medskip> |
145 The main \<^emph>\<open>Isabelle\<close> plugin is an integral part of |
142 The main \<^emph>\<open>Isabelle\<close> plugin is an integral part of Isabelle/jEdit and needs |
146 Isabelle/jEdit and needs to remain active at all times! A few additional |
143 to remain active at all times! A few additional plugins are bundled with |
147 plugins are bundled with Isabelle/jEdit for convenience or out of necessity, |
144 Isabelle/jEdit for convenience or out of necessity, notably \<^emph>\<open>Console\<close> with |
148 notably \<^emph>\<open>Console\<close> with its Isabelle/Scala sub-plugin |
145 its Isabelle/Scala sub-plugin (\secref{sec:scala-console}) and \<^emph>\<open>SideKick\<close> |
149 (\secref{sec:scala-console}) and \<^emph>\<open>SideKick\<close> with some Isabelle-specific |
146 with some Isabelle-specific parsers for document tree structure |
150 parsers for document tree structure (\secref{sec:sidekick}). The |
147 (\secref{sec:sidekick}). The \<^emph>\<open>Navigator\<close> plugin is particularly important |
151 \<^emph>\<open>Navigator\<close> plugin is particularly important for hyperlinks within the |
148 for hyperlinks within the formal document-model |
152 formal document-model (\secref{sec:tooltips-hyperlinks}). Further plugins |
149 (\secref{sec:tooltips-hyperlinks}). Further plugins (e.g.\ \<^emph>\<open>ErrorList\<close>, |
153 (e.g.\ \<^emph>\<open>ErrorList\<close>, \<^emph>\<open>Code2HTML\<close>) are included to saturate the |
150 \<^emph>\<open>Code2HTML\<close>) are included to saturate the dependencies of bundled plugins, |
154 dependencies of bundled plugins, but have no particular use in |
151 but have no particular use in Isabelle/jEdit. |
155 Isabelle/jEdit. |
|
156 \<close> |
152 \<close> |
157 |
153 |
158 |
154 |
159 subsection \<open>Options \label{sec:options}\<close> |
155 subsection \<open>Options \label{sec:options}\<close> |
160 |
156 |
161 text \<open>Both jEdit and Isabelle have distinctive management of |
157 text \<open> |
162 persistent options. |
158 Both jEdit and Isabelle have distinctive management of persistent options. |
163 |
159 |
164 Regular jEdit options are accessible via the dialogs \<^emph>\<open>Utilities~/ |
160 Regular jEdit options are accessible via the dialogs \<^emph>\<open>Utilities~/ Global |
165 Global Options\<close> or \<^emph>\<open>Plugins~/ Plugin Options\<close>, with a second chance to |
161 Options\<close> or \<^emph>\<open>Plugins~/ Plugin Options\<close>, with a second chance to flip the |
166 flip the two within the central options dialog. Changes are stored in |
162 two within the central options dialog. Changes are stored in |
167 @{file_unchecked "$ISABELLE_HOME_USER/jedit/properties"} and |
163 @{file_unchecked "$ISABELLE_HOME_USER/jedit/properties"} and |
168 @{file_unchecked "$ISABELLE_HOME_USER/jedit/keymaps"}. |
164 @{file_unchecked "$ISABELLE_HOME_USER/jedit/keymaps"}. |
169 |
165 |
170 Isabelle system options are managed by Isabelle/Scala and changes are stored |
166 Isabelle system options are managed by Isabelle/Scala and changes are stored |
171 in @{file_unchecked "$ISABELLE_HOME_USER/etc/preferences"}, independently of |
167 in @{file_unchecked "$ISABELLE_HOME_USER/etc/preferences"}, independently of |
172 other jEdit properties. See also @{cite "isabelle-system"}, especially the |
168 other jEdit properties. See also @{cite "isabelle-system"}, especially the |
173 coverage of sessions and command-line tools like @{tool build} or @{tool |
169 coverage of sessions and command-line tools like @{tool build} or @{tool |
174 options}. |
170 options}. |
175 |
171 |
176 Those Isabelle options that are declared as \<^bold>\<open>public\<close> are configurable |
172 Those Isabelle options that are declared as \<^bold>\<open>public\<close> are configurable in |
177 in Isabelle/jEdit via \<^emph>\<open>Plugin Options~/ Isabelle~/ General\<close>. Moreover, |
173 Isabelle/jEdit via \<^emph>\<open>Plugin Options~/ Isabelle~/ General\<close>. Moreover, there |
178 there are various options for rendering of document content, which are |
174 are various options for rendering of document content, which are |
179 configurable via \<^emph>\<open>Plugin Options~/ Isabelle~/ Rendering\<close>. Thus |
175 configurable via \<^emph>\<open>Plugin Options~/ Isabelle~/ Rendering\<close>. Thus \<^emph>\<open>Plugin |
180 \<^emph>\<open>Plugin Options~/ Isabelle\<close> in jEdit provides a view on a subset of |
176 Options~/ Isabelle\<close> in jEdit provides a view on a subset of Isabelle system |
181 Isabelle system options. Note that some of these options affect general |
177 options. Note that some of these options affect general parameters that are |
182 parameters that are relevant outside Isabelle/jEdit as well, e.g.\ |
178 relevant outside Isabelle/jEdit as well, e.g.\ @{system_option threads} or |
183 @{system_option threads} or @{system_option parallel_proofs} for the |
179 @{system_option parallel_proofs} for the Isabelle build tool @{cite |
184 Isabelle build tool @{cite "isabelle-system"}, but it is possible to use the |
180 "isabelle-system"}, but it is possible to use the settings variable |
185 settings variable @{setting ISABELLE_BUILD_OPTIONS} to change defaults for |
181 @{setting ISABELLE_BUILD_OPTIONS} to change defaults for batch builds |
186 batch builds without affecting Isabelle/jEdit. |
182 without affecting Isabelle/jEdit. |
187 |
183 |
188 The jEdit action @{action_def isabelle.options} opens the options dialog for |
184 The jEdit action @{action_def isabelle.options} opens the options dialog for |
189 the Isabelle plugin; it can be mapped to editor GUI elements as usual. |
185 the Isabelle plugin; it can be mapped to editor GUI elements as usual. |
190 |
186 |
191 \<^medskip> |
187 \<^medskip> |
192 Options are usually loaded on startup and saved on shutdown of |
188 Options are usually loaded on startup and saved on shutdown of |
193 Isabelle/jEdit. Editing the machine-generated @{file_unchecked |
189 Isabelle/jEdit. Editing the machine-generated @{file_unchecked |
194 "$ISABELLE_HOME_USER/jedit/properties"} or @{file_unchecked |
190 "$ISABELLE_HOME_USER/jedit/properties"} or @{file_unchecked |
195 "$ISABELLE_HOME_USER/etc/preferences"} manually while the application is |
191 "$ISABELLE_HOME_USER/etc/preferences"} manually while the application is |
196 running is likely to cause surprise due to lost update!\<close> |
192 running is likely to cause surprise due to lost update! |
|
193 \<close> |
197 |
194 |
198 |
195 |
199 subsection \<open>Keymaps\<close> |
196 subsection \<open>Keymaps\<close> |
200 |
197 |
201 text \<open>Keyboard shortcuts used to be managed as jEdit properties in |
198 text \<open> |
202 the past, but recent versions (2013) have a separate concept of |
199 Keyboard shortcuts used to be managed as jEdit properties in the past, but |
203 \<^emph>\<open>keymap\<close> that is configurable via \<^emph>\<open>Global Options~/ |
200 recent versions (2013) have a separate concept of \<^emph>\<open>keymap\<close> that is |
204 Shortcuts\<close>. The \<^verbatim>\<open>imported\<close> keymap is derived from the |
201 configurable via \<^emph>\<open>Global Options~/ Shortcuts\<close>. The \<^verbatim>\<open>imported\<close> keymap is |
205 initial environment of properties that is available at the first |
202 derived from the initial environment of properties that is available at the |
206 start of the editor; afterwards the keymap file takes precedence. |
203 first start of the editor; afterwards the keymap file takes precedence. |
207 |
204 |
208 This is relevant for Isabelle/jEdit due to various fine-tuning of default |
205 This is relevant for Isabelle/jEdit due to various fine-tuning of default |
209 properties, and additional keyboard shortcuts for Isabelle-specific |
206 properties, and additional keyboard shortcuts for Isabelle-specific |
210 functionality. Users may change their keymap later, but need to copy some |
207 functionality. Users may change their keymap later, but need to copy some |
211 keyboard shortcuts manually (see also @{file_unchecked |
208 keyboard shortcuts manually (see also @{file_unchecked |
212 "$ISABELLE_HOME_USER/jedit/keymaps"} versus \<^verbatim>\<open>shortcut\<close> properties |
209 "$ISABELLE_HOME_USER/jedit/keymaps"} versus \<^verbatim>\<open>shortcut\<close> properties in @{file |
213 in @{file "$ISABELLE_HOME/src/Tools/jEdit/src/jEdit.props"}). |
210 "$ISABELLE_HOME/src/Tools/jEdit/src/jEdit.props"}). |
214 \<close> |
211 \<close> |
215 |
212 |
216 |
213 |
217 section \<open>Command-line invocation \label{sec:command-line}\<close> |
214 section \<open>Command-line invocation \label{sec:command-line}\<close> |
218 |
215 |
281 \secref{sec:problems}). |
277 \secref{sec:problems}). |
282 |
278 |
283 Isabelle/jEdit enables platform-specific look-and-feel by default as |
279 Isabelle/jEdit enables platform-specific look-and-feel by default as |
284 follows. |
280 follows. |
285 |
281 |
286 \<^descr>[Linux:] The platform-independent \<^emph>\<open>Metal\<close> is used by |
282 \<^descr>[Linux:] The platform-independent \<^emph>\<open>Metal\<close> is used by default. |
287 default. |
283 |
288 |
284 \<^emph>\<open>GTK+\<close> also works under the side-condition that the overall GTK theme is |
289 \<^emph>\<open>GTK+\<close> also works under the side-condition that the overall GTK theme |
285 selected in a Swing-friendly way.\<^footnote>\<open>GTK support in Java/Swing was once |
290 is selected in a Swing-friendly way.\<^footnote>\<open>GTK support in Java/Swing was |
286 marketed aggressively by Sun, but never quite finished. Today (2015) it is |
291 once marketed aggressively by Sun, but never quite finished. Today (2015) it |
287 lagging behind further development of Swing and GTK. The graphics |
292 is lagging behind further development of Swing and GTK. The graphics |
288 rendering performance can be worse than for other Swing look-and-feels. |
293 rendering performance can be worse than for other Swing look-and-feels. |
289 Nonetheless it has its uses for displays with very high resolution (such |
294 Nonetheless it has its uses for displays with very high resolution (such as |
290 as ``4K'' or ``UHD'' models), because the rendering by the external |
295 ``4K'' or ``UHD'' models), because the rendering by the external library is |
291 library is subject to global system settings for font scaling.\<close> |
296 subject to global system settings for font scaling.\<close> |
292 |
297 |
293 \<^descr>[Windows:] Regular \<^emph>\<open>Windows\<close> is used by default, but \<^emph>\<open>Windows Classic\<close> |
298 \<^descr>[Windows:] Regular \<^emph>\<open>Windows\<close> is used by default, but |
294 also works. |
299 \<^emph>\<open>Windows Classic\<close> also works. |
295 |
300 |
296 \<^descr>[Mac OS X:] Regular \<^emph>\<open>Mac OS X\<close> is used by default. |
301 \<^descr>[Mac OS X:] Regular \<^emph>\<open>Mac OS X\<close> is used by default. |
297 |
302 |
298 The bundled \<^emph>\<open>MacOSX\<close> plugin provides various functions that are expected |
303 The bundled \<^emph>\<open>MacOSX\<close> plugin provides various functions that are |
299 from applications on that particular platform: quit from menu or dock, |
304 expected from applications on that particular platform: quit from menu or |
300 preferences menu, drag-and-drop of text files on the application, |
305 dock, preferences menu, drag-and-drop of text files on the application, |
301 full-screen mode for main editor windows. It is advisable to have the |
306 full-screen mode for main editor windows. It is advisable to have the |
302 \<^emph>\<open>MacOSX\<close> plugin enabled all the time on that platform. |
307 \<^emph>\<open>MacOSX\<close> plugin enabled all the time on that platform. |
303 |
308 |
304 Users may experiment with different look-and-feels, but need to keep in mind |
309 |
305 that this extra variance of GUI functionality is unlikely to work in |
310 Users may experiment with different look-and-feels, but need to keep |
306 arbitrary combinations. The platform-independent \<^emph>\<open>Metal\<close> and \<^emph>\<open>Nimbus\<close> |
311 in mind that this extra variance of GUI functionality is unlikely to |
307 should always work. The historic \<^emph>\<open>CDE/Motif\<close> should be ignored. |
312 work in arbitrary combinations. The platform-independent |
308 |
313 \<^emph>\<open>Metal\<close> and \<^emph>\<open>Nimbus\<close> should always work. The historic |
309 After changing the look-and-feel in \<^emph>\<open>Global Options~/ Appearance\<close>, it is |
314 \<^emph>\<open>CDE/Motif\<close> should be ignored. |
310 advisable to restart Isabelle/jEdit in order to take full effect. |
315 |
|
316 After changing the look-and-feel in \<^emph>\<open>Global Options~/ |
|
317 Appearance\<close>, it is advisable to restart Isabelle/jEdit in order to |
|
318 take full effect. |
|
319 \<close> |
311 \<close> |
320 |
312 |
321 |
313 |
322 subsection \<open>Displays with very high resolution \label{sec:hdpi}\<close> |
314 subsection \<open>Displays with very high resolution \label{sec:hdpi}\<close> |
323 |
315 |
324 text \<open> |
316 text \<open> |
325 Many years ago, displays with $1024 \times 768$ or $1280 \times 1024$ pixels |
317 Many years ago, displays with $1024 \times 768$ or $1280 \times 1024$ pixels |
326 were considered ``high resolution'' and bitmap fonts with 12 or 14 pixels as |
318 were considered ``high resolution'' and bitmap fonts with 12 or 14 pixels as |
327 adequate for text rendering. Today (2015), we routinely see ``Full HD'' |
319 adequate for text rendering. Today (2015), we routinely see ``Full HD'' |
328 monitors at $1920 \times 1080$ pixels, and occasionally ``Ultra HD'' at |
320 monitors at $1920 \times 1080$ pixels, and occasionally ``Ultra HD'' at |
329 $3840 \times 2160$ or more, but GUI rendering did not really progress |
321 $3840 \times 2160$ or more, but GUI rendering did not really progress beyond |
330 beyond the old standards. |
322 the old standards. |
331 |
323 |
332 Isabelle/jEdit defaults are a compromise for reasonable out-of-the box |
324 Isabelle/jEdit defaults are a compromise for reasonable out-of-the box |
333 results on common platforms and medium resolution displays (e.g.\ the ``Full |
325 results on common platforms and medium resolution displays (e.g.\ the ``Full |
334 HD'' category). Subsequently there are further hints to improve on that. |
326 HD'' category). Subsequently there are further hints to improve on that. |
335 |
327 |
336 \<^medskip> |
328 \<^medskip> |
337 The \<^bold>\<open>operating-system platform\<close> usually provides some |
329 The \<^bold>\<open>operating-system platform\<close> usually provides some configuration for |
338 configuration for global scaling of text fonts, e.g.\ $120\%$--$250\%$ on |
330 global scaling of text fonts, e.g.\ $120\%$--$250\%$ on Windows. Changing |
339 Windows. Changing that only has a partial effect on GUI rendering; |
331 that only has a partial effect on GUI rendering; satisfactory display |
340 satisfactory display quality requires further adjustments. |
332 quality requires further adjustments. |
341 |
333 |
342 \<^medskip> |
334 \<^medskip> |
343 The Isabelle/jEdit \<^bold>\<open>application\<close> and its plugins provide |
335 The Isabelle/jEdit \<^bold>\<open>application\<close> and its plugins provide various font |
344 various font properties that are summarized below. |
336 properties that are summarized below. |
345 |
337 |
346 \<^item> \<^emph>\<open>Global Options / Text Area / Text font\<close>: the main text area |
338 \<^item> \<^emph>\<open>Global Options / Text Area / Text font\<close>: the main text area font, |
347 font, which is also used as reference point for various derived font sizes, |
339 which is also used as reference point for various derived font sizes, |
348 e.g.\ the Output panel (\secref{sec:output}). |
340 e.g.\ the Output panel (\secref{sec:output}). |
349 |
341 |
350 \<^item> \<^emph>\<open>Global Options / Gutter / Gutter font\<close>: the font for the gutter |
342 \<^item> \<^emph>\<open>Global Options / Gutter / Gutter font\<close>: the font for the gutter area |
351 area left of the main text area, e.g.\ relevant for display of line numbers |
343 left of the main text area, e.g.\ relevant for display of line numbers |
352 (disabled by default). |
344 (disabled by default). |
353 |
345 |
354 \<^item> \<^emph>\<open>Global Options / Appearance / Button, menu and label font\<close> as |
346 \<^item> \<^emph>\<open>Global Options / Appearance / Button, menu and label font\<close> as well as |
355 well as \<^emph>\<open>List and text field font\<close>: this specifies the primary and |
347 \<^emph>\<open>List and text field font\<close>: this specifies the primary and secondary font |
356 secondary font for the traditional \<^emph>\<open>Metal\<close> look-and-feel |
348 for the traditional \<^emph>\<open>Metal\<close> look-and-feel (\secref{sec:look-and-feel}), |
357 (\secref{sec:look-and-feel}), which happens to scale better than newer ones |
349 which happens to scale better than newer ones like \<^emph>\<open>Nimbus\<close>. |
358 like \<^emph>\<open>Nimbus\<close>. |
350 |
359 |
351 \<^item> \<^emph>\<open>Plugin Options / Isabelle / General / Reset Font Size\<close>: the main text |
360 \<^item> \<^emph>\<open>Plugin Options / Isabelle / General / Reset Font Size\<close>: the main |
352 area font size for action @{action_ref "isabelle.reset-font-size"}, e.g.\ |
361 text area font size for action @{action_ref "isabelle.reset-font-size"}, |
353 relevant for quick scaling like in major web browsers. |
362 e.g.\ relevant for quick scaling like in major web browsers. |
354 |
363 |
355 \<^item> \<^emph>\<open>Plugin Options / Console / General / Font\<close>: the console window font, |
364 \<^item> \<^emph>\<open>Plugin Options / Console / General / Font\<close>: the console window |
356 e.g.\ relevant for Isabelle/Scala command-line. |
365 font, e.g.\ relevant for Isabelle/Scala command-line. |
357 |
366 |
358 In \figref{fig:isabelle-jedit-hdpi} the \<^emph>\<open>Metal\<close> look-and-feel is configured |
367 |
359 with custom fonts at 30 pixels, and the main text area and console at 36 |
368 In \figref{fig:isabelle-jedit-hdpi} the \<^emph>\<open>Metal\<close> look-and-feel is |
360 pixels. Despite the old-fashioned appearance of \<^emph>\<open>Metal\<close>, this leads to |
369 configured with custom fonts at 30 pixels, and the main text area and |
361 decent rendering quality on all platforms. |
370 console at 36 pixels. Despite the old-fashioned appearance of \<^emph>\<open>Metal\<close>, |
|
371 this leads to decent rendering quality on all platforms. |
|
372 |
362 |
373 \begin{figure}[htb] |
363 \begin{figure}[htb] |
374 \begin{center} |
364 \begin{center} |
375 \includegraphics[width=\textwidth]{isabelle-jedit-hdpi} |
365 \includegraphics[width=\textwidth]{isabelle-jedit-hdpi} |
376 \end{center} |
366 \end{center} |
594 The \<^emph>\<open>SideKick\<close> plugin provides some general services to display buffer |
582 The \<^emph>\<open>SideKick\<close> plugin provides some general services to display buffer |
595 structure in a tree view. |
583 structure in a tree view. |
596 |
584 |
597 Isabelle/jEdit provides SideKick parsers for its main mode for theory files, |
585 Isabelle/jEdit provides SideKick parsers for its main mode for theory files, |
598 as well as some minor modes for the \<^verbatim>\<open>NEWS\<close> file (see |
586 as well as some minor modes for the \<^verbatim>\<open>NEWS\<close> file (see |
599 \figref{fig:sidekick}), session \<^verbatim>\<open>ROOT\<close> files, and system |
587 \figref{fig:sidekick}), session \<^verbatim>\<open>ROOT\<close> files, and system \<^verbatim>\<open>options\<close>. |
600 \<^verbatim>\<open>options\<close>. |
|
601 |
588 |
602 \begin{figure}[htb] |
589 \begin{figure}[htb] |
603 \begin{center} |
590 \begin{center} |
604 \includegraphics[scale=0.333]{sidekick} |
591 \includegraphics[scale=0.333]{sidekick} |
605 \end{center} |
592 \end{center} |
606 \caption{The Isabelle NEWS file with SideKick tree view} |
593 \caption{The Isabelle NEWS file with SideKick tree view} |
607 \label{fig:sidekick} |
594 \label{fig:sidekick} |
608 \end{figure} |
595 \end{figure} |
609 |
596 |
610 Moreover, the special SideKick parser \<^verbatim>\<open>isabelle-markup\<close> |
597 Moreover, the special SideKick parser \<^verbatim>\<open>isabelle-markup\<close> provides access to |
611 provides access to the full (uninterpreted) markup tree of the PIDE |
598 the full (uninterpreted) markup tree of the PIDE document model of the |
612 document model of the current buffer. This is occasionally useful |
599 current buffer. This is occasionally useful for informative purposes, but |
613 for informative purposes, but the amount of displayed information |
600 the amount of displayed information might cause problems for large buffers, |
614 might cause problems for large buffers, both for the human and the |
601 both for the human and the machine. |
615 machine. |
|
616 \<close> |
602 \<close> |
617 |
603 |
618 |
604 |
619 section \<open>Scala console \label{sec:scala-console}\<close> |
605 section \<open>Scala console \label{sec:scala-console}\<close> |
620 |
606 |
621 text \<open> |
607 text \<open> |
622 The \<^emph>\<open>Console\<close> plugin manages various shells (command interpreters), |
608 The \<^emph>\<open>Console\<close> plugin manages various shells (command interpreters), e.g.\ |
623 e.g.\ \<^emph>\<open>BeanShell\<close>, which is the official jEdit scripting language, and |
609 \<^emph>\<open>BeanShell\<close>, which is the official jEdit scripting language, and the |
624 the cross-platform \<^emph>\<open>System\<close> shell. Thus the console provides similar |
610 cross-platform \<^emph>\<open>System\<close> shell. Thus the console provides similar |
625 functionality than the Emacs buffers \<^verbatim>\<open>*scratch*\<close> and |
611 functionality than the Emacs buffers \<^verbatim>\<open>*scratch*\<close> and \<^verbatim>\<open>*shell*\<close>. |
626 \<^verbatim>\<open>*shell*\<close>. |
612 |
627 |
613 Isabelle/jEdit extends the repertoire of the console by \<^emph>\<open>Scala\<close>, which is |
628 Isabelle/jEdit extends the repertoire of the console by \<^emph>\<open>Scala\<close>, which |
614 the regular Scala toplevel loop running inside the same JVM process as |
629 is the regular Scala toplevel loop running inside the same JVM process as |
|
630 Isabelle/jEdit itself. This means the Scala command interpreter has access |
615 Isabelle/jEdit itself. This means the Scala command interpreter has access |
631 to the JVM name space and state of the running Prover IDE application. The |
616 to the JVM name space and state of the running Prover IDE application. The |
632 default environment imports the full content of packages \<^verbatim>\<open>isabelle\<close> and |
617 default environment imports the full content of packages \<^verbatim>\<open>isabelle\<close> and |
633 \<^verbatim>\<open>isabelle.jedit\<close>. |
618 \<^verbatim>\<open>isabelle.jedit\<close>. |
634 |
619 |
635 For example, \<^verbatim>\<open>PIDE\<close> refers to the Isabelle/jEdit plugin object, |
620 For example, \<^verbatim>\<open>PIDE\<close> refers to the Isabelle/jEdit plugin object, and \<^verbatim>\<open>view\<close> |
636 and \<^verbatim>\<open>view\<close> to the current editor view of jEdit. The Scala |
621 to the current editor view of jEdit. The Scala expression |
637 expression \<^verbatim>\<open>PIDE.snapshot(view)\<close> makes a PIDE document snapshot |
622 \<^verbatim>\<open>PIDE.snapshot(view)\<close> makes a PIDE document snapshot of the current buffer |
638 of the current buffer within the current editor view. |
623 within the current editor view. |
639 |
624 |
640 This helps to explore Isabelle/Scala functionality interactively. Some care |
625 This helps to explore Isabelle/Scala functionality interactively. Some care |
641 is required to avoid interference with the internals of the running |
626 is required to avoid interference with the internals of the running |
642 application, especially in production use. |
627 application, especially in production use. |
643 \<close> |
628 \<close> |
778 document model for further checking. It is also possible to let the system |
760 document model for further checking. It is also possible to let the system |
779 resolve dependencies automatically, according to the system option |
761 resolve dependencies automatically, according to the system option |
780 @{system_option jedit_auto_load}. |
762 @{system_option jedit_auto_load}. |
781 |
763 |
782 \<^medskip> |
764 \<^medskip> |
783 The visible \<^emph>\<open>perspective\<close> of Isabelle/jEdit is defined by the |
765 The visible \<^emph>\<open>perspective\<close> of Isabelle/jEdit is defined by the collective |
784 collective view on theory buffers via open text areas. The perspective is |
766 view on theory buffers via open text areas. The perspective is taken as a |
785 taken as a hint for document processing: the prover ensures that those parts |
767 hint for document processing: the prover ensures that those parts of a |
786 of a theory where the user is looking are checked, while other parts that |
768 theory where the user is looking are checked, while other parts that are |
787 are presently not required are ignored. The perspective is changed by |
769 presently not required are ignored. The perspective is changed by opening or |
788 opening or closing text area windows, or scrolling within a window. |
770 closing text area windows, or scrolling within a window. |
789 |
771 |
790 The \<^emph>\<open>Theories\<close> panel provides some further options to influence |
772 The \<^emph>\<open>Theories\<close> panel provides some further options to influence the process |
791 the process of continuous checking: it may be switched off globally |
773 of continuous checking: it may be switched off globally to restrict the |
792 to restrict the prover to superficial processing of command syntax. |
774 prover to superficial processing of command syntax. It is also possible to |
793 It is also possible to indicate theory nodes as \<^emph>\<open>required\<close> for |
775 indicate theory nodes as \<^emph>\<open>required\<close> for continuous checking: this means |
794 continuous checking: this means such nodes and all their imports are |
776 such nodes and all their imports are always processed independently of the |
795 always processed independently of the visibility status (if |
777 visibility status (if continuous checking is enabled). Big theory libraries |
796 continuous checking is enabled). Big theory libraries that are |
778 that are marked as required can have significant impact on performance, |
797 marked as required can have significant impact on performance, |
|
798 though. |
779 though. |
799 |
780 |
800 \<^medskip> |
781 \<^medskip> |
801 Formal markup of checked theory content is turned into GUI |
782 Formal markup of checked theory content is turned into GUI rendering, based |
802 rendering, based on a standard repertoire known from IDEs for programming |
783 on a standard repertoire known from IDEs for programming languages: colors, |
803 languages: colors, icons, highlighting, squiggly underlines, tooltips, |
784 icons, highlighting, squiggly underlines, tooltips, hyperlinks etc. For |
804 hyperlinks etc. For outer syntax of Isabelle/Isar there is some traditional |
785 outer syntax of Isabelle/Isar there is some traditional syntax-highlighting |
805 syntax-highlighting via static keywords and tokenization within the editor; |
786 via static keywords and tokenization within the editor; this buffer syntax |
806 this buffer syntax is determined from theory imports. In contrast, the |
787 is determined from theory imports. In contrast, the painting of inner syntax |
807 painting of inner syntax (term language etc.)\ uses semantic information |
788 (term language etc.)\ uses semantic information that is reported dynamically |
808 that is reported dynamically from the logical context. Thus the prover can |
789 from the logical context. Thus the prover can provide additional markup to |
809 provide additional markup to help the user to understand the meaning of |
790 help the user to understand the meaning of formal text, and to produce more |
810 formal text, and to produce more text with some add-on tools (e.g.\ |
791 text with some add-on tools (e.g.\ information messages with \<^emph>\<open>sendback\<close> |
811 information messages with \<^emph>\<open>sendback\<close> markup by automated provers or |
792 markup by automated provers or disprovers in the background). |
812 disprovers in the background). |
793 \<close> |
813 |
794 |
814 \<close> |
|
815 |
795 |
816 subsection \<open>Auxiliary files \label{sec:aux-files}\<close> |
796 subsection \<open>Auxiliary files \label{sec:aux-files}\<close> |
817 |
797 |
818 text \<open> |
798 text \<open> |
819 Special load commands like @{command_ref ML_file} and @{command_ref |
799 Special load commands like @{command_ref ML_file} and @{command_ref |
923 find a separate window for prover messages familiar, but it is important to |
899 find a separate window for prover messages familiar, but it is important to |
924 understand that the main Prover IDE feedback happens elsewhere. It is |
900 understand that the main Prover IDE feedback happens elsewhere. It is |
925 possible to do meaningful proof editing within the primary text area and its |
901 possible to do meaningful proof editing within the primary text area and its |
926 markup, while using secondary output windows only rarely. |
902 markup, while using secondary output windows only rarely. |
927 |
903 |
928 The main purpose of the output window is to ``debug'' unclear |
904 The main purpose of the output window is to ``debug'' unclear situations by |
929 situations by inspecting internal state of the prover.\<^footnote>\<open>In |
905 inspecting internal state of the prover.\<^footnote>\<open>In that sense, unstructured tactic |
930 that sense, unstructured tactic scripts depend on continuous |
906 scripts depend on continuous debugging with internal state inspection.\<close> |
931 debugging with internal state inspection.\<close> Consequently, some |
907 Consequently, some special messages for \<^emph>\<open>tracing\<close> or \<^emph>\<open>proof state\<close> only |
932 special messages for \<^emph>\<open>tracing\<close> or \<^emph>\<open>proof state\<close> only |
|
933 appear here, and are not attached to the original source. |
908 appear here, and are not attached to the original source. |
934 |
909 |
935 \<^medskip> |
910 \<^medskip> |
936 In any case, prover messages also contain markup that may |
911 In any case, prover messages also contain markup that may be explored |
937 be explored recursively via tooltips or hyperlinks (see |
912 recursively via tooltips or hyperlinks (see |
938 \secref{sec:tooltips-hyperlinks}), or clicked directly to initiate |
913 \secref{sec:tooltips-hyperlinks}), or clicked directly to initiate certain |
939 certain actions (see \secref{sec:auto-tools} and |
914 actions (see \secref{sec:auto-tools} and \secref{sec:sledgehammer}). |
940 \secref{sec:sledgehammer}).\<close> |
915 \<close> |
941 |
916 |
942 |
917 |
943 section \<open>Query \label{sec:query}\<close> |
918 section \<open>Query \label{sec:query}\<close> |
944 |
919 |
945 text \<open> |
920 text \<open> |
946 The \<^emph>\<open>Query\<close> panel provides various GUI forms to request extra |
921 The \<^emph>\<open>Query\<close> panel provides various GUI forms to request extra information |
947 information from the prover. In old times the user would have issued some |
922 from the prover. In old times the user would have issued some diagnostic |
948 diagnostic command like @{command find_theorems} and inspected its output, |
923 command like @{command find_theorems} and inspected its output, but this is |
949 but this is now integrated into the Prover IDE. |
924 now integrated into the Prover IDE. |
950 |
925 |
951 A \<^emph>\<open>Query\<close> window provides some input fields and buttons for a |
926 A \<^emph>\<open>Query\<close> window provides some input fields and buttons for a particular |
952 particular query command, with output in a dedicated text area. There are |
927 query command, with output in a dedicated text area. There are various query |
953 various query modes: \<^emph>\<open>Find Theorems\<close>, \<^emph>\<open>Find Constants\<close>, |
928 modes: \<^emph>\<open>Find Theorems\<close>, \<^emph>\<open>Find Constants\<close>, \<^emph>\<open>Print Context\<close>, e.g.\ see |
954 \<^emph>\<open>Print Context\<close>, e.g.\ see \figref{fig:query}. As usual in jEdit, |
929 \figref{fig:query}. As usual in jEdit, multiple \<^emph>\<open>Query\<close> windows may be |
955 multiple \<^emph>\<open>Query\<close> windows may be active at the same time: any number of |
930 active at the same time: any number of floating instances, but at most one |
956 floating instances, but at most one docked instance (which is used by |
931 docked instance (which is used by default). |
957 default). |
|
958 |
932 |
959 \begin{figure}[htb] |
933 \begin{figure}[htb] |
960 \begin{center} |
934 \begin{center} |
961 \includegraphics[scale=0.333]{query} |
935 \includegraphics[scale=0.333]{query} |
962 \end{center} |
936 \end{center} |
1026 |
999 |
1027 |
1000 |
1028 subsection \<open>Print context\<close> |
1001 subsection \<open>Print context\<close> |
1029 |
1002 |
1030 text \<open> |
1003 text \<open> |
1031 The \<^emph>\<open>Query\<close> panel in \<^emph>\<open>Print Context\<close> mode prints information from |
1004 The \<^emph>\<open>Query\<close> panel in \<^emph>\<open>Print Context\<close> mode prints information from the |
1032 the theory or proof context, or proof state. See also the Isar commands |
1005 theory or proof context, or proof state. See also the Isar commands |
1033 @{command_ref print_context}, @{command_ref print_cases}, @{command_ref |
1006 @{command_ref print_context}, @{command_ref print_cases}, @{command_ref |
1034 print_term_bindings}, @{command_ref print_theorems}, @{command_ref |
1007 print_term_bindings}, @{command_ref print_theorems}, @{command_ref |
1035 print_state} described in @{cite "isabelle-isar-ref"}. |
1008 print_state} described in @{cite "isabelle-isar-ref"}. |
1036 \<close> |
1009 \<close> |
1037 |
1010 |
1038 |
1011 |
1039 section \<open>Tooltips and hyperlinks \label{sec:tooltips-hyperlinks}\<close> |
1012 section \<open>Tooltips and hyperlinks \label{sec:tooltips-hyperlinks}\<close> |
1040 |
1013 |
1041 text \<open> |
1014 text \<open> |
1042 Formally processed text (prover input or output) contains rich markup |
1015 Formally processed text (prover input or output) contains rich markup |
1043 information that can be explored further by using the \<^verbatim>\<open>CONTROL\<close> |
1016 information that can be explored further by using the \<^verbatim>\<open>CONTROL\<close> modifier |
1044 modifier key on Linux and Windows, or \<^verbatim>\<open>COMMAND\<close> on Mac OS X. |
1017 key on Linux and Windows, or \<^verbatim>\<open>COMMAND\<close> on Mac OS X. Hovering with the mouse |
1045 Hovering with the mouse while the modifier is pressed reveals a |
1018 while the modifier is pressed reveals a \<^emph>\<open>tooltip\<close> (grey box over the text |
1046 \<^emph>\<open>tooltip\<close> (grey box over the text with a yellow popup) and/or a |
1019 with a yellow popup) and/or a \<^emph>\<open>hyperlink\<close> (black rectangle over the text |
1047 \<^emph>\<open>hyperlink\<close> (black rectangle over the text with change of mouse |
1020 with change of mouse pointer); see also \figref{fig:tooltip}. |
1048 pointer); see also \figref{fig:tooltip}. |
|
1049 |
1021 |
1050 \begin{figure}[htb] |
1022 \begin{figure}[htb] |
1051 \begin{center} |
1023 \begin{center} |
1052 \includegraphics[scale=0.5]{popup1} |
1024 \includegraphics[scale=0.5]{popup1} |
1053 \end{center} |
1025 \end{center} |
1054 \caption{Tooltip and hyperlink for some formal entity} |
1026 \caption{Tooltip and hyperlink for some formal entity} |
1055 \label{fig:tooltip} |
1027 \label{fig:tooltip} |
1056 \end{figure} |
1028 \end{figure} |
1057 |
1029 |
1058 Tooltip popups use the same rendering mechanisms as the main text |
1030 Tooltip popups use the same rendering mechanisms as the main text area, and |
1059 area, and further tooltips and/or hyperlinks may be exposed |
1031 further tooltips and/or hyperlinks may be exposed recursively by the same |
1060 recursively by the same mechanism; see \figref{fig:nested-tooltips}. |
1032 mechanism; see \figref{fig:nested-tooltips}. |
1061 |
1033 |
1062 \begin{figure}[htb] |
1034 \begin{figure}[htb] |
1063 \begin{center} |
1035 \begin{center} |
1064 \includegraphics[scale=0.5]{popup2} |
1036 \includegraphics[scale=0.5]{popup2} |
1065 \end{center} |
1037 \end{center} |
1066 \caption{Nested tooltips over formal entities} |
1038 \caption{Nested tooltips over formal entities} |
1067 \label{fig:nested-tooltips} |
1039 \label{fig:nested-tooltips} |
1068 \end{figure} |
1040 \end{figure} |
1069 |
1041 |
1070 The tooltip popup window provides some controls to \<^emph>\<open>close\<close> or |
1042 The tooltip popup window provides some controls to \<^emph>\<open>close\<close> or \<^emph>\<open>detach\<close> the |
1071 \<^emph>\<open>detach\<close> the window, turning it into a separate \<^emph>\<open>Info\<close> |
1043 window, turning it into a separate \<^emph>\<open>Info\<close> window managed by jEdit. The |
1072 window managed by jEdit. The \<^verbatim>\<open>ESCAPE\<close> key closes |
1044 \<^verbatim>\<open>ESCAPE\<close> key closes \<^emph>\<open>all\<close> popups, which is particularly relevant when |
1073 \<^emph>\<open>all\<close> popups, which is particularly relevant when nested |
1045 nested tooltips are stacking up. |
1074 tooltips are stacking up. |
1046 |
1075 |
1047 \<^medskip> |
1076 \<^medskip> |
1048 A black rectangle in the text indicates a hyperlink that may be followed by |
1077 A black rectangle in the text indicates a hyperlink that may be |
1049 a mouse click (while the \<^verbatim>\<open>CONTROL\<close> or \<^verbatim>\<open>COMMAND\<close> modifier key is still |
1078 followed by a mouse click (while the \<^verbatim>\<open>CONTROL\<close> or \<^verbatim>\<open>COMMAND\<close> modifier |
1050 pressed). Such jumps to other text locations are recorded by the |
1079 key is still pressed). Such jumps to other text locations |
1051 \<^emph>\<open>Navigator\<close> plugin, which is bundled with Isabelle/jEdit and enabled by |
1080 are recorded by the \<^emph>\<open>Navigator\<close> plugin, which is bundled with |
1052 default, including navigation arrows in the main jEdit toolbar. |
1081 Isabelle/jEdit and enabled by default, including navigation arrows in the |
1053 |
1082 main jEdit toolbar. |
1054 Also note that the link target may be a file that is itself not subject to |
1083 |
1055 formal document processing of the editor session and thus prevents further |
1084 Also note that the link target may be a file that is itself not |
1056 exploration: the chain of hyperlinks may end in some source file of the |
1085 subject to formal document processing of the editor session and thus |
1057 underlying logic image, or within the ML bootstrap sources of |
1086 prevents further exploration: the chain of hyperlinks may end in |
1058 Isabelle/Pure. |
1087 some source file of the underlying logic image, or within the |
1059 \<close> |
1088 ML bootstrap sources of Isabelle/Pure.\<close> |
|
1089 |
1060 |
1090 |
1061 |
1091 section \<open>Completion \label{sec:completion}\<close> |
1062 section \<open>Completion \label{sec:completion}\<close> |
1092 |
1063 |
1093 text \<open> |
1064 text \<open> |
1315 text \<open> |
1283 text \<open> |
1316 Completion is triggered by certain events produced by the user, with |
1284 Completion is triggered by certain events produced by the user, with |
1317 optional delay after keyboard input according to @{system_option |
1285 optional delay after keyboard input according to @{system_option |
1318 jedit_completion_delay}. |
1286 jedit_completion_delay}. |
1319 |
1287 |
1320 \<^descr>[Explicit completion] works via action @{action_ref |
1288 \<^descr>[Explicit completion] works via action @{action_ref "isabelle.complete"} |
1321 "isabelle.complete"} with keyboard shortcut \<^verbatim>\<open>C+b\<close>. This |
1289 with keyboard shortcut \<^verbatim>\<open>C+b\<close>. This overrides the shortcut for @{action_ref |
1322 overrides the shortcut for @{action_ref "complete-word"} in jEdit, but it is |
1290 "complete-word"} in jEdit, but it is possible to restore the original jEdit |
1323 possible to restore the original jEdit keyboard mapping of @{action |
1291 keyboard mapping of @{action "complete-word"} via \<^emph>\<open>Global Options~/ |
1324 "complete-word"} via \<^emph>\<open>Global Options~/ Shortcuts\<close> and invent a |
1292 Shortcuts\<close> and invent a different one for @{action "isabelle.complete"}. |
1325 different one for @{action "isabelle.complete"}. |
|
1326 |
1293 |
1327 \<^descr>[Explicit spell-checker completion] works via @{action_ref |
1294 \<^descr>[Explicit spell-checker completion] works via @{action_ref |
1328 "isabelle.complete-word"}, which is exposed in the jEdit context menu, if |
1295 "isabelle.complete-word"}, which is exposed in the jEdit context menu, if |
1329 the mouse points to a word that the spell-checker can complete. |
1296 the mouse points to a word that the spell-checker can complete. |
1330 |
1297 |
1331 \<^descr>[Implicit completion] works via regular keyboard input of the editor. |
1298 \<^descr>[Implicit completion] works via regular keyboard input of the editor. It |
1332 It depends on further side-conditions: |
1299 depends on further side-conditions: |
1333 |
1300 |
1334 \<^enum> The system option @{system_option_ref jedit_completion} needs to |
1301 \<^enum> The system option @{system_option_ref jedit_completion} needs to be |
1335 be enabled (default). |
1302 enabled (default). |
1336 |
1303 |
1337 \<^enum> Completion of syntax keywords requires at least 3 relevant |
1304 \<^enum> Completion of syntax keywords requires at least 3 relevant characters in |
1338 characters in the text. |
1305 the text. |
1339 |
1306 |
1340 \<^enum> The system option @{system_option_ref jedit_completion_delay} |
1307 \<^enum> The system option @{system_option_ref jedit_completion_delay} determines |
1341 determines an additional delay (0.5 by default), before opening a completion |
1308 an additional delay (0.5 by default), before opening a completion popup. |
1342 popup. The delay gives the prover a chance to provide semantic completion |
1309 The delay gives the prover a chance to provide semantic completion |
1343 information, notably the context (\secref{sec:completion-context}). |
1310 information, notably the context (\secref{sec:completion-context}). |
1344 |
1311 |
1345 \<^enum> The system option @{system_option_ref jedit_completion_immediate} |
1312 \<^enum> The system option @{system_option_ref jedit_completion_immediate} |
1346 (enabled by default) controls whether replacement text should be inserted |
1313 (enabled by default) controls whether replacement text should be inserted |
1347 immediately without popup, regardless of @{system_option |
1314 immediately without popup, regardless of @{system_option |
1348 jedit_completion_delay}. This aggressive mode of completion is restricted to |
1315 jedit_completion_delay}. This aggressive mode of completion is restricted |
1349 Isabelle symbols and their abbreviations (\secref{sec:symbols}). |
1316 to Isabelle symbols and their abbreviations (\secref{sec:symbols}). |
1350 |
1317 |
1351 \<^enum> Completion of symbol abbreviations with only one relevant |
1318 \<^enum> Completion of symbol abbreviations with only one relevant character in |
1352 character in the text always enforces an explicit popup, |
1319 the text always enforces an explicit popup, regardless of |
1353 regardless of @{system_option_ref jedit_completion_immediate}. |
1320 @{system_option_ref jedit_completion_immediate}. |
1354 \<close> |
1321 \<close> |
1355 |
1322 |
1356 |
1323 |
1357 subsection \<open>Completion popup \label{sec:completion-popup}\<close> |
1324 subsection \<open>Completion popup \label{sec:completion-popup}\<close> |
1358 |
1325 |
1359 text \<open> |
1326 text \<open> |
1360 A \<^emph>\<open>completion popup\<close> is a minimally invasive GUI component over the |
1327 A \<^emph>\<open>completion popup\<close> is a minimally invasive GUI component over the text |
1361 text area that offers a selection of completion items to be inserted into |
1328 area that offers a selection of completion items to be inserted into the |
1362 the text, e.g.\ by mouse clicks. Items are sorted dynamically, according to |
1329 text, e.g.\ by mouse clicks. Items are sorted dynamically, according to the |
1363 the frequency of selection, with persistent history. The popup may interpret |
1330 frequency of selection, with persistent history. The popup may interpret |
1364 special keys \<^verbatim>\<open>ENTER\<close>, \<^verbatim>\<open>TAB\<close>, \<^verbatim>\<open>ESCAPE\<close>, |
1331 special keys \<^verbatim>\<open>ENTER\<close>, \<^verbatim>\<open>TAB\<close>, \<^verbatim>\<open>ESCAPE\<close>, \<^verbatim>\<open>UP\<close>, \<^verbatim>\<open>DOWN\<close>, \<^verbatim>\<open>PAGE_UP\<close>, |
1365 \<^verbatim>\<open>UP\<close>, \<^verbatim>\<open>DOWN\<close>, \<^verbatim>\<open>PAGE_UP\<close>, \<^verbatim>\<open>PAGE_DOWN\<close>, but all other key events are |
1332 \<^verbatim>\<open>PAGE_DOWN\<close>, but all other key events are passed to the underlying text |
1366 passed to the underlying text area. |
1333 area. This allows to ignore unwanted completions most of the time and |
1367 This allows to ignore unwanted completions most of the time and continue |
1334 continue typing quickly. Thus the popup serves as a mechanism of |
1368 typing quickly. Thus the popup serves as a mechanism of confirmation of |
1335 confirmation of proposed items, but the default is to continue without |
1369 proposed items, but the default is to continue without completion. |
1336 completion. |
1370 |
1337 |
1371 The meaning of special keys is as follows: |
1338 The meaning of special keys is as follows: |
1372 |
1339 |
1373 \<^medskip> |
1340 \<^medskip> |
1374 \begin{tabular}{ll} |
1341 \begin{tabular}{ll} |
1399 depending on the state of the \<^emph>\<open>text selection\<close>. Isabelle/jEdit tries to |
1366 depending on the state of the \<^emph>\<open>text selection\<close>. Isabelle/jEdit tries to |
1400 accommodate the most common forms of advanced selections in jEdit, but not |
1367 accommodate the most common forms of advanced selections in jEdit, but not |
1401 all combinations make sense. At least the following important cases are |
1368 all combinations make sense. At least the following important cases are |
1402 well-defined: |
1369 well-defined: |
1403 |
1370 |
1404 \<^descr>[No selection.] The original is removed and the replacement inserted, |
1371 \<^descr>[No selection.] The original is removed and the replacement inserted, |
1405 depending on the caret position. |
1372 depending on the caret position. |
1406 |
1373 |
1407 \<^descr>[Rectangular selection of zero width.] This special case is treated by |
1374 \<^descr>[Rectangular selection of zero width.] This special case is treated by |
1408 jEdit as ``tall caret'' and insertion of completion imitates its normal |
1375 jEdit as ``tall caret'' and insertion of completion imitates its normal |
1409 behaviour: separate copies of the replacement are inserted for each line of |
1376 behaviour: separate copies of the replacement are inserted for each line |
1410 the selection. |
1377 of the selection. |
1411 |
1378 |
1412 \<^descr>[Other rectangular selection or multiple selections.] Here the original |
1379 \<^descr>[Other rectangular selection or multiple selections.] Here the original |
1413 is removed and the replacement is inserted for each line (or segment) of the |
1380 is removed and the replacement is inserted for each line (or segment) of |
1414 selection. |
1381 the selection. |
1415 |
1382 |
1416 |
1383 Support for multiple selections is particularly useful for \<^emph>\<open>HyperSearch\<close>: |
1417 Support for multiple selections is particularly useful for |
1384 clicking on one of the items in the \<^emph>\<open>HyperSearch Results\<close> window makes |
1418 \<^emph>\<open>HyperSearch\<close>: clicking on one of the items in the \<^emph>\<open>HyperSearch |
1385 jEdit select all its occurrences in the corresponding line of text. Then |
1419 Results\<close> window makes jEdit select all its occurrences in the corresponding |
1386 explicit completion can be invoked via \<^verbatim>\<open>C+b\<close>, e.g.\ to replace occurrences |
1420 line of text. Then explicit completion can be invoked via \<^verbatim>\<open>C+b\<close>, |
1387 of \<^verbatim>\<open>-->\<close> by \<open>\<longrightarrow>\<close>. |
1421 e.g.\ to replace occurrences of \<^verbatim>\<open>-->\<close> by \<open>\<longrightarrow>\<close>. |
1388 |
1422 |
1389 \<^medskip> |
1423 \<^medskip> |
1390 Insertion works by removing and inserting pieces of text from the buffer. |
1424 Insertion works by removing and inserting pieces of text from the |
1391 This counts as one atomic operation on the jEdit history. Thus unintended |
1425 buffer. This counts as one atomic operation on the jEdit history. Thus |
1392 completions may be reverted by the regular @{action undo} action of jEdit. |
1426 unintended completions may be reverted by the regular @{action undo} action |
1393 According to normal jEdit policies, the recovered text after @{action undo} |
1427 of jEdit. According to normal jEdit policies, the recovered text after |
1394 is selected: \<^verbatim>\<open>ESCAPE\<close> is required to reset the selection and to continue |
1428 @{action undo} is selected: \<^verbatim>\<open>ESCAPE\<close> is required to reset the |
1395 typing more text. |
1429 selection and to continue typing more text. |
|
1430 \<close> |
1396 \<close> |
1431 |
1397 |
1432 |
1398 |
1433 subsection \<open>Options \label{sec:completion-options}\<close> |
1399 subsection \<open>Options \label{sec:completion-options}\<close> |
1434 |
1400 |
1435 text \<open> |
1401 text \<open> |
1436 This is a summary of Isabelle/Scala system options that are relevant for |
1402 This is a summary of Isabelle/Scala system options that are relevant for |
1437 completion. They may be configured in \<^emph>\<open>Plugin Options~/ Isabelle~/ |
1403 completion. They may be configured in \<^emph>\<open>Plugin Options~/ Isabelle~/ General\<close> |
1438 General\<close> as usual. |
1404 as usual. |
1439 |
1405 |
1440 \<^item> @{system_option_def completion_limit} specifies the maximum number of |
1406 \<^item> @{system_option_def completion_limit} specifies the maximum number of |
1441 items for various semantic completion operations (name-space entries etc.) |
1407 items for various semantic completion operations (name-space entries etc.) |
1442 |
1408 |
1443 \<^item> @{system_option_def jedit_completion} guards implicit completion via |
1409 \<^item> @{system_option_def jedit_completion} guards implicit completion via |
1444 regular jEdit key events (\secref{sec:completion-input}): it allows to |
1410 regular jEdit key events (\secref{sec:completion-input}): it allows to |
1445 disable implicit completion altogether. |
1411 disable implicit completion altogether. |
1446 |
1412 |
1447 \<^item> @{system_option_def jedit_completion_select_enter} and |
1413 \<^item> @{system_option_def jedit_completion_select_enter} and @{system_option_def |
1448 @{system_option_def jedit_completion_select_tab} enable keys to select a |
1414 jedit_completion_select_tab} enable keys to select a completion item from |
1449 completion item from the popup (\secref{sec:completion-popup}). Note that a |
1415 the popup (\secref{sec:completion-popup}). Note that a regular mouse click |
1450 regular mouse click on the list of items is always possible. |
1416 on the list of items is always possible. |
1451 |
1417 |
1452 \<^item> @{system_option_def jedit_completion_context} specifies whether the |
1418 \<^item> @{system_option_def jedit_completion_context} specifies whether the |
1453 language context provided by the prover should be used at all. Disabling |
1419 language context provided by the prover should be used at all. Disabling |
1454 that option makes completion less ``semantic''. Note that incomplete or |
1420 that option makes completion less ``semantic''. Note that incomplete or |
1455 severely broken input may cause some disagreement of the prover and the user |
1421 severely broken input may cause some disagreement of the prover and the user |
1457 |
1423 |
1458 \<^item> @{system_option_def jedit_completion_delay} and @{system_option_def |
1424 \<^item> @{system_option_def jedit_completion_delay} and @{system_option_def |
1459 jedit_completion_immediate} determine the handling of keyboard events for |
1425 jedit_completion_immediate} determine the handling of keyboard events for |
1460 implicit completion (\secref{sec:completion-input}). |
1426 implicit completion (\secref{sec:completion-input}). |
1461 |
1427 |
1462 A @{system_option jedit_completion_delay}~\<^verbatim>\<open>> 0\<close> postpones the |
1428 A @{system_option jedit_completion_delay}~\<^verbatim>\<open>> 0\<close> postpones the processing of |
1463 processing of key events, until after the user has stopped typing for the |
1429 key events, until after the user has stopped typing for the given time span, |
1464 given time span, but @{system_option jedit_completion_immediate}~\<^verbatim>\<open>"= true\<close> |
1430 but @{system_option jedit_completion_immediate}~\<^verbatim>\<open>"= true\<close> means that |
1465 means that abbreviations of Isabelle symbols are handled nonetheless. |
1431 abbreviations of Isabelle symbols are handled nonetheless. |
1466 |
1432 |
1467 \<^item> @{system_option_def jedit_completion_path_ignore} specifies ``glob'' |
1433 \<^item> @{system_option_def jedit_completion_path_ignore} specifies ``glob'' |
1468 patterns to ignore in file-system path completion (separated by colons), |
1434 patterns to ignore in file-system path completion (separated by colons), |
1469 e.g.\ backup files ending with tilde. |
1435 e.g.\ backup files ending with tilde. |
1470 |
1436 |
1471 \<^item> @{system_option_def spell_checker} is a global guard for all |
1437 \<^item> @{system_option_def spell_checker} is a global guard for all spell-checker |
1472 spell-checker operations: it allows to disable that mechanism altogether. |
1438 operations: it allows to disable that mechanism altogether. |
1473 |
1439 |
1474 \<^item> @{system_option_def spell_checker_dictionary} determines the current |
1440 \<^item> @{system_option_def spell_checker_dictionary} determines the current |
1475 dictionary, taken from the colon-separated list in the settings variable |
1441 dictionary, taken from the colon-separated list in the settings variable |
1476 @{setting_def JORTHO_DICTIONARIES}. There are jEdit actions to specify local |
1442 @{setting_def JORTHO_DICTIONARIES}. There are jEdit actions to specify local |
1477 updates to a dictionary, by including or excluding words. The result of |
1443 updates to a dictionary, by including or excluding words. The result of |
1478 permanent dictionary updates is stored in the directory @{file_unchecked |
1444 permanent dictionary updates is stored in the directory @{file_unchecked |
1479 "$ISABELLE_HOME_USER/dictionaries"}, in a separate file for each dictionary. |
1445 "$ISABELLE_HOME_USER/dictionaries"}, in a separate file for each dictionary. |
1480 |
1446 |
1481 \<^item> @{system_option_def spell_checker_elements} specifies a |
1447 \<^item> @{system_option_def spell_checker_elements} specifies a comma-separated |
1482 comma-separated list of markup elements that delimit words in the source |
1448 list of markup elements that delimit words in the source that is subject to |
1483 that is subject to spell-checking, including various forms of comments. |
1449 spell-checking, including various forms of comments. |
1484 \<close> |
1450 \<close> |
1485 |
1451 |
1486 |
1452 |
1487 section \<open>Automatically tried tools \label{sec:auto-tools}\<close> |
1453 section \<open>Automatically tried tools \label{sec:auto-tools}\<close> |
1488 |
1454 |
1489 text \<open> |
1455 text \<open> |
1490 Continuous document processing works asynchronously in the background. |
1456 Continuous document processing works asynchronously in the background. |
1491 Visible document source that has been evaluated may get augmented by |
1457 Visible document source that has been evaluated may get augmented by |
1492 additional results of \<^emph>\<open>asynchronous print functions\<close>. The canonical |
1458 additional results of \<^emph>\<open>asynchronous print functions\<close>. The canonical example |
1493 example is proof state output, which is always enabled. More heavy-weight |
1459 is proof state output, which is always enabled. More heavy-weight print |
1494 print functions may be applied, in order to prove or disprove parts of the |
1460 functions may be applied, in order to prove or disprove parts of the formal |
1495 formal text by other means. |
1461 text by other means. |
1496 |
1462 |
1497 Isabelle/HOL provides various automatically tried tools that operate |
1463 Isabelle/HOL provides various automatically tried tools that operate on |
1498 on outermost goal statements (e.g.\ @{command lemma}, @{command |
1464 outermost goal statements (e.g.\ @{command lemma}, @{command theorem}), |
1499 theorem}), independently of the state of the current proof attempt. |
1465 independently of the state of the current proof attempt. They work |
1500 They work implicitly without any arguments. Results are output as |
1466 implicitly without any arguments. Results are output as \<^emph>\<open>information |
1501 \<^emph>\<open>information messages\<close>, which are indicated in the text area by |
1467 messages\<close>, which are indicated in the text area by blue squiggles and a blue |
1502 blue squiggles and a blue information sign in the gutter (see |
1468 information sign in the gutter (see \figref{fig:auto-tools}). The message |
1503 \figref{fig:auto-tools}). The message content may be shown as for |
1469 content may be shown as for other output (see also \secref{sec:output}). |
1504 other output (see also \secref{sec:output}). Some tools |
1470 Some tools produce output with \<^emph>\<open>sendback\<close> markup, which means that clicking |
1505 produce output with \<^emph>\<open>sendback\<close> markup, which means that |
1471 on certain parts of the output inserts that text into the source in the |
1506 clicking on certain parts of the output inserts that text into the |
1472 proper place. |
1507 source in the proper place. |
|
1508 |
1473 |
1509 \begin{figure}[htb] |
1474 \begin{figure}[htb] |
1510 \begin{center} |
1475 \begin{center} |
1511 \includegraphics[scale=0.333]{auto-tools} |
1476 \includegraphics[scale=0.333]{auto-tools} |
1512 \end{center} |
1477 \end{center} |
1513 \caption{Result of automatically tried tools} |
1478 \caption{Result of automatically tried tools} |
1514 \label{fig:auto-tools} |
1479 \label{fig:auto-tools} |
1515 \end{figure} |
1480 \end{figure} |
1516 |
1481 |
1517 \<^medskip> |
1482 \<^medskip> |
1518 The following Isabelle system options control the behavior |
1483 The following Isabelle system options control the behavior of automatically |
1519 of automatically tried tools (see also the jEdit dialog window |
1484 tried tools (see also the jEdit dialog window \<^emph>\<open>Plugin Options~/ Isabelle~/ |
1520 \<^emph>\<open>Plugin Options~/ Isabelle~/ General~/ Automatically tried |
1485 General~/ Automatically tried tools\<close>): |
1521 tools\<close>): |
1486 |
1522 |
1487 \<^item> @{system_option_ref auto_methods} controls automatic use of a combination |
1523 \<^item> @{system_option_ref auto_methods} controls automatic use of a |
1488 of standard proof methods (@{method auto}, @{method simp}, @{method blast}, |
1524 combination of standard proof methods (@{method auto}, @{method |
1489 etc.). This corresponds to the Isar command @{command_ref "try0"} @{cite |
1525 simp}, @{method blast}, etc.). This corresponds to the Isar command |
1490 "isabelle-isar-ref"}. |
1526 @{command_ref "try0"} @{cite "isabelle-isar-ref"}. |
|
1527 |
1491 |
1528 The tool is disabled by default, since unparameterized invocation of |
1492 The tool is disabled by default, since unparameterized invocation of |
1529 standard proof methods often consumes substantial CPU resources |
1493 standard proof methods often consumes substantial CPU resources without |
1530 without leading to success. |
1494 leading to success. |
1531 |
1495 |
1532 \<^item> @{system_option_ref auto_nitpick} controls a slightly reduced |
1496 \<^item> @{system_option_ref auto_nitpick} controls a slightly reduced version of |
1533 version of @{command_ref nitpick}, which tests for counterexamples using |
1497 @{command_ref nitpick}, which tests for counterexamples using first-order |
1534 first-order relational logic. See also the Nitpick manual |
1498 relational logic. See also the Nitpick manual @{cite "isabelle-nitpick"}. |
1535 @{cite "isabelle-nitpick"}. |
1499 |
1536 |
1500 This tool is disabled by default, due to the extra overhead of invoking an |
1537 This tool is disabled by default, due to the extra overhead of |
1501 external Java process for each attempt to disprove a subgoal. |
1538 invoking an external Java process for each attempt to disprove a |
|
1539 subgoal. |
|
1540 |
1502 |
1541 \<^item> @{system_option_ref auto_quickcheck} controls automatic use of |
1503 \<^item> @{system_option_ref auto_quickcheck} controls automatic use of |
1542 @{command_ref quickcheck}, which tests for counterexamples using a |
1504 @{command_ref quickcheck}, which tests for counterexamples using a series of |
1543 series of assignments for free variables of a subgoal. |
1505 assignments for free variables of a subgoal. |
1544 |
1506 |
1545 This tool is \<^emph>\<open>enabled\<close> by default. It requires little |
1507 This tool is \<^emph>\<open>enabled\<close> by default. It requires little overhead, but is a |
1546 overhead, but is a bit weaker than @{command nitpick}. |
1508 bit weaker than @{command nitpick}. |
1547 |
1509 |
1548 \<^item> @{system_option_ref auto_sledgehammer} controls a significantly |
1510 \<^item> @{system_option_ref auto_sledgehammer} controls a significantly reduced |
1549 reduced version of @{command_ref sledgehammer}, which attempts to prove |
1511 version of @{command_ref sledgehammer}, which attempts to prove a subgoal |
1550 a subgoal using external automatic provers. See also the |
1512 using external automatic provers. See also the Sledgehammer manual @{cite |
1551 Sledgehammer manual @{cite "isabelle-sledgehammer"}. |
1513 "isabelle-sledgehammer"}. |
1552 |
1514 |
1553 This tool is disabled by default, due to the relatively heavy nature |
1515 This tool is disabled by default, due to the relatively heavy nature of |
1554 of Sledgehammer. |
1516 Sledgehammer. |
1555 |
1517 |
1556 \<^item> @{system_option_ref auto_solve_direct} controls automatic use of |
1518 \<^item> @{system_option_ref auto_solve_direct} controls automatic use of |
1557 @{command_ref solve_direct}, which checks whether the current subgoals |
1519 @{command_ref solve_direct}, which checks whether the current subgoals can |
1558 can be solved directly by an existing theorem. This also helps to |
1520 be solved directly by an existing theorem. This also helps to detect |
1559 detect duplicate lemmas. |
1521 duplicate lemmas. |
1560 |
1522 |
1561 This tool is \<^emph>\<open>enabled\<close> by default. |
1523 This tool is \<^emph>\<open>enabled\<close> by default. |
1562 |
1524 |
1563 |
1525 |
1564 Invocation of automatically tried tools is subject to some global |
1526 Invocation of automatically tried tools is subject to some global policies |
1565 policies of parallel execution, which may be configured as follows: |
1527 of parallel execution, which may be configured as follows: |
1566 |
1528 |
1567 \<^item> @{system_option_ref auto_time_limit} (default 2.0) determines the |
1529 \<^item> @{system_option_ref auto_time_limit} (default 2.0) determines the timeout |
1568 timeout (in seconds) for each tool execution. |
1530 (in seconds) for each tool execution. |
1569 |
1531 |
1570 \<^item> @{system_option_ref auto_time_start} (default 1.0) determines the |
1532 \<^item> @{system_option_ref auto_time_start} (default 1.0) determines the start |
1571 start delay (in seconds) for automatically tried tools, after the |
1533 delay (in seconds) for automatically tried tools, after the main command |
1572 main command evaluation is finished. |
1534 evaluation is finished. |
1573 |
1535 |
1574 |
1536 |
1575 Each tool is submitted independently to the pool of parallel |
1537 Each tool is submitted independently to the pool of parallel execution tasks |
1576 execution tasks in Isabelle/ML, using hardwired priorities according |
1538 in Isabelle/ML, using hardwired priorities according to its relative |
1577 to its relative ``heaviness''. The main stages of evaluation and |
1539 ``heaviness''. The main stages of evaluation and printing of proof states |
1578 printing of proof states take precedence, but an already running |
1540 take precedence, but an already running tool is not canceled and may thus |
1579 tool is not canceled and may thus reduce reactivity of proof |
1541 reduce reactivity of proof document processing. |
1580 document processing. |
1542 |
1581 |
1543 Users should experiment how the available CPU resources (number of cores) |
1582 Users should experiment how the available CPU resources (number of |
1544 are best invested to get additional feedback from prover in the background, |
1583 cores) are best invested to get additional feedback from prover in |
1545 by using a selection of weaker or stronger tools. |
1584 the background, by using a selection of weaker or stronger tools. |
|
1585 \<close> |
1546 \<close> |
1586 |
1547 |
1587 |
1548 |
1588 section \<open>Sledgehammer \label{sec:sledgehammer}\<close> |
1549 section \<open>Sledgehammer \label{sec:sledgehammer}\<close> |
1589 |
1550 |
1590 text \<open>The \<^emph>\<open>Sledgehammer\<close> panel (\figref{fig:sledgehammer}) |
1551 text \<open> |
1591 provides a view on some independent execution of the Isar command |
1552 The \<^emph>\<open>Sledgehammer\<close> panel (\figref{fig:sledgehammer}) provides a view on |
1592 @{command_ref sledgehammer}, with process indicator (spinning wheel) and |
1553 some independent execution of the Isar command @{command_ref sledgehammer}, |
1593 GUI elements for important Sledgehammer arguments and options. Any |
1554 with process indicator (spinning wheel) and GUI elements for important |
1594 number of Sledgehammer panels may be active, according to the |
1555 Sledgehammer arguments and options. Any number of Sledgehammer panels may be |
1595 standard policies of Dockable Window Management in jEdit. Closing |
1556 active, according to the standard policies of Dockable Window Management in |
1596 such windows also cancels the corresponding prover tasks. |
1557 jEdit. Closing such windows also cancels the corresponding prover tasks. |
1597 |
1558 |
1598 \begin{figure}[htb] |
1559 \begin{figure}[htb] |
1599 \begin{center} |
1560 \begin{center} |
1600 \includegraphics[scale=0.333]{sledgehammer} |
1561 \includegraphics[scale=0.333]{sledgehammer} |
1601 \end{center} |
1562 \end{center} |
1602 \caption{An instance of the Sledgehammer panel} |
1563 \caption{An instance of the Sledgehammer panel} |
1603 \label{fig:sledgehammer} |
1564 \label{fig:sledgehammer} |
1604 \end{figure} |
1565 \end{figure} |
1605 |
1566 |
1606 The \<^emph>\<open>Apply\<close> button attaches a fresh invocation of @{command |
1567 The \<^emph>\<open>Apply\<close> button attaches a fresh invocation of @{command sledgehammer} |
1607 sledgehammer} to the command where the cursor is pointing in the |
1568 to the command where the cursor is pointing in the text --- this should be |
1608 text --- this should be some pending proof problem. Further buttons |
1569 some pending proof problem. Further buttons like \<^emph>\<open>Cancel\<close> and \<^emph>\<open>Locate\<close> |
1609 like \<^emph>\<open>Cancel\<close> and \<^emph>\<open>Locate\<close> help to manage the running |
1570 help to manage the running process. |
1610 process. |
1571 |
1611 |
1572 Results appear incrementally in the output window of the panel. Proposed |
1612 Results appear incrementally in the output window of the panel. |
1573 proof snippets are marked-up as \<^emph>\<open>sendback\<close>, which means a single mouse |
1613 Proposed proof snippets are marked-up as \<^emph>\<open>sendback\<close>, which |
1574 click inserts the text into a suitable place of the original source. Some |
1614 means a single mouse click inserts the text into a suitable place of |
1575 manual editing may be required nonetheless, say to remove earlier proof |
1615 the original source. Some manual editing may be required |
1576 attempts. |
1616 nonetheless, say to remove earlier proof attempts.\<close> |
1577 \<close> |
1617 |
1578 |
1618 |
1579 |
1619 chapter \<open>Isabelle document preparation\<close> |
1580 chapter \<open>Isabelle document preparation\<close> |
1620 |
1581 |
1621 text \<open>The ultimate purpose of Isabelle is to produce nicely rendered documents |
1582 text \<open> |
|
1583 The ultimate purpose of Isabelle is to produce nicely rendered documents |
1622 with the Isabelle document preparation system, which is based on {\LaTeX}; |
1584 with the Isabelle document preparation system, which is based on {\LaTeX}; |
1623 see also @{cite "isabelle-system" and "isabelle-isar-ref"}. Isabelle/jEdit |
1585 see also @{cite "isabelle-system" and "isabelle-isar-ref"}. Isabelle/jEdit |
1624 provides some additional support for document editing.\<close> |
1586 provides some additional support for document editing. |
|
1587 \<close> |
1625 |
1588 |
1626 |
1589 |
1627 section \<open>Document outline\<close> |
1590 section \<open>Document outline\<close> |
1628 |
1591 |
1629 text \<open>Theory sources may contain document markup commands, such as |
1592 text \<open> |
1630 @{command_ref chapter}, @{command_ref section}, @{command subsection}. The |
1593 Theory sources may contain document markup commands, such as @{command_ref |
1631 Isabelle SideKick parser (\secref{sec:sidekick}) represents this document |
1594 chapter}, @{command_ref section}, @{command subsection}. The Isabelle |
1632 outline as structured tree view, with formal statements and proofs nested |
1595 SideKick parser (\secref{sec:sidekick}) represents this document outline as |
1633 inside; see \figref{fig:sidekick-document}. |
1596 structured tree view, with formal statements and proofs nested inside; see |
|
1597 \figref{fig:sidekick-document}. |
1634 |
1598 |
1635 \begin{figure}[htb] |
1599 \begin{figure}[htb] |
1636 \begin{center} |
1600 \begin{center} |
1637 \includegraphics[scale=0.333]{sidekick-document} |
1601 \includegraphics[scale=0.333]{sidekick-document} |
1638 \end{center} |
1602 \end{center} |
1639 \caption{Isabelle document outline via SideKick tree view} |
1603 \caption{Isabelle document outline via SideKick tree view} |
1640 \label{fig:sidekick-document} |
1604 \label{fig:sidekick-document} |
1641 \end{figure} |
1605 \end{figure} |
1642 |
1606 |
1643 It is also possible to use text folding according to this structure, by |
1607 It is also possible to use text folding according to this structure, by |
1644 adjusting \<^emph>\<open>Utilities / Buffer Options / Folding mode\<close> of jEdit. The |
1608 adjusting \<^emph>\<open>Utilities / Buffer Options / Folding mode\<close> of jEdit. The default |
1645 default mode \<^verbatim>\<open>isabelle\<close> uses the structure of formal definitions, |
1609 mode \<^verbatim>\<open>isabelle\<close> uses the structure of formal definitions, statements, and |
1646 statements, and proofs. The alternative mode \<^verbatim>\<open>sidekick\<close> uses the |
1610 proofs. The alternative mode \<^verbatim>\<open>sidekick\<close> uses the document structure of the |
1647 document structure of the SideKick parser, as explained above.\<close> |
1611 SideKick parser, as explained above. |
|
1612 \<close> |
1648 |
1613 |
1649 |
1614 |
1650 section \<open>Citations and Bib{\TeX} entries\<close> |
1615 section \<open>Citations and Bib{\TeX} entries\<close> |
1651 |
1616 |
1652 text \<open>Citations are managed by {\LaTeX} and Bib{\TeX} in \<^verbatim>\<open>.bib\<close> |
1617 text \<open> |
1653 files. The Isabelle session build process and the @{tool latex} tool @{cite |
1618 Citations are managed by {\LaTeX} and Bib{\TeX} in \<^verbatim>\<open>.bib\<close> files. The |
|
1619 Isabelle session build process and the @{tool latex} tool @{cite |
1654 "isabelle-system"} are smart enough to assemble the result, based on the |
1620 "isabelle-system"} are smart enough to assemble the result, based on the |
1655 session directory layout. |
1621 session directory layout. |
1656 |
1622 |
1657 The document antiquotation \<open>@{cite}\<close> is described in @{cite |
1623 The document antiquotation \<open>@{cite}\<close> is described in @{cite |
1658 "isabelle-isar-ref"}. Within the Prover IDE it provides semantic markup for |
1624 "isabelle-isar-ref"}. Within the Prover IDE it provides semantic markup for |
1659 tooltips, hyperlinks, and completion for Bib{\TeX} database entries. |
1625 tooltips, hyperlinks, and completion for Bib{\TeX} database entries. |
1660 Isabelle/jEdit does \<^emph>\<open>not\<close> know about the actual Bib{\TeX} environment |
1626 Isabelle/jEdit does \<^emph>\<open>not\<close> know about the actual Bib{\TeX} environment used |
1661 used in {\LaTeX} batch-mode, but it can take citations from those \<^verbatim>\<open>.bib\<close> |
1627 in {\LaTeX} batch-mode, but it can take citations from those \<^verbatim>\<open>.bib\<close> files |
1662 files that happen to be open in the editor; see \figref{fig:cite-completion}. |
1628 that happen to be open in the editor; see \figref{fig:cite-completion}. |
1663 |
1629 |
1664 \begin{figure}[htb] |
1630 \begin{figure}[htb] |
1665 \begin{center} |
1631 \begin{center} |
1666 \includegraphics[scale=0.333]{cite-completion} |
1632 \includegraphics[scale=0.333]{cite-completion} |
1667 \end{center} |
1633 \end{center} |
1668 \caption{Semantic completion of citations from open Bib{\TeX} files} |
1634 \caption{Semantic completion of citations from open Bib{\TeX} files} |
1669 \label{fig:cite-completion} |
1635 \label{fig:cite-completion} |
1670 \end{figure} |
1636 \end{figure} |
1671 |
1637 |
1672 Isabelle/jEdit also provides some support for editing \<^verbatim>\<open>.bib\<close> |
1638 Isabelle/jEdit also provides some support for editing \<^verbatim>\<open>.bib\<close> files |
1673 files themselves. There is syntax highlighting based on entry types |
1639 themselves. There is syntax highlighting based on entry types (according to |
1674 (according to standard Bib{\TeX} styles), a context-menu to compose entries |
1640 standard Bib{\TeX} styles), a context-menu to compose entries |
1675 systematically, and a SideKick tree view of the overall content; see |
1641 systematically, and a SideKick tree view of the overall content; see |
1676 \figref{fig:bibtex-mode}. |
1642 \figref{fig:bibtex-mode}. |
1677 |
1643 |
1678 \begin{figure}[htb] |
1644 \begin{figure}[htb] |
1679 \begin{center} |
1645 \begin{center} |
1687 |
1653 |
1688 chapter \<open>Miscellaneous tools\<close> |
1654 chapter \<open>Miscellaneous tools\<close> |
1689 |
1655 |
1690 section \<open>Timing\<close> |
1656 section \<open>Timing\<close> |
1691 |
1657 |
1692 text \<open>Managed evaluation of commands within PIDE documents includes |
1658 text \<open> |
1693 timing information, which consists of elapsed (wall-clock) time, CPU |
1659 Managed evaluation of commands within PIDE documents includes timing |
1694 time, and GC (garbage collection) time. Note that in a |
1660 information, which consists of elapsed (wall-clock) time, CPU time, and GC |
1695 multithreaded system it is difficult to measure execution time |
1661 (garbage collection) time. Note that in a multithreaded system it is |
1696 precisely: elapsed time is closer to the real requirements of |
1662 difficult to measure execution time precisely: elapsed time is closer to the |
1697 runtime resources than CPU or GC time, which are both subject to |
1663 real requirements of runtime resources than CPU or GC time, which are both |
1698 influences from the parallel environment that are outside the scope |
1664 subject to influences from the parallel environment that are outside the |
1699 of the current command transaction. |
1665 scope of the current command transaction. |
1700 |
1666 |
1701 The \<^emph>\<open>Timing\<close> panel provides an overview of cumulative command |
1667 The \<^emph>\<open>Timing\<close> panel provides an overview of cumulative command timings for |
1702 timings for each document node. Commands with elapsed time below |
1668 each document node. Commands with elapsed time below the given threshold are |
1703 the given threshold are ignored in the grand total. Nodes are |
1669 ignored in the grand total. Nodes are sorted according to their overall |
1704 sorted according to their overall timing. For the document node |
1670 timing. For the document node that corresponds to the current buffer, |
1705 that corresponds to the current buffer, individual command timings |
1671 individual command timings are shown as well. A double-click on a theory |
1706 are shown as well. A double-click on a theory node or command moves |
1672 node or command moves the editor focus to that particular source position. |
1707 the editor focus to that particular source position. |
1673 |
1708 |
1674 It is also possible to reveal individual timing information via some tooltip |
1709 It is also possible to reveal individual timing information via some |
1675 for the corresponding command keyword, using the technique of mouse hovering |
1710 tooltip for the corresponding command keyword, using the technique |
1676 with \<^verbatim>\<open>CONTROL\<close>~/ \<^verbatim>\<open>COMMAND\<close> modifier key as explained in |
1711 of mouse hovering with \<^verbatim>\<open>CONTROL\<close>/\<^verbatim>\<open>COMMAND\<close> |
1677 \secref{sec:tooltips-hyperlinks}. Actual display of timing depends on the |
1712 modifier key as explained in \secref{sec:tooltips-hyperlinks}. |
1678 global option @{system_option_ref jedit_timing_threshold}, which can be |
1713 Actual display of timing depends on the global option |
1679 configured in \<^emph>\<open>Plugin Options~/ Isabelle~/ General\<close>. |
1714 @{system_option_ref jedit_timing_threshold}, which can be configured in |
1680 |
1715 \<^emph>\<open>Plugin Options~/ Isabelle~/ General\<close>. |
1681 \<^medskip> |
1716 |
1682 The \<^emph>\<open>Monitor\<close> panel visualizes various data collections about recent |
1717 \<^medskip> |
1683 activity of the Isabelle/ML task farm and the underlying ML runtime system. |
1718 The \<^emph>\<open>Monitor\<close> panel visualizes various data collections about |
1684 The display is continuously updated according to @{system_option_ref |
1719 recent activity of the Isabelle/ML task farm and the underlying ML runtime |
|
1720 system. The display is continuously updated according to @{system_option_ref |
|
1721 editor_chart_delay}. Note that the painting of the chart takes considerable |
1685 editor_chart_delay}. Note that the painting of the chart takes considerable |
1722 runtime itself --- on the Java Virtual Machine that runs Isabelle/Scala, not |
1686 runtime itself --- on the Java Virtual Machine that runs Isabelle/Scala, not |
1723 Isabelle/ML. Internally, the Isabelle/Scala module \<^verbatim>\<open>isabelle.ML_Statistics\<close> |
1687 Isabelle/ML. Internally, the Isabelle/Scala module \<^verbatim>\<open>isabelle.ML_Statistics\<close> |
1724 provides further access to statistics of Isabelle/ML. |
1688 provides further access to statistics of Isabelle/ML. |
1725 \<close> |
1689 \<close> |
1726 |
1690 |
1727 |
1691 |
1728 section \<open>Low-level output\<close> |
1692 section \<open>Low-level output\<close> |
1729 |
1693 |
1730 text \<open>Prover output is normally shown directly in the main text area |
1694 text \<open> |
1731 or secondary \<^emph>\<open>Output\<close> panels, as explained in |
1695 Prover output is normally shown directly in the main text area or secondary |
1732 \secref{sec:output}. |
1696 \<^emph>\<open>Output\<close> panels, as explained in \secref{sec:output}. |
1733 |
1697 |
1734 Beyond this, it is occasionally useful to inspect low-level output |
1698 Beyond this, it is occasionally useful to inspect low-level output channels |
1735 channels via some of the following additional panels: |
1699 via some of the following additional panels: |
1736 |
1700 |
1737 \<^item> \<^emph>\<open>Protocol\<close> shows internal messages between the |
1701 \<^item> \<^emph>\<open>Protocol\<close> shows internal messages between the Isabelle/Scala and |
1738 Isabelle/Scala and Isabelle/ML side of the PIDE document editing protocol. |
1702 Isabelle/ML side of the PIDE document editing protocol. Recording of |
1739 Recording of messages starts with the first activation of the |
1703 messages starts with the first activation of the corresponding dockable |
1740 corresponding dockable window; earlier messages are lost. |
1704 window; earlier messages are lost. |
1741 |
1705 |
1742 Actual display of protocol messages causes considerable slowdown, so |
1706 Actual display of protocol messages causes considerable slowdown, so it is |
1743 it is important to undock all \<^emph>\<open>Protocol\<close> panels for production |
1707 important to undock all \<^emph>\<open>Protocol\<close> panels for production work. |
1744 work. |
|
1745 |
1708 |
1746 \<^item> \<^emph>\<open>Raw Output\<close> shows chunks of text from the \<^verbatim>\<open>stdout\<close> and \<^verbatim>\<open>stderr\<close> |
1709 \<^item> \<^emph>\<open>Raw Output\<close> shows chunks of text from the \<^verbatim>\<open>stdout\<close> and \<^verbatim>\<open>stderr\<close> |
1747 channels of the prover process. |
1710 channels of the prover process. Recording of output starts with the first |
1748 Recording of output starts with the first activation of the |
1711 activation of the corresponding dockable window; earlier output is lost. |
1749 corresponding dockable window; earlier output is lost. |
1712 |
1750 |
1713 The implicit stateful nature of physical I/O channels makes it difficult to |
1751 The implicit stateful nature of physical I/O channels makes it |
1714 relate raw output to the actual command from where it was originating. |
1752 difficult to relate raw output to the actual command from where it |
1715 Parallel execution may add to the confusion. Peeking at physical process I/O |
1753 was originating. Parallel execution may add to the confusion. |
1716 is only the last resort to diagnose problems with tools that are not PIDE |
1754 Peeking at physical process I/O is only the last resort to diagnose |
1717 compliant. |
1755 problems with tools that are not PIDE compliant. |
|
1756 |
1718 |
1757 Under normal circumstances, prover output always works via managed message |
1719 Under normal circumstances, prover output always works via managed message |
1758 channels (corresponding to @{ML writeln}, @{ML warning}, @{ML |
1720 channels (corresponding to @{ML writeln}, @{ML warning}, @{ML |
1759 Output.error_message} in Isabelle/ML), which are displayed by regular means |
1721 Output.error_message} in Isabelle/ML), which are displayed by regular means |
1760 within the document model (\secref{sec:output}). Unhandled Isabelle/ML |
1722 within the document model (\secref{sec:output}). Unhandled Isabelle/ML |
1761 exceptions are printed by the system via @{ML Output.error_message}. |
1723 exceptions are printed by the system via @{ML Output.error_message}. |
1762 |
1724 |
1763 \<^item> \<^emph>\<open>Syslog\<close> shows system messages that might be relevant to diagnose |
1725 \<^item> \<^emph>\<open>Syslog\<close> shows system messages that might be relevant to diagnose |
1764 problems with the startup or shutdown phase of the prover process; this also |
1726 problems with the startup or shutdown phase of the prover process; this also |
1765 includes raw output on \<^verbatim>\<open>stderr\<close>. Isabelle/ML also provides an |
1727 includes raw output on \<^verbatim>\<open>stderr\<close>. Isabelle/ML also provides an explicit @{ML |
1766 explicit @{ML Output.system_message} operation, which is occasionally useful |
1728 Output.system_message} operation, which is occasionally useful for |
1767 for diagnostic purposes within the system infrastructure itself. |
1729 diagnostic purposes within the system infrastructure itself. |
1768 |
1730 |
1769 A limited amount of syslog messages are buffered, independently of |
1731 A limited amount of syslog messages are buffered, independently of the |
1770 the docking state of the \<^emph>\<open>Syslog\<close> panel. This allows to |
1732 docking state of the \<^emph>\<open>Syslog\<close> panel. This allows to diagnose serious |
1771 diagnose serious problems with Isabelle/PIDE process management, |
1733 problems with Isabelle/PIDE process management, outside of the actual |
1772 outside of the actual protocol layer. |
1734 protocol layer. |
1773 |
1735 |
1774 Under normal situations, such low-level system output can be |
1736 Under normal situations, such low-level system output can be ignored. |
1775 ignored. |
|
1776 \<close> |
1737 \<close> |
1777 |
1738 |
1778 |
1739 |
1779 chapter \<open>Known problems and workarounds \label{sec:problems}\<close> |
1740 chapter \<open>Known problems and workarounds \label{sec:problems}\<close> |
1780 |
1741 |
1781 text \<open> |
1742 text \<open> |
1782 \<^item> \<^bold>\<open>Problem:\<close> Odd behavior of some diagnostic commands with |
1743 \<^item> \<^bold>\<open>Problem:\<close> Odd behavior of some diagnostic commands with global |
1783 global side-effects, like writing a physical file. |
1744 side-effects, like writing a physical file. |
1784 |
1745 |
1785 \<^bold>\<open>Workaround:\<close> Copy/paste complete command text from |
1746 \<^bold>\<open>Workaround:\<close> Copy/paste complete command text from elsewhere, or disable |
1786 elsewhere, or disable continuous checking temporarily. |
1747 continuous checking temporarily. |
1787 |
1748 |
1788 \<^item> \<^bold>\<open>Problem:\<close> No direct support to remove document nodes from the |
1749 \<^item> \<^bold>\<open>Problem:\<close> No direct support to remove document nodes from the collection |
1789 collection of theories. |
1750 of theories. |
1790 |
1751 |
1791 \<^bold>\<open>Workaround:\<close> Clear the buffer content of unused files and close |
1752 \<^bold>\<open>Workaround:\<close> Clear the buffer content of unused files and close \<^emph>\<open>without\<close> |
1792 \<^emph>\<open>without\<close> saving changes. |
1753 saving changes. |
1793 |
1754 |
1794 \<^item> \<^bold>\<open>Problem:\<close> Keyboard shortcuts \<^verbatim>\<open>C+PLUS\<close> and |
1755 \<^item> \<^bold>\<open>Problem:\<close> Keyboard shortcuts \<^verbatim>\<open>C+PLUS\<close> and \<^verbatim>\<open>C+MINUS\<close> for adjusting the |
1795 \<^verbatim>\<open>C+MINUS\<close> for adjusting the editor font size depend on |
1756 editor font size depend on platform details and national keyboards. |
1796 platform details and national keyboards. |
1757 |
1797 |
1758 \<^bold>\<open>Workaround:\<close> Rebind keys via \<^emph>\<open>Global Options~/ Shortcuts\<close>. |
1798 \<^bold>\<open>Workaround:\<close> Rebind keys via \<^emph>\<open>Global Options~/ |
|
1799 Shortcuts\<close>. |
|
1800 |
1759 |
1801 \<^item> \<^bold>\<open>Problem:\<close> The Mac OS X key sequence \<^verbatim>\<open>COMMAND+COMMA\<close> for application |
1760 \<^item> \<^bold>\<open>Problem:\<close> The Mac OS X key sequence \<^verbatim>\<open>COMMAND+COMMA\<close> for application |
1802 \<^emph>\<open>Preferences\<close> is in conflict with the |
1761 \<^emph>\<open>Preferences\<close> is in conflict with the jEdit default keyboard shortcut for |
1803 jEdit default keyboard shortcut for \<^emph>\<open>Incremental Search Bar\<close> (action |
1762 \<^emph>\<open>Incremental Search Bar\<close> (action @{action_ref "quick-search"}). |
1804 @{action_ref "quick-search"}). |
1763 |
1805 |
1764 \<^bold>\<open>Workaround:\<close> Rebind key via \<^emph>\<open>Global Options~/ Shortcuts\<close> according to |
1806 \<^bold>\<open>Workaround:\<close> Rebind key via \<^emph>\<open>Global Options~/ |
1765 national keyboard, e.g.\ \<^verbatim>\<open>COMMAND+SLASH\<close> on English ones. |
1807 Shortcuts\<close> according to national keyboard, e.g.\ \<^verbatim>\<open>COMMAND+SLASH\<close> |
|
1808 on English ones. |
|
1809 |
1766 |
1810 \<^item> \<^bold>\<open>Problem:\<close> On Mac OS X with native Apple look-and-feel, some exotic |
1767 \<^item> \<^bold>\<open>Problem:\<close> On Mac OS X with native Apple look-and-feel, some exotic |
1811 national keyboards may cause a conflict of menu accelerator keys with |
1768 national keyboards may cause a conflict of menu accelerator keys with |
1812 regular jEdit key bindings. This leads to duplicate execution of the |
1769 regular jEdit key bindings. This leads to duplicate execution of the |
1813 corresponding jEdit action. |
1770 corresponding jEdit action. |
1814 |
1771 |
1815 \<^bold>\<open>Workaround:\<close> Disable the native Apple menu bar via Java runtime option |
1772 \<^bold>\<open>Workaround:\<close> Disable the native Apple menu bar via Java runtime option |
1816 \<^verbatim>\<open>-Dapple.laf.useScreenMenuBar=false\<close>. |
1773 \<^verbatim>\<open>-Dapple.laf.useScreenMenuBar=false\<close>. |
1817 |
1774 |
1818 \<^item> \<^bold>\<open>Problem:\<close> Mac OS X system fonts sometimes lead to |
1775 \<^item> \<^bold>\<open>Problem:\<close> Mac OS X system fonts sometimes lead to character drop-outs in |
1819 character drop-outs in the main text area. |
1776 the main text area. |
1820 |
1777 |
1821 \<^bold>\<open>Workaround:\<close> Use the default \<^verbatim>\<open>IsabelleText\<close> font. |
1778 \<^bold>\<open>Workaround:\<close> Use the default \<^verbatim>\<open>IsabelleText\<close> font. (Do not install that |
1822 (Do not install that font on the system.) |
1779 font on the system.) |
1823 |
1780 |
1824 \<^item> \<^bold>\<open>Problem:\<close> Some Linux/X11 input methods such as IBus |
1781 \<^item> \<^bold>\<open>Problem:\<close> Some Linux/X11 input methods such as IBus tend to disrupt key |
1825 tend to disrupt key event handling of Java/AWT/Swing. |
1782 event handling of Java/AWT/Swing. |
1826 |
1783 |
1827 \<^bold>\<open>Workaround:\<close> Do not use X11 input methods. Note that environment |
1784 \<^bold>\<open>Workaround:\<close> Do not use X11 input methods. Note that environment variable |
1828 variable \<^verbatim>\<open>XMODIFIERS\<close> is reset by default within Isabelle |
1785 \<^verbatim>\<open>XMODIFIERS\<close> is reset by default within Isabelle settings. |
1829 settings. |
1786 |
1830 |
1787 \<^item> \<^bold>\<open>Problem:\<close> Some Linux/X11 window managers that are not ``re-parenting'' |
1831 \<^item> \<^bold>\<open>Problem:\<close> Some Linux/X11 window managers that are |
1788 cause problems with additional windows opened by Java. This affects either |
1832 not ``re-parenting'' cause problems with additional windows opened |
1789 historic or neo-minimalistic window managers like \<^verbatim>\<open>awesome\<close> or \<^verbatim>\<open>xmonad\<close>. |
1833 by Java. This affects either historic or neo-minimalistic window |
|
1834 managers like \<^verbatim>\<open>awesome\<close> or \<^verbatim>\<open>xmonad\<close>. |
|
1835 |
1790 |
1836 \<^bold>\<open>Workaround:\<close> Use a regular re-parenting X11 window manager. |
1791 \<^bold>\<open>Workaround:\<close> Use a regular re-parenting X11 window manager. |
1837 |
1792 |
1838 \<^item> \<^bold>\<open>Problem:\<close> Various forks of Linux/X11 window managers and |
1793 \<^item> \<^bold>\<open>Problem:\<close> Various forks of Linux/X11 window managers and desktop |
1839 desktop environments (like Gnome) disrupt the handling of menu popups and |
1794 environments (like Gnome) disrupt the handling of menu popups and mouse |
1840 mouse positions of Java/AWT/Swing. |
1795 positions of Java/AWT/Swing. |
1841 |
1796 |
1842 \<^bold>\<open>Workaround:\<close> Use mainstream versions of Linux desktops. |
1797 \<^bold>\<open>Workaround:\<close> Use mainstream versions of Linux desktops. |
1843 |
1798 |
1844 \<^item> \<^bold>\<open>Problem:\<close> Native Windows look-and-feel with global font |
1799 \<^item> \<^bold>\<open>Problem:\<close> Native Windows look-and-feel with global font scaling leads to |
1845 scaling leads to bad GUI rendering of various tree views. |
1800 bad GUI rendering of various tree views. |
1846 |
1801 |
1847 \<^bold>\<open>Workaround:\<close> Use \<^emph>\<open>Metal\<close> look-and-feel and re-adjust its |
1802 \<^bold>\<open>Workaround:\<close> Use \<^emph>\<open>Metal\<close> look-and-feel and re-adjust its primary and |
1848 primary and secondary font as explained in \secref{sec:hdpi}. |
1803 secondary font as explained in \secref{sec:hdpi}. |
1849 |
1804 |
1850 \<^item> \<^bold>\<open>Problem:\<close> Full-screen mode via jEdit action @{action_ref |
1805 \<^item> \<^bold>\<open>Problem:\<close> Full-screen mode via jEdit action @{action_ref |
1851 "toggle-full-screen"} (default keyboard shortcut \<^verbatim>\<open>F11\<close>) works on |
1806 "toggle-full-screen"} (default keyboard shortcut \<^verbatim>\<open>F11\<close>) works on Windows, |
1852 Windows, but not on Mac OS X or various Linux/X11 window managers. |
1807 but not on Mac OS X or various Linux/X11 window managers. |
1853 |
1808 |
1854 \<^bold>\<open>Workaround:\<close> Use native full-screen control of the window |
1809 \<^bold>\<open>Workaround:\<close> Use native full-screen control of the window manager (notably |
1855 manager (notably on Mac OS X). |
1810 on Mac OS X). |
1856 \<close> |
1811 \<close> |
1857 |
1812 |
1858 end |
1813 end |