-
Notifications
You must be signed in to change notification settings - Fork 2
/
Copy pathcsp-mode.texi
260 lines (191 loc) · 8.22 KB
/
csp-mode.texi
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
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
\input texinfo @c -*-texinfo-*-
@comment %**start of header
@setfilename csp-mode.info
@settitle CSP-Mode V@value{cspver}
@comment %**end of header
@c $Author: rscholz $
@c $Date: 2002/01/01 20:46:33 $
@c $Source: /var/local/cvs/csp-mode/csp-mode.texi,v $
@c $Revision: 1.1.1.1 $
@set cspver 1.0.1
@set docver 2
@set printdate @today{}
@set reldate Nov 2001
@ifinfo
This file documents the major mode csp version @value{cspver} for editing CSP code in FDR2-syntax.
Copyright @copyright{} 2000 Olaf Bergmann, Markus Dahlweid
Permission is granted to make and distribute verbatim copies of this manual
provided the copyright notice and this permission notice are preserved
on all copies (see the GNU General Public License).
@end ifinfo
@titlepage
@title CSP-Mode
@subtitle The Emacs major mode for editing CSP code in FDR2-syntax, Edition @value{docver}
@subtitle @value{reldate}
@author by Olaf Bergmann, Markus Dahlweid
@end titlepage
@node Top, Introduction, (dir), (dir)
@comment node-name, next, previous, up
@menu
* Introduction:: what is csp mode
* Keybindings:: description of the commands and keybindings
* Customizing:: how to change the behaviour of csp
* Bugs:: unfortunately is this page not empty
@end menu
A mode for programming CSP in Emacs.
Designed and written by
@example
Olaf Bergmann bergmann@@informatik.uni-bremen.de
Markus Dahlweid dahlweid@@informatik.uni-bremen.de
Uwe Schulze uschulze@@informatik.uni-bremen.de
@end example
@menu
* Introduction:: what is csp mode
* Keybindings:: description of the commands and keybindings
* Customizing:: how to change the behaviour of csp
* Bugs:: unfortunately is this page not empty
--- The Detailed Node Listing ---
* Introduction:: what is csp mode
* Keybindings:: description of the commands and keybindings
* Customizing:: how to change the behaviour of csp
* Bugs:: unfortunately is this page not empty
Introduction
* History::
@end menu
@node Introduction, Keybindings, Top, Top
@comment node-name, next, previous, up
@chapter Introduction
Csp-Mode is a major mode for use with Emacs.
@menu
* History::
@end menu
@node History, , Introduction, Introduction
@comment node-name, next, previous, up
@section History
In winter 1996/1997 there were some students of computer science at the
University of Bremen, Germany, who felt that there was need of a mode
for editing CSP-code using the ASCII representation for the
FDR2-model-checker.
@node Keybindings, Customizing, Introduction, Top
@comment node-name, next, previous, up
@chapter Commands and keybindings
As usual for common major modes dealing with program languages, there
are some often used keys which take care for correct indentation of
expressions and comments. The indentation itself may be controlled by a
number of parameters we look at in the following chapter.
@itemize @bullet
@item
Pressing @code{TAB} @code{(electric-csp-tab)} as usual indents the current line looking at its
preceding line. Each tab is converted to spaces if and only if @code{csp-untabify} is set to @code{t}.
@item
Pressing @code{LFD} @code{(electric-csp-terminate-line)}indents the current line correctly and terminates it. The next line is indented as well.
@item
@code{C-c C-c} @code{(csp-comment-area)} will comment out the
currently marked area. This is done by inserting the b-style
comment-start-sequence @code{--} at the beginning of each in line in the
current region. If there is already such a character combination,
nothing is inserted. This may cause problems when you press @code{C-c
C-c} being in a block-comment since executing the inverse operation
@code{csp-uncomment-area} will delete all leading
comment-start-sequence characters.
@item
@code{C-c C-u} @code{(csp-uncomment-area)} removes all leading
comment-start-sequence characters in the commented area surrounding the
current position. The first commented line in this area will be
searched. The actual ``Area'' is then delimited by the first and the
last line which have no leading comment-start-sequence (i.e. they even
might be empty).
@item
Pressing @code{;} @code{(electric-csp-semi)} and
@code{csp-auto-newline} is non-nil will cause a semicolon to be
inserted at the current position. After that, the current line is
terminated and the following line will be indented correctly.
@ifinfo
@item
@code{C->} @code{(electric-csp-arrow)} does the same as
@code{electric-csp-semi} described before, but the arrow-operator
@code{->} is inserted at the end of the current line.
@end ifinfo
@iftex
@item
@code{C->} @code{(electric-csp-arrow)} does the same as
@code{electric-csp-semi} described before, but the arrow-operator
@tex
$\rightarrow$ is inserted at the end of the current line.
@end tex
@end iftex
@item
@code{C-c e} @code{(electric-csp-external-choice)} inserts an external
choice operator @code{[]} at current position.
@item
@code{C-c l} @code{(electric-csp-interleave)} inserts an interleave
operator @code{|||} at current position.
@item
@code{C-c ~} or @code{C-c i} @code{(electric-csp-internal-choice)}
inserts an internal choice operator @code{|~|} at current position.
@item
@code{C-c |} or @code{C-c p} @code{(electric-csp-sync)} inserts a
synchronisation operator @code{[| |]} at current position and places
the point centered between the two vertical bars.
@item
@code{C-c @{} or @code{C-c s} @code{(electric-csp-channel-set)}
inserts a set operator @code{@{| |@}} at current position and places
the point centered between the two vertical bars.
@item
@code{C-c C-v} @code{(csp-validate)} invokes the validation command
specified in @code{csp-validate-command}. If errors occurred, you can
use @code{next-error} to find the actual code line corresponding to the
line given in the message.
@end itemize
@node Customizing, Bugs, Keybindings, Top
@comment node-name, next, previous, up
@chapter Customizing
This chapter describes the variables you can use to customize the
behaviour of csp mode. At least there are switches to determine
whether lines are allowed to be indented or tabs to be converted into
spaces automatically.
@itemize @bullet
@item
@code{csp-indent-level} is an integer-value denoting the amount of
spaces which are inserted when a line is indented with respect to a
containig block. Its default value is @code{3}.
@item
If @code{csp-auto-newline} is non-nil, this means that there will be
inserted a newline automatically after inserting a semicolon or the
array-operator. The default is set to @code{t}.
@item
@code{csp-tab-always-indent} means that a @code{TAB} in Csp-mode
should always reindent the current line, regardless of where in the line
point is when the @code{TAB} command is used. Default is @code{t}.
@item
@code{csp-untabify} specifies whether tabs should be converted into
spaces or not. If @code{t} which is the default value, tabs will be
converted.
@item
@code{csp-validate-error-regexps} contains an alist of regular
expressions to recognize error messages from @code{csp-validate}.
@item
@code{csp-offer-save}. If this is @code{t}, invocation of
@code{csp-validate} will cause Emacs to ask whether modified buffers
should be saved before executing @code{csp-validate}. Default is
@code{t}.
@item
@code{csp-validate-command} contains the shell-command to validate the
CSP program in current buffer. The file name of the buffer will be
appended, seperated by a space.
@end itemize
@node Bugs, , Customizing, Top
@comment node-name, next, previous, up
@chapter Bugs
There are several bugs known by now, but none of them are severe. As for
the most syntax-controlled programming modes, correct statements will be
indented correctly, but the result of indenting wrong statements will
sometimes have funny effects. Fortunately, most of them indicate
incorrect use of the language's constructs, so this will help you not to
make too many syntactic errors. However, there still remain some dirty
effects even if typed syntax is correct. Here is a list of the known bugs:
@itemize @bullet
@item
Block comments are not recognized correctly if there is a normal comment starting with @code{--} in it.
@end itemize
@bye