90
|
1 |
|
24
|
2 |
structure Chunks =
|
|
3 |
struct
|
|
4 |
|
90
|
5 |
(* rebuilding the output_list function from ThyOutput in order to *)
|
117
|
6 |
(* enable the options [gray, linenos] *)
|
90
|
7 |
|
|
8 |
val gray = ref false;
|
117
|
9 |
val linenos = ref false
|
90
|
10 |
|
|
11 |
fun boolean "" = true
|
|
12 |
| boolean "true" = true
|
|
13 |
| boolean "false" = false
|
|
14 |
| boolean s = error ("Bad boolean value: " ^ quote s);
|
|
15 |
|
|
16 |
fun output_list pretty src ctxt xs =
|
|
17 |
map (pretty ctxt) xs (*always pretty in order to exhibit errors!*)
|
|
18 |
|> (if ! ThyOutput.source then K [ThyOutput.pretty_text (ThyOutput.str_of_source src)] else I)
|
|
19 |
|> (if ! ThyOutput.quotes then map Pretty.quote else I)
|
|
20 |
|> (if ! ThyOutput.display then
|
|
21 |
map (Output.output o Pretty.string_of o Pretty.indent (! ThyOutput.indent))
|
|
22 |
#> space_implode "\\isasep\\isanewline%\n"
|
118
|
23 |
#> (if ! linenos then (enclose "\\begin{linenos}%\n" "%\n\\end{linenos}") else I)
|
90
|
24 |
#> (if ! gray then (enclose "\\begin{graybox}%\n" "%\n\\end{graybox}") else I)
|
|
25 |
#> enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}"
|
|
26 |
else
|
|
27 |
map (Output.output o (if ! ThyOutput.break then Pretty.string_of else Pretty.str_of))
|
|
28 |
#> space_implode "\\isasep\\isanewline%\n"
|
|
29 |
#> enclose "\\isa{" "}");
|
|
30 |
|
96
018bfa718982
(re)defined the document antiquotation @subgoal in order to be closer to what is actually printed
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
31 |
fun output pretty src ctxt = output_list pretty src ctxt o single
|
018bfa718982
(re)defined the document antiquotation @subgoal in order to be closer to what is actually printed
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
32 |
|
90
|
33 |
val _ = ThyOutput.add_options
|
117
|
34 |
[("gray", Library.setmp gray o boolean),
|
|
35 |
("linenos", Library.setmp linenos o boolean)]
|
90
|
36 |
|
96
018bfa718982
(re)defined the document antiquotation @subgoal in order to be closer to what is actually printed
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
37 |
|
018bfa718982
(re)defined the document antiquotation @subgoal in order to be closer to what is actually printed
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
38 |
|
018bfa718982
(re)defined the document antiquotation @subgoal in order to be closer to what is actually printed
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
39 |
|
24
|
40 |
(** theory data **)
|
|
41 |
|
|
42 |
structure ChunkData = TheoryDataFun
|
|
43 |
(
|
|
44 |
type T = (ML_Lex.token list * stamp) NameSpace.table
|
|
45 |
val empty = NameSpace.empty_table;
|
|
46 |
val copy = I;
|
|
47 |
val extend = I;
|
|
48 |
fun merge _ tables : T = NameSpace.merge_tables (eq_snd (op =)) tables handle Symtab.DUP dup =>
|
|
49 |
error ("Attempt to merge different versions of ML chunk " ^ quote dup);
|
|
50 |
);
|
|
51 |
|
|
52 |
fun declare_chunk name thy =
|
55
|
53 |
(Sign.full_bname thy name,
|
|
54 |
ChunkData.map (snd o NameSpace.bind (Sign.naming_of thy)
|
|
55 |
(Binding.name name, ([], stamp ()))) thy
|
24
|
56 |
handle Symtab.DUP _ => error ("Duplicate definition of ML chunk " ^ quote name));
|
|
57 |
|
|
58 |
fun augment_chunk tok name =
|
|
59 |
ChunkData.map (apsnd (Symtab.map_entry name (apfst (cons tok))));
|
|
60 |
|
|
61 |
fun the_chunk thy name =
|
|
62 |
let val (space, tab) = ChunkData.get thy
|
|
63 |
in case Symtab.lookup tab (NameSpace.intern space name) of
|
|
64 |
NONE => error ("Unknown ML chunk " ^ quote name)
|
|
65 |
| SOME (toks, _) => rev toks
|
|
66 |
end;
|
|
67 |
|
|
68 |
|
|
69 |
(** parsers **)
|
|
70 |
|
|
71 |
val not_eof = ML_Lex.stopper |> Scan.is_stopper #> not;
|
|
72 |
|
|
73 |
val scan_space = Scan.many Symbol.is_blank;
|
|
74 |
|
|
75 |
fun scan_cmt scan =
|
|
76 |
Scan.one (ML_Lex.kind_of #> equal ML_Lex.Comment) >>
|
|
77 |
(ML_Lex.content_of #> Symbol.explode #> Scan.finite Symbol.stopper scan #> fst);
|
|
78 |
|
|
79 |
val scan_chunks = Scan.depend (fn (open_chunks, thy) =>
|
|
80 |
scan_cmt ((Scan.this_string "(*" -- scan_space -- Scan.this_string "@chunk" --
|
|
81 |
scan_space) |-- Symbol.scan_id --|
|
|
82 |
(scan_space -- Scan.this_string "*)") >> (fn name =>
|
|
83 |
let val (name', thy') = declare_chunk name thy
|
|
84 |
in ((name' :: open_chunks, thy'), "") end))
|
|
85 |
||
|
|
86 |
scan_cmt (Scan.this_string "(*" -- scan_space -- Scan.this_string "@end" --
|
|
87 |
scan_space -- Scan.this_string "*)" >> (fn _ =>
|
|
88 |
(case open_chunks of
|
|
89 |
[] => error "end without matching chunk encountered"
|
|
90 |
| _ :: open_chunks' => ((open_chunks', thy), ""))))
|
|
91 |
||
|
|
92 |
Scan.one not_eof >> (fn tok =>
|
|
93 |
((open_chunks, fold (augment_chunk tok) open_chunks thy), ML_Lex.content_of tok)));
|
|
94 |
|
|
95 |
fun chunks_of s thy =
|
|
96 |
let val toks = Source.exhaust (ML_Lex.source (Source.of_string s))
|
|
97 |
in case Scan.finite' ML_Lex.stopper (Scan.repeat (Scan.error scan_chunks))
|
|
98 |
(([], thy), toks) of
|
|
99 |
(toks', (([], thy'), _)) => (implode toks', thy')
|
|
100 |
| (_, ((open_chunks, _), _)) =>
|
|
101 |
error ("Open chunks at end of text: " ^ commas_quote open_chunks)
|
|
102 |
end;
|
|
103 |
|
|
104 |
|
|
105 |
(** use command **)
|
|
106 |
|
|
107 |
fun load_ml dir raw_path thy =
|
|
108 |
(case ThyLoad.check_ml dir raw_path of
|
|
109 |
NONE => error ("Could not find ML file " ^ quote (Path.implode raw_path))
|
|
110 |
| SOME (path, _) =>
|
|
111 |
let val (s, thy') = chunks_of (File.read path) thy
|
|
112 |
in
|
|
113 |
Context.theory_map (ThyInfo.exec_file false raw_path) thy'
|
|
114 |
end);
|
|
115 |
|
|
116 |
fun use_chunks path thy =
|
|
117 |
load_ml (ThyInfo.master_directory (Context.theory_name thy)) path thy;
|
|
118 |
|
|
119 |
val _ =
|
|
120 |
OuterSyntax.command "use_chunks" "eval ML text from file"
|
|
121 |
(OuterKeyword.tag_ml OuterKeyword.thy_decl)
|
|
122 |
(OuterParse.path >> (Toplevel.theory o use_chunks));
|
|
123 |
|
|
124 |
|
|
125 |
(** antiquotation **)
|
|
126 |
|
|
127 |
val str_of_source = space_implode " " o map OuterLex.unparse o #2 o #1 o Args.dest_src;
|
|
128 |
|
|
129 |
val verbatim = space_implode "\\verb,|," o map (enclose "\\verb|" "|") o space_explode "|";
|
|
130 |
|
|
131 |
val transform_cmts =
|
|
132 |
Scan.finite ML_Lex.stopper (Scan.repeat
|
|
133 |
( scan_cmt
|
|
134 |
(Scan.this_string "(*{" |--
|
|
135 |
Scan.repeat (Scan.unless (Scan.this_string "}*)")
|
|
136 |
(Scan.one (not o Symbol.is_eof))) --|
|
|
137 |
Scan.this_string "}*)" >>
|
57
|
138 |
(Symbol.encode_raw o enclose "\\hfill\\textrm{\\textit{" "}}" o implode))
|
24
|
139 |
|| Scan.one not_eof >> ML_Lex.content_of)) #>
|
|
140 |
fst;
|
|
141 |
|
165
|
142 |
fun output_chunk {state: Toplevel.state, source = src, context = ctxt} name =
|
24
|
143 |
let
|
|
144 |
val toks = the_chunk (ProofContext.theory_of ctxt) name;
|
|
145 |
val (spc, toks') = (case toks of
|
|
146 |
[] => ("", [])
|
|
147 |
| [tok] => ("", [tok])
|
|
148 |
| tok :: toks' =>
|
|
149 |
let
|
|
150 |
val (toks'', tok') = split_last toks'
|
|
151 |
val toks''' =
|
|
152 |
if ML_Lex.kind_of tok' = ML_Lex.Space then toks''
|
|
153 |
else toks'
|
|
154 |
in
|
|
155 |
if ML_Lex.kind_of tok = ML_Lex.Space then
|
|
156 |
(tok |> ML_Lex.content_of |> Symbol.explode |>
|
|
157 |
take_suffix (equal " ") |> snd |> implode,
|
|
158 |
toks''')
|
|
159 |
else ("", tok :: toks''')
|
|
160 |
end)
|
|
161 |
val txt = spc ^ implode (transform_cmts toks')
|
|
162 |
in
|
57
|
163 |
txt |> split_lines |>
|
90
|
164 |
output_list (fn _ => fn s => Pretty.str s) src ctxt
|
24
|
165 |
end;
|
|
166 |
|
165
|
167 |
val _ = ThyOutput.antiquotation "ML_chunk" (Scan.lift Args.name) output_chunk;
|
24
|
168 |
|
|
169 |
end;
|