author | wenzelm |
Mon, 03 Apr 2017 14:29:44 +0200 | |
changeset 65358 | e345e9420109 |
parent 59689 | 7968c57ea240 |
child 68177 | 6e40f5d43936 |
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 |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
13 |
end; |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
14 |
|
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
15 |
structure Command_Span: COMMAND_SPAN = |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
16 |
struct |
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 |
datatype kind = Command_Span of string * Position.T | Ignored_Span | Malformed_Span; |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
19 |
datatype span = Span of kind * Token.T list; |
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 |
fun kind (Span (k, _)) = k; |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
22 |
fun content (Span (_, toks)) = toks; |
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 |
end; |