isabelle: src/Tools/jEdit/README.html@e7fdb008aa7d (annotated)

41628 ed4d793f0c26 improved README -- Isabelle symbols and fonts; wenzelm parents: 41538 diff changeset	1	<?xml version="1.0" encoding="UTF-8" ?>
39591 a43a723753e6 more content for Session_Dockable; wenzelm parents: diff changeset	2	<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
a43a723753e6 more content for Session_Dockable; wenzelm parents: diff changeset	3	<html xmlns="http://www.w3.org/1999/xhtml">
a43a723753e6 more content for Session_Dockable; wenzelm parents: diff changeset	4
a43a723753e6 more content for Session_Dockable; wenzelm parents: diff changeset	5	<head>
a43a723753e6 more content for Session_Dockable; wenzelm parents: diff changeset	6	<meta http-equiv="Content-Type" content="text/html; charset=utf-8"/>
43470 3d42dea16357 explain special control symbols; wenzelm parents: 43287 diff changeset	7	<style type="text/css" media="screen">
43509 4414c8b02bf9 prefer STIXGeneral -- hard to tell if better or worse; wenzelm parents: 43472 diff changeset	8	body { font-family: STIXGeneral, IsabelleText; font-size: 14pt; }
43470 3d42dea16357 explain special control symbols; wenzelm parents: 43287 diff changeset	9	</style>
39738 909ee37c34c1 tuned README; wenzelm parents: 39736 diff changeset	10	<title>Notes on the Isabelle/jEdit Prover IDE</title>
39591 a43a723753e6 more content for Session_Dockable; wenzelm parents: diff changeset	11	</head>
a43a723753e6 more content for Session_Dockable; wenzelm parents: diff changeset	12
a43a723753e6 more content for Session_Dockable; wenzelm parents: diff changeset	13	<body>
a43a723753e6 more content for Session_Dockable; wenzelm parents: diff changeset	14
41628 ed4d793f0c26 improved README -- Isabelle symbols and fonts; wenzelm parents: 41538 diff changeset	15	<h2>The Isabelle/jEdit Prover IDE</h2>
39591 a43a723753e6 more content for Session_Dockable; wenzelm parents: diff changeset	16
a43a723753e6 more content for Session_Dockable; wenzelm parents: diff changeset	17	<ul>
a43a723753e6 more content for Session_Dockable; wenzelm parents: diff changeset	18
39738 909ee37c34c1 tuned README; wenzelm parents: 39736 diff changeset	19	<li>The original jEdit look-and-feel is generally preserved, although
909ee37c34c1 tuned README; wenzelm parents: 39736 diff changeset	20	some default properties have been changed to accommodate Isabelle
40894 a0f7ebe8f7a7 tuned README; wenzelm parents: 39815 diff changeset	21	(e.g. the text area font).</li>
39736 e19cece7d18a tuned README; wenzelm parents: 39591 diff changeset	22
39738 909ee37c34c1 tuned README; wenzelm parents: 39736 diff changeset	23	<li>Formal Isabelle/Isar text is checked asynchronously while editing.
909ee37c34c1 tuned README; wenzelm parents: 39736 diff changeset	24	The user is in full command of the editor, and the prover refrains
909ee37c34c1 tuned README; wenzelm parents: 39736 diff changeset	25	from locking portions of the buffer etc.</li>
39591 a43a723753e6 more content for Session_Dockable; wenzelm parents: diff changeset	26
39738 909ee37c34c1 tuned README; wenzelm parents: 39736 diff changeset	27	<li>Prover feedback works via tooltips, syntax highlighting, colors,
909ee37c34c1 tuned README; wenzelm parents: 39736 diff changeset	28	boxes etc. based on semantic markup provided by Isabelle in the
909ee37c34c1 tuned README; wenzelm parents: 39736 diff changeset	29	background.</li>
909ee37c34c1 tuned README; wenzelm parents: 39736 diff changeset	30
909ee37c34c1 tuned README; wenzelm parents: 39736 diff changeset	31	<li>Using the mouse together with the modifier key <tt>C</tt>
909ee37c34c1 tuned README; wenzelm parents: 39736 diff changeset	32	(<tt>CONTROL</tt> on Linux or Windows,
39736 e19cece7d18a tuned README; wenzelm parents: 39591 diff changeset	33	<tt>COMMAND</tt> on Mac OS) exposes additional information.</li>
e19cece7d18a tuned README; wenzelm parents: 39591 diff changeset	34
39738 909ee37c34c1 tuned README; wenzelm parents: 39736 diff changeset	35	<li>Dockable panels (e.g. <em>Output</em>) are managed as independent
909ee37c34c1 tuned README; wenzelm parents: 39736 diff changeset	36	windows by jEdit, which also allows multiple instances.</li>
39591 a43a723753e6 more content for Session_Dockable; wenzelm parents: diff changeset	37
a43a723753e6 more content for Session_Dockable; wenzelm parents: diff changeset	38	</ul>
a43a723753e6 more content for Session_Dockable; wenzelm parents: diff changeset	39
41628 ed4d793f0c26 improved README -- Isabelle symbols and fonts; wenzelm parents: 41538 diff changeset	40
ed4d793f0c26 improved README -- Isabelle symbols and fonts; wenzelm parents: 41538 diff changeset	41	<h2>Isabelle symbols and fonts</h2>
ed4d793f0c26 improved README -- Isabelle symbols and fonts; wenzelm parents: 41538 diff changeset	42
ed4d793f0c26 improved README -- Isabelle symbols and fonts; wenzelm parents: 41538 diff changeset	43	<ul>
ed4d793f0c26 improved README -- Isabelle symbols and fonts; wenzelm parents: 41538 diff changeset	44
ed4d793f0c26 improved README -- Isabelle symbols and fonts; wenzelm parents: 41538 diff changeset	45	<li>Isabelle supports infinitely many symbols:<br/>
43472 ac6db8f44e5d literal unicode in README.html allows to copy/paste from Lobo output; wenzelm parents: 43470 diff changeset	46	α, β, γ, …<br/>
ac6db8f44e5d literal unicode in README.html allows to copy/paste from Lobo output; wenzelm parents: 43470 diff changeset	47	∀, ∃, ∨, ∧, ⟶, ⟷, …<br/>
ac6db8f44e5d literal unicode in README.html allows to copy/paste from Lobo output; wenzelm parents: 43470 diff changeset	48	≤, ≥, ⊓, ⊔, …<br/>
ac6db8f44e5d literal unicode in README.html allows to copy/paste from Lobo output; wenzelm parents: 43470 diff changeset	49	ℵ, △, ∇, …<br/>
ac6db8f44e5d literal unicode in README.html allows to copy/paste from Lobo output; wenzelm parents: 43470 diff changeset	50	<tt>\<foo></tt>, <tt>\<bar></tt>, <tt>\<baz></tt>, …<br/>
41628 ed4d793f0c26 improved README -- Isabelle symbols and fonts; wenzelm parents: 41538 diff changeset	51	</li>
ed4d793f0c26 improved README -- Isabelle symbols and fonts; wenzelm parents: 41538 diff changeset	52
43470 3d42dea16357 explain special control symbols; wenzelm parents: 43287 diff changeset	53	<li>There are some special control symbols to modify the style of a
3d42dea16357 explain special control symbols; wenzelm parents: 43287 diff changeset	54	<em>single</em> symbol:<br/>
43472 ac6db8f44e5d literal unicode in README.html allows to copy/paste from Lobo output; wenzelm parents: 43470 diff changeset	55	⇩ subscript<br/>
ac6db8f44e5d literal unicode in README.html allows to copy/paste from Lobo output; wenzelm parents: 43470 diff changeset	56	⇧ superscript<br/>
ac6db8f44e5d literal unicode in README.html allows to copy/paste from Lobo output; wenzelm parents: 43470 diff changeset	57	⇣ subscript within identifier<br/>
ac6db8f44e5d literal unicode in README.html allows to copy/paste from Lobo output; wenzelm parents: 43470 diff changeset	58	⇡ superscript within identifier<br/>
ac6db8f44e5d literal unicode in README.html allows to copy/paste from Lobo output; wenzelm parents: 43470 diff changeset	59	❙ bold face</li>
43470 3d42dea16357 explain special control symbols; wenzelm parents: 43287 diff changeset	60
41628 ed4d793f0c26 improved README -- Isabelle symbols and fonts; wenzelm parents: 41538 diff changeset	61	<li>A default mapping relates some Isabelle symbols to Unicode points
ed4d793f0c26 improved README -- Isabelle symbols and fonts; wenzelm parents: 41538 diff changeset	62	(see <tt>$ISABELLE_HOME/etc/symbols</tt> and <tt>$ISABELLE_HOME_USER/etc/symbols</tt>).
ed4d793f0c26 improved README -- Isabelle symbols and fonts; wenzelm parents: 41538 diff changeset	63	</li>
ed4d793f0c26 improved README -- Isabelle symbols and fonts; wenzelm parents: 41538 diff changeset	64
ed4d793f0c26 improved README -- Isabelle symbols and fonts; wenzelm parents: 41538 diff changeset	65	<li>The <em>IsabelleText</em> font ensures that Unicode points are actually
ed4d793f0c26 improved README -- Isabelle symbols and fonts; wenzelm parents: 41538 diff changeset	66	seen on the screen (or printer).
ed4d793f0c26 improved README -- Isabelle symbols and fonts; wenzelm parents: 41538 diff changeset	67	</li>
ed4d793f0c26 improved README -- Isabelle symbols and fonts; wenzelm parents: 41538 diff changeset	68
ed4d793f0c26 improved README -- Isabelle symbols and fonts; wenzelm parents: 41538 diff changeset	69	<li>Input methods:
ed4d793f0c26 improved README -- Isabelle symbols and fonts; wenzelm parents: 41538 diff changeset	70	<ul>
ed4d793f0c26 improved README -- Isabelle symbols and fonts; wenzelm parents: 41538 diff changeset	71	<li>copy/paste from decoded source files</li>
ed4d793f0c26 improved README -- Isabelle symbols and fonts; wenzelm parents: 41538 diff changeset	72	<li>copy/paste from prover output</li>
ed4d793f0c26 improved README -- Isabelle symbols and fonts; wenzelm parents: 41538 diff changeset	73	<li>completion provided by Isabelle plugin, e.g.<br/>
ed4d793f0c26 improved README -- Isabelle symbols and fonts; wenzelm parents: 41538 diff changeset	74
ed4d793f0c26 improved README -- Isabelle symbols and fonts; wenzelm parents: 41538 diff changeset	75	<table border="1">
ed4d793f0c26 improved README -- Isabelle symbols and fonts; wenzelm parents: 41538 diff changeset	76	<tr><th><b>name</b></th> <th><b>abbreviation</b></th> <th><b>symbol</b></th></tr>
ed4d793f0c26 improved README -- Isabelle symbols and fonts; wenzelm parents: 41538 diff changeset	77
43472 ac6db8f44e5d literal unicode in README.html allows to copy/paste from Lobo output; wenzelm parents: 43470 diff changeset	78	<tr><td>lambda</td> <td><tt>%</tt></td> <td>λ</td></tr>
ac6db8f44e5d literal unicode in README.html allows to copy/paste from Lobo output; wenzelm parents: 43470 diff changeset	79	<tr><td>Rightarrow</td> <td><tt>=></tt></td> <td>⇒</td></tr>
ac6db8f44e5d literal unicode in README.html allows to copy/paste from Lobo output; wenzelm parents: 43470 diff changeset	80	<tr><td>Longrightarrow</td> <td><tt>==></tt></td> <td>⟹</td></tr>
41628 ed4d793f0c26 improved README -- Isabelle symbols and fonts; wenzelm parents: 41538 diff changeset	81
43472 ac6db8f44e5d literal unicode in README.html allows to copy/paste from Lobo output; wenzelm parents: 43470 diff changeset	82	<tr><td>And</td> <td><tt>!!</tt></td> <td>⋀</td></tr>
ac6db8f44e5d literal unicode in README.html allows to copy/paste from Lobo output; wenzelm parents: 43470 diff changeset	83	<tr><td>equiv</td> <td><tt>==</tt></td> <td>≡</td></tr>
41628 ed4d793f0c26 improved README -- Isabelle symbols and fonts; wenzelm parents: 41538 diff changeset	84
43472 ac6db8f44e5d literal unicode in README.html allows to copy/paste from Lobo output; wenzelm parents: 43470 diff changeset	85	<tr><td>forall</td> <td><tt>!</tt></td> <td>∀</td></tr>
ac6db8f44e5d literal unicode in README.html allows to copy/paste from Lobo output; wenzelm parents: 43470 diff changeset	86	<tr><td>exists</td> <td><tt>?</tt></td> <td>∃</td></tr>
ac6db8f44e5d literal unicode in README.html allows to copy/paste from Lobo output; wenzelm parents: 43470 diff changeset	87	<tr><td>longrightarrow</td> <td><tt>--></tt></td> <td>⟶</td></tr>
ac6db8f44e5d literal unicode in README.html allows to copy/paste from Lobo output; wenzelm parents: 43470 diff changeset	88	<tr><td>and</td> <td><tt>/\</tt></td> <td>∧</td></tr>
ac6db8f44e5d literal unicode in README.html allows to copy/paste from Lobo output; wenzelm parents: 43470 diff changeset	89	<tr><td>or</td> <td><tt>\/</tt></td> <td>∨</td></tr>
ac6db8f44e5d literal unicode in README.html allows to copy/paste from Lobo output; wenzelm parents: 43470 diff changeset	90	<tr><td>not</td> <td><tt>~ </tt></td> <td>¬</td></tr>
ac6db8f44e5d literal unicode in README.html allows to copy/paste from Lobo output; wenzelm parents: 43470 diff changeset	91	<tr><td>noteq</td> <td><tt>~=</tt></td> <td>≠</td></tr>
ac6db8f44e5d literal unicode in README.html allows to copy/paste from Lobo output; wenzelm parents: 43470 diff changeset	92	<tr><td>in</td> <td><tt>:</tt></td> <td>∈</td></tr>
ac6db8f44e5d literal unicode in README.html allows to copy/paste from Lobo output; wenzelm parents: 43470 diff changeset	93	<tr><td>notin</td> <td><tt>~:</tt></td> <td>∉</td></tr>
43470 3d42dea16357 explain special control symbols; wenzelm parents: 43287 diff changeset	94
43472 ac6db8f44e5d literal unicode in README.html allows to copy/paste from Lobo output; wenzelm parents: 43470 diff changeset	95	<tr><td>sub</td> <td><tt>=_</tt></td> <td>⇩</td></tr>
ac6db8f44e5d literal unicode in README.html allows to copy/paste from Lobo output; wenzelm parents: 43470 diff changeset	96	<tr><td>sup</td> <td><tt>=^</tt></td> <td>⇧</td></tr>
ac6db8f44e5d literal unicode in README.html allows to copy/paste from Lobo output; wenzelm parents: 43470 diff changeset	97	<tr><td>isup</td> <td><tt>-_</tt></td> <td>⇣</td></tr>
ac6db8f44e5d literal unicode in README.html allows to copy/paste from Lobo output; wenzelm parents: 43470 diff changeset	98	<tr><td>isub</td> <td><tt>-^</tt></td> <td>⇡</td></tr>
ac6db8f44e5d literal unicode in README.html allows to copy/paste from Lobo output; wenzelm parents: 43470 diff changeset	99	<tr><td>bold</td> <td><tt>-.</tt></td> <td>❙</td></tr>
43470 3d42dea16357 explain special control symbols; wenzelm parents: 43287 diff changeset	100
41628 ed4d793f0c26 improved README -- Isabelle symbols and fonts; wenzelm parents: 41538 diff changeset	101	</table>
ed4d793f0c26 improved README -- Isabelle symbols and fonts; wenzelm parents: 41538 diff changeset	102	</li>
ed4d793f0c26 improved README -- Isabelle symbols and fonts; wenzelm parents: 41538 diff changeset	103	</ul>
ed4d793f0c26 improved README -- Isabelle symbols and fonts; wenzelm parents: 41538 diff changeset	104	</li>
ed4d793f0c26 improved README -- Isabelle symbols and fonts; wenzelm parents: 41538 diff changeset	105
ed4d793f0c26 improved README -- Isabelle symbols and fonts; wenzelm parents: 41538 diff changeset	106	<li><b>NOTE:</b> The above abbreviations refer to the input method.
ed4d793f0c26 improved README -- Isabelle symbols and fonts; wenzelm parents: 41538 diff changeset	107	The logical notation provides ASCII alternatives that often
ed4d793f0c26 improved README -- Isabelle symbols and fonts; wenzelm parents: 41538 diff changeset	108	coincide, but deviate occasionally.
ed4d793f0c26 improved README -- Isabelle symbols and fonts; wenzelm parents: 41538 diff changeset	109	</li>
ed4d793f0c26 improved README -- Isabelle symbols and fonts; wenzelm parents: 41538 diff changeset	110
ed4d793f0c26 improved README -- Isabelle symbols and fonts; wenzelm parents: 41538 diff changeset	111	<li><b>NOTE:</b> Generic jEdit abbreviations or plugins perform similar
ed4d793f0c26 improved README -- Isabelle symbols and fonts; wenzelm parents: 41538 diff changeset	112	source replacement operations; this works for Isabelle as long
ed4d793f0c26 improved README -- Isabelle symbols and fonts; wenzelm parents: 41538 diff changeset	113	as the Unicode sequences coincide with the symbol mapping.
ed4d793f0c26 improved README -- Isabelle symbols and fonts; wenzelm parents: 41538 diff changeset	114	</li>
ed4d793f0c26 improved README -- Isabelle symbols and fonts; wenzelm parents: 41538 diff changeset	115
ed4d793f0c26 improved README -- Isabelle symbols and fonts; wenzelm parents: 41538 diff changeset	116	</ul>
ed4d793f0c26 improved README -- Isabelle symbols and fonts; wenzelm parents: 41538 diff changeset	117
ed4d793f0c26 improved README -- Isabelle symbols and fonts; wenzelm parents: 41538 diff changeset	118
41538 d060ccad02bd updated Isabelle/jEdit limitations and workarounds; wenzelm parents: 40894 diff changeset	119	<h2>Limitations and workrounds (January 2011)</h2>
d060ccad02bd updated Isabelle/jEdit limitations and workarounds; wenzelm parents: 40894 diff changeset	120
d060ccad02bd updated Isabelle/jEdit limitations and workarounds; wenzelm parents: 40894 diff changeset	121	<ul>
d060ccad02bd updated Isabelle/jEdit limitations and workarounds; wenzelm parents: 40894 diff changeset	122	<li>No way to start/stop prover or switch to a different logic.<br/>
d060ccad02bd updated Isabelle/jEdit limitations and workarounds; wenzelm parents: 40894 diff changeset	123	<em>Workaround:</em> Change options and restart editor.</li>
d060ccad02bd updated Isabelle/jEdit limitations and workarounds; wenzelm parents: 40894 diff changeset	124
44203 77881904ee91 updated README; wenzelm parents: 43509 diff changeset	125	<li>Limited support for dependencies between multiple theory buffers.<br/>
77881904ee91 updated README; wenzelm parents: 43509 diff changeset	126	<em>Workaround:</em> Load required files manually.</li>
41538 d060ccad02bd updated Isabelle/jEdit limitations and workarounds; wenzelm parents: 40894 diff changeset	127
d060ccad02bd updated Isabelle/jEdit limitations and workarounds; wenzelm parents: 40894 diff changeset	128	<li>No reclaiming of old/unused document versions in prover or
d060ccad02bd updated Isabelle/jEdit limitations and workarounds; wenzelm parents: 40894 diff changeset	129	editor.<br/>
d060ccad02bd updated Isabelle/jEdit limitations and workarounds; wenzelm parents: 40894 diff changeset	130	<em>Workaround:</em> Avoid large files; restart after a few hours of use.</li>
d060ccad02bd updated Isabelle/jEdit limitations and workarounds; wenzelm parents: 40894 diff changeset	131
d060ccad02bd updated Isabelle/jEdit limitations and workarounds; wenzelm parents: 40894 diff changeset	132	<li>Incremental reparsing sometimes produces unexpected command
d060ccad02bd updated Isabelle/jEdit limitations and workarounds; wenzelm parents: 40894 diff changeset	133	spans.<br/>
d060ccad02bd updated Isabelle/jEdit limitations and workarounds; wenzelm parents: 40894 diff changeset	134	<em>Workaround:</em> Cut/paste larger parts or reload buffer.</li>
d060ccad02bd updated Isabelle/jEdit limitations and workarounds; wenzelm parents: 40894 diff changeset	135
d060ccad02bd updated Isabelle/jEdit limitations and workarounds; wenzelm parents: 40894 diff changeset	136	<li>Command execution sometimes gets stuck (purple background).<br/>
d060ccad02bd updated Isabelle/jEdit limitations and workarounds; wenzelm parents: 40894 diff changeset	137	<em>Workaround:</em> Force reparsing as above.</li>
d060ccad02bd updated Isabelle/jEdit limitations and workarounds; wenzelm parents: 40894 diff changeset	138
d060ccad02bd updated Isabelle/jEdit limitations and workarounds; wenzelm parents: 40894 diff changeset	139	<li>Odd behavior of some diagnostic commands, notably those
d060ccad02bd updated Isabelle/jEdit limitations and workarounds; wenzelm parents: 40894 diff changeset	140	starting external processes asynchronously
d060ccad02bd updated Isabelle/jEdit limitations and workarounds; wenzelm parents: 40894 diff changeset	141	(e.g. <tt>thy_deps</tt>, <tt>sledgehammer</tt>).<br/>
d060ccad02bd updated Isabelle/jEdit limitations and workarounds; wenzelm parents: 40894 diff changeset	142	<em>Workaround:</em> Avoid such commands.</li>
d060ccad02bd updated Isabelle/jEdit limitations and workarounds; wenzelm parents: 40894 diff changeset	143
d060ccad02bd updated Isabelle/jEdit limitations and workarounds; wenzelm parents: 40894 diff changeset	144	<li>No support for non-local markup, e.g. commands reporting on
d060ccad02bd updated Isabelle/jEdit limitations and workarounds; wenzelm parents: 40894 diff changeset	145	previous commands (proof end on proof head), or markup produced by
d060ccad02bd updated Isabelle/jEdit limitations and workarounds; wenzelm parents: 40894 diff changeset	146	loading external files.</li>
d060ccad02bd updated Isabelle/jEdit limitations and workarounds; wenzelm parents: 40894 diff changeset	147
d060ccad02bd updated Isabelle/jEdit limitations and workarounds; wenzelm parents: 40894 diff changeset	148	<li>General lack of various conveniences known from Proof
d060ccad02bd updated Isabelle/jEdit limitations and workarounds; wenzelm parents: 40894 diff changeset	149	General.</li>
d060ccad02bd updated Isabelle/jEdit limitations and workarounds; wenzelm parents: 40894 diff changeset	150	</ul>
d060ccad02bd updated Isabelle/jEdit limitations and workarounds; wenzelm parents: 40894 diff changeset	151
39591 a43a723753e6 more content for Session_Dockable; wenzelm parents: diff changeset	152	</body>
a43a723753e6 more content for Session_Dockable; wenzelm parents: diff changeset	153	</html>
a43a723753e6 more content for Session_Dockable; wenzelm parents: diff changeset	154

author	wenzelm
	Tue, 23 Aug 2011 12:20:12 +0200
changeset 44385	e7fdb008aa7d
parent 44203	77881904ee91
child 44700	f4b42f310f86
permissions	-rw-r--r--