blob: 3a0daff60a06fa3579fdd926e2f0104ba5a06a5b (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
|
Screenshot notes.
=================
All in 80x40 sized XEmacs.
* Isabelle: Dagstuhl HOLCF example. Show theory file on screen too.
* Isar: Example Group.thy is modified version with extra X-Symbol line:
syntax (xsymbols)
"op *" :: "['a::times, 'a] => 'a" (infixl "\\<bullet>" 70);
And uses of * replaced with \\<bullet>.
* Coq: Example from Sorting library. Multiple frame mode, X-Symbols,
also with Netscape.
Most shots scaled to 0.2 or thereabouts to give nice sized thumbnail.
-----------------------------------------------------------------
Regenerating screen shot in html/IsaPGscreen.jpg:
30x80 sized XEmacs. Visit isa/example.ML.
Click on "next" button four times.
Drag middle modeline to display whole proof script.
Move point to end of locked region.
Grab with gimp, Xtns -> Screen Shot.
Save with default quality settings.
-----------------------------------------------------------------
|
