|
1 (* Title: Pure/Thy/thy_edit.ML |
|
2 ID: $Id$ |
|
3 Author: Makarius |
|
4 |
|
5 Basic editing of theory sources. |
|
6 *) |
|
7 |
|
8 signature THY_EDIT = |
|
9 sig |
|
10 val read_tokens: Position.T -> (string, 'a) Source.source -> OuterLex.token list |
|
11 datatype item = |
|
12 Whitespace of OuterLex.token list | |
|
13 Junk of OuterLex.token list | |
|
14 Commandspan of string * OuterLex.token list |
|
15 val read_items: Position.T -> (string, 'a) Source.source -> item list |
|
16 val present_html: Path.T -> Path.T -> unit |
|
17 end; |
|
18 |
|
19 structure ThyEdit: THY_EDIT = |
|
20 struct |
|
21 |
|
22 structure T = OuterLex; |
|
23 structure P = OuterParse; |
|
24 |
|
25 |
|
26 (* tokens *) |
|
27 |
|
28 fun token_source pos src = |
|
29 Symbol.source true src |
|
30 |> T.source (SOME false) OuterSyntax.get_lexicons pos; |
|
31 |
|
32 fun read_tokens pos src = Source.exhaust (token_source pos src); |
|
33 |
|
34 |
|
35 (* items *) |
|
36 |
|
37 datatype item = |
|
38 Whitespace of T.token list | |
|
39 Junk of T.token list | |
|
40 Commandspan of string * T.token list; |
|
41 |
|
42 local |
|
43 |
|
44 val whitespace = Scan.many1 (T.is_kind T.Space orf T.is_kind T.Comment); |
|
45 val before_command = Scan.optional whitespace [] -- Scan.ahead P.command; |
|
46 val body = Scan.repeat1 (Scan.unless before_command P.not_eof); |
|
47 |
|
48 val item = |
|
49 whitespace >> Whitespace || |
|
50 body >> Junk || |
|
51 before_command -- P.not_eof -- Scan.optional body [] |
|
52 >> (fn (((ws, name), c), bs) => Commandspan (name, ws @ [c] @ bs)); |
|
53 |
|
54 in |
|
55 |
|
56 fun item_source src = src |
|
57 |> Source.source T.stopper (Scan.bulk item) NONE; |
|
58 |
|
59 end; |
|
60 |
|
61 fun read_items pos src = |
|
62 Source.exhaust (item_source (token_source pos src)); |
|
63 |
|
64 |
|
65 (* presentation *) |
|
66 |
|
67 local |
|
68 |
|
69 val token_kind_markup = |
|
70 fn T.Command => (Markup.commandN, []) |
|
71 | T.Keyword => (Markup.keywordN, []) |
|
72 | T.Ident => Markup.ident |
|
73 | T.LongIdent => Markup.ident |
|
74 | T.SymIdent => Markup.ident |
|
75 | T.Var => Markup.ident |
|
76 | T.TypeIdent => Markup.ident |
|
77 | T.TypeVar => Markup.ident |
|
78 | T.Nat => Markup.ident |
|
79 | T.String => Markup.string |
|
80 | T.AltString => Markup.altstring |
|
81 | T.Verbatim => Markup.verbatim |
|
82 | T.Space => Markup.space |
|
83 | T.Comment => Markup.comment |
|
84 | T.Sync => Markup.control |
|
85 | T.Malformed _ => Markup.malformed |
|
86 | T.EOF => Markup.control; |
|
87 |
|
88 fun present_token tok = |
|
89 Markup.enclose (token_kind_markup (T.kind_of tok)) (Output.output (T.unparse tok)); |
|
90 |
|
91 val present_tokens = implode o map present_token; |
|
92 |
|
93 fun present_item (Whitespace toks) = Markup.enclose Markup.whitespace (present_tokens toks) |
|
94 | present_item (Junk toks) = Markup.enclose Markup.junk (present_tokens toks) |
|
95 | present_item (Commandspan (name, toks)) = |
|
96 Markup.enclose (Markup.commandspan name) (present_tokens toks); |
|
97 |
|
98 val present_items = implode o map present_item; |
|
99 |
|
100 in |
|
101 |
|
102 fun present_html inpath outpath = |
|
103 read_items (Position.path inpath) (Source.of_string (File.read inpath)) |
|
104 |> HTML.html_mode present_items |
|
105 |> enclose |
|
106 (HTML.begin_document (Path.implode (Path.base inpath)) ^ "<div class=\"source\"><pre>") |
|
107 ("</pre></div>" ^ HTML.end_document) |
|
108 |> File.write outpath; |
|
109 |
|
110 end |
|
111 |
|
112 end; |