author | wenzelm |
Thu, 06 Jun 2024 11:53:52 +0200 | |
changeset 80266 | d52be75ae60b |
parent 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 |
72754 | 9 |
val extensions: string list -> Path.T -> Path.T list |
57905
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
10 |
datatype kind = Command_Span of string * Position.T | Ignored_Span | Malformed_Span |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
11 |
datatype span = Span of kind * Token.T list |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
12 |
val kind: span -> kind |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
13 |
val content: span -> Token.T list |
68183
6560324b1e4d
adjust position according to offset of command/exec id;
wenzelm
parents:
68177
diff
changeset
|
14 |
val symbol_length: span -> int option |
6560324b1e4d
adjust position according to offset of command/exec id;
wenzelm
parents:
68177
diff
changeset
|
15 |
val adjust_offsets_kind: (int -> int option) -> kind -> kind |
6560324b1e4d
adjust position according to offset of command/exec id;
wenzelm
parents:
68177
diff
changeset
|
16 |
val adjust_offsets: (int -> int option) -> span -> span |
57905
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
17 |
end; |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
18 |
|
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
19 |
structure Command_Span: COMMAND_SPAN = |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
20 |
struct |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
21 |
|
72754 | 22 |
(* loaded files *) |
23 |
||
24 |
fun extensions exts path = map (fn ext => Path.ext ext path) exts; |
|
25 |
||
26 |
||
27 |
(* span *) |
|
28 |
||
57905
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
29 |
datatype kind = Command_Span of string * Position.T | Ignored_Span | Malformed_Span; |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
30 |
datatype span = Span of kind * Token.T list; |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
31 |
|
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
32 |
fun kind (Span (k, _)) = k; |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
33 |
fun content (Span (_, toks)) = toks; |
68183
6560324b1e4d
adjust position according to offset of command/exec id;
wenzelm
parents:
68177
diff
changeset
|
34 |
val symbol_length = Position.distance_of o Token.range_of o content; |
68177 | 35 |
|
72754 | 36 |
|
37 |
(* presentation positions *) |
|
38 |
||
68183
6560324b1e4d
adjust position according to offset of command/exec id;
wenzelm
parents:
68177
diff
changeset
|
39 |
fun adjust_offsets_kind adjust k = |
6560324b1e4d
adjust position according to offset of command/exec id;
wenzelm
parents:
68177
diff
changeset
|
40 |
(case k of |
6560324b1e4d
adjust position according to offset of command/exec id;
wenzelm
parents:
68177
diff
changeset
|
41 |
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
|
42 |
| _ => k); |
6560324b1e4d
adjust position according to offset of command/exec id;
wenzelm
parents:
68177
diff
changeset
|
43 |
|
6560324b1e4d
adjust position according to offset of command/exec id;
wenzelm
parents:
68177
diff
changeset
|
44 |
fun adjust_offsets adjust (Span (k, toks)) = |
6560324b1e4d
adjust position according to offset of command/exec id;
wenzelm
parents:
68177
diff
changeset
|
45 |
Span (adjust_offsets_kind adjust k, map (Token.adjust_offsets adjust) toks); |
68177 | 46 |
|
57905
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
47 |
end; |