author | wenzelm |
Tue, 21 Oct 2014 17:49:51 +0200 | |
changeset 58749 | 83b0f633190e |
parent 57905 | c0c5652e796e |
child 58923 | cb9b69cca999 |
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 |
val resolve_files: (string -> Path.T * Position.T -> Token.file Exn.result list) -> span -> span |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
14 |
end; |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
15 |
|
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
16 |
structure Command_Span: COMMAND_SPAN = |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
17 |
struct |
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 |
datatype kind = Command_Span of string * Position.T | Ignored_Span | Malformed_Span; |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
20 |
datatype span = Span of kind * Token.T list; |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
21 |
|
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
22 |
fun kind (Span (k, _)) = k; |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
23 |
fun content (Span (_, toks)) = toks; |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
24 |
|
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
25 |
|
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
26 |
(* resolve inlined files *) |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
27 |
|
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
28 |
local |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
29 |
|
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
30 |
fun clean ((i1, t1) :: (i2, t2) :: toks) = |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
31 |
if Token.keyword_with (fn s => s = "%" orelse s = "--") t1 then clean toks |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
32 |
else (i1, t1) :: clean ((i2, t2) :: toks) |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
33 |
| clean toks = toks; |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
34 |
|
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
35 |
fun clean_tokens toks = |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
36 |
((0 upto length toks - 1) ~~ toks) |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
37 |
|> filter (fn (_, tok) => Token.is_proper tok) |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
38 |
|> clean; |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
39 |
|
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
40 |
fun find_file ((_, tok) :: toks) = |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
41 |
if Token.is_command tok then |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
42 |
toks |> get_first (fn (i, tok) => |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
43 |
if Token.is_name tok then |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
44 |
SOME (i, (Path.explode (Token.content_of tok), Token.pos_of tok)) |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
45 |
handle ERROR msg => error (msg ^ Position.here (Token.pos_of tok)) |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
46 |
else NONE) |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
47 |
else NONE |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
48 |
| find_file [] = NONE; |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
49 |
|
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
50 |
in |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
51 |
|
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
52 |
fun resolve_files read_files span = |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
53 |
(case span of |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
54 |
Span (Command_Span (cmd, pos), toks) => |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
55 |
if Keyword.is_theory_load cmd then |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
56 |
(case find_file (clean_tokens toks) of |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
57 |
NONE => error ("Bad file argument of command " ^ quote cmd ^ Position.here pos) |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
58 |
| SOME (i, path) => |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
59 |
let |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
60 |
val toks' = toks |> map_index (fn (j, tok) => |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
61 |
if i = j then Token.put_files (read_files cmd path) tok |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
62 |
else tok); |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
63 |
in Span (Command_Span (cmd, pos), toks') end) |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
64 |
else span |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
65 |
| _ => span); |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
66 |
|
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
67 |
end; |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
68 |
|
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
69 |
end; |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
70 |