author | wenzelm |
Fri, 06 Sep 2019 18:59:24 +0200 | |
changeset 70664 | 2bd9e30183b1 |
parent 68183 | 6560324b1e4d |
child 72754 | 1456c5747416 |
permissions | -rw-r--r-- |
57905
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
1 |
(* Title: Pure/PIDE/command_span.ML |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
2 |
Author: Makarius |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
3 |
|
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
4 |
Syntactic representation of command spans. |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
5 |
*) |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
6 |
|
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
7 |
signature COMMAND_SPAN = |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
8 |
sig |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
9 |
datatype kind = Command_Span of string * Position.T | Ignored_Span | Malformed_Span |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
10 |
datatype span = Span of kind * Token.T list |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
11 |
val kind: span -> kind |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
12 |
val content: span -> Token.T list |
68183
6560324b1e4d
adjust position according to offset of command/exec id;
wenzelm
parents:
68177
diff
changeset
|
13 |
val symbol_length: span -> int option |
6560324b1e4d
adjust position according to offset of command/exec id;
wenzelm
parents:
68177
diff
changeset
|
14 |
val adjust_offsets_kind: (int -> int option) -> kind -> kind |
6560324b1e4d
adjust position according to offset of command/exec id;
wenzelm
parents:
68177
diff
changeset
|
15 |
val adjust_offsets: (int -> int option) -> span -> span |
57905
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
16 |
end; |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
17 |
|
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
18 |
structure Command_Span: COMMAND_SPAN = |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
19 |
struct |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
20 |
|
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
21 |
datatype kind = Command_Span of string * Position.T | Ignored_Span | Malformed_Span; |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
22 |
datatype span = Span of kind * Token.T list; |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
23 |
|
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
24 |
fun kind (Span (k, _)) = k; |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
25 |
fun content (Span (_, toks)) = toks; |
68183
6560324b1e4d
adjust position according to offset of command/exec id;
wenzelm
parents:
68177
diff
changeset
|
26 |
val symbol_length = Position.distance_of o Token.range_of o content; |
68177 | 27 |
|
68183
6560324b1e4d
adjust position according to offset of command/exec id;
wenzelm
parents:
68177
diff
changeset
|
28 |
fun adjust_offsets_kind adjust k = |
6560324b1e4d
adjust position according to offset of command/exec id;
wenzelm
parents:
68177
diff
changeset
|
29 |
(case k of |
6560324b1e4d
adjust position according to offset of command/exec id;
wenzelm
parents:
68177
diff
changeset
|
30 |
Command_Span (name, pos) => Command_Span (name, Position.adjust_offsets adjust pos) |
6560324b1e4d
adjust position according to offset of command/exec id;
wenzelm
parents:
68177
diff
changeset
|
31 |
| _ => k); |
6560324b1e4d
adjust position according to offset of command/exec id;
wenzelm
parents:
68177
diff
changeset
|
32 |
|
6560324b1e4d
adjust position according to offset of command/exec id;
wenzelm
parents:
68177
diff
changeset
|
33 |
fun adjust_offsets adjust (Span (k, toks)) = |
6560324b1e4d
adjust position according to offset of command/exec id;
wenzelm
parents:
68177
diff
changeset
|
34 |
Span (adjust_offsets_kind adjust k, map (Token.adjust_offsets adjust) toks); |
68177 | 35 |
|
57905
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
36 |
end; |