1structure holindexData :> holindexData =
2struct
3
4open Lib Feedback
5
6val scomp = String.collate (fn (c1, c2) =>
7    Char.compare (Char.toUpper c1, Char.toUpper c2))
8
9type data_entry =
10   {label         : string option,
11    in_index      : bool,
12    printed       : bool,
13    full_index    : bool option,
14    comment       : string option,
15    pos_opt       : int option,
16    options       : string,
17    content       : string option,
18    latex         : string option,
19    pages         : string Redblackset.set}
20
21val default_data_entry =
22  ({label         = NONE,
23    in_index      = false,
24    printed       = false,
25    full_index    = NONE,
26    pos_opt       = NONE,
27    comment       = NONE,
28    options       = "",
29    content       = NONE,
30    latex         = NONE,
31    pages         = (Redblackset.empty String.compare)}:data_entry)
32
33fun data_entry___update_in_index new_ii
34  ({label         = label,
35    in_index      = in_index,
36    printed       = printed,
37    full_index    = full_index,
38    comment       = comment,
39    pos_opt       = pos_opt,
40    options       = options,
41    content       = content,
42    latex         = latex,
43    pages         = pages}:data_entry) =
44   {label            = label,
45    in_index      = new_ii,
46    printed       = printed,
47    full_index    = full_index,
48    comment       = comment,
49    pos_opt       = pos_opt,
50    options       = options,
51    content       = content,
52    latex         = latex,
53    pages         = pages}:data_entry;
54
55fun data_entry___update_printed new_printed
56  ({label         = label,
57    in_index      = in_index,
58    printed       = printed,
59    full_index    = full_index,
60    comment       = comment,
61    pos_opt       = pos_opt,
62    options       = options,
63    content       = content,
64    latex         = latex,
65    pages         = pages}:data_entry) =
66   {label            = label,
67    in_index      = in_index,
68    printed       = new_printed,
69    full_index    = full_index,
70    comment       = comment,
71    pos_opt       = pos_opt,
72    options       = options,
73    content       = content,
74    latex         = latex,
75    pages         = pages}:data_entry;
76
77
78fun data_entry___update_full_index new_fi
79  ({label         = label,
80    in_index      = in_index,
81    printed       = printed,
82    full_index    = full_index,
83    comment       = comment,
84    pos_opt       = pos_opt,
85    options       = options,
86    content       = content,
87    latex         = latex,
88    pages         = pages}:data_entry) =
89   {label            = label,
90    in_index      = in_index,
91    printed       = printed,
92    full_index    = SOME new_fi,
93    comment       = comment,
94    pos_opt       = pos_opt,
95    options       = options,
96    content       = content,
97    latex         = latex,
98    pages         = pages}:data_entry;
99
100
101fun data_entry___update_label new_label
102  ({label         = label,
103    in_index      = in_index,
104    printed       = printed,
105    full_index    = full_index,
106    comment       = comment,
107    pos_opt       = pos_opt,
108    options       = options,
109    content       = content,
110    latex         = latex,
111    pages         = pages}:data_entry) =
112   {label         = new_label,
113    in_index      = in_index,
114    printed       = printed,
115    full_index    = full_index,
116    comment       = comment,
117    pos_opt       = pos_opt,
118    options       = options,
119    content       = content,
120    latex         = latex,
121    pages         = pages}:data_entry;
122
123
124fun data_entry___update_comment new_comment
125  ({label         = label,
126    in_index      = in_index,
127    printed       = printed,
128    full_index    = full_index,
129    comment       = comment,
130    pos_opt       = pos_opt,
131    options       = options,
132    content       = content,
133    latex         = latex,
134    pages         = pages}:data_entry) =
135   {label         = label,
136    in_index      = in_index,
137    printed       = printed,
138    full_index    = full_index,
139    comment       = new_comment,
140    pos_opt       = pos_opt,
141    options       = options,
142    content       = content,
143    latex         = latex,
144    pages         = pages}:data_entry;
145
146fun data_entry___update_options new_op
147  ({label         = label,
148    in_index      = in_index,
149    printed       = printed,
150    full_index    = full_index,
151    comment       = comment,
152    pos_opt       = pos_opt,
153    options       = options,
154    content       = content,
155    latex         = latex,
156    pages         = pages}:data_entry) =
157   {label         = label,
158    in_index      = in_index,
159    printed       = printed,
160    full_index    = full_index,
161    comment       = comment,
162    pos_opt       = pos_opt,
163    options       = new_op,
164    content       = content,
165    latex         = latex,
166    pages         = pages}:data_entry;
167
168fun data_entry___update_content new_content
169  ({label         = label,
170    in_index      = in_index,
171    printed       = printed,
172    full_index    = full_index,
173    comment       = comment,
174    pos_opt       = pos_opt,
175    options       = options,
176    content       = content,
177    latex         = latex,
178    pages         = pages}:data_entry) =
179   {label         = label,
180    in_index      = in_index,
181    printed       = printed,
182    full_index    = full_index,
183    comment       = comment,
184    pos_opt       = pos_opt,
185    options       = options,
186    content       = new_content,
187    latex         = latex,
188    pages         = pages}:data_entry;
189
190
191
192fun data_entry___update_latex new_latex
193  ({label         = label,
194    in_index      = in_index,
195    printed       = printed,
196    full_index    = full_index,
197    comment       = comment,
198    pos_opt       = pos_opt,
199    options       = options,
200    content       = content,
201    latex         = latex,
202    pages         = pages}:data_entry) =
203   {label         = label,
204    in_index      = in_index,
205    printed       = printed,
206    full_index    = full_index,
207    comment       = comment,
208    pos_opt       = pos_opt,
209    options       = options,
210    content       = content,
211    latex         = new_latex,
212    pages         = pages}:data_entry;
213
214
215val data_entry___pos_counter_ref = ref 0;
216fun data_entry___add_page page
217  ({label         = label,
218    in_index      = in_index,
219    printed       = printed,
220    full_index    = full_index,
221    comment       = comment,
222    pos_opt       = pos_opt,
223    options       = options,
224    content       = content,
225    latex         = latex,
226    pages         = pages}:data_entry) =
227   let
228      val new_pos_opt =
229         if isSome pos_opt then pos_opt else
230         (data_entry___pos_counter_ref := (!data_entry___pos_counter_ref) + 1;
231          SOME (!data_entry___pos_counter_ref));
232   in
233   {label         = label,
234    in_index      = in_index,
235    printed       = printed,
236    full_index    = full_index,
237    comment       = comment,
238    pos_opt       = new_pos_opt,
239    options       = options,
240    content       = content,
241    latex         = latex,
242    pages         = Redblackset.add(pages,page)}:data_entry
243   end;
244
245
246fun data_entry_is_used
247  ({in_index      = in_index,
248    pos_opt       = pos_opt,
249    ...}:data_entry) =
250   (in_index orelse isSome pos_opt);
251
252
253val new_data_substore = (Redblackmap.mkDict scomp):(string, data_entry) Redblackmap.dict
254
255val new_data_store  =  (*Thms, Terms, Types*)
256   (new_data_substore, new_data_substore, new_data_substore);
257
258
259(*
260   val key1 = "Term";
261   val key2 = "Term_ID_1"
262   fun upf e = data_entry___add_page e "1";
263*)
264type data_store_ty = ((string, data_entry) Redblackmap.dict * (string, data_entry) Redblackmap.dict * (string, data_entry) Redblackmap.dict);
265
266local
267   fun update_data_substore (allow_new,error_fun) sds (key:string) upf =
268   let
269      open Redblackmap
270      val (ent,ok) = (find (sds, key),true) handle NotFound => (default_data_entry, allow_new);
271      val sds' = if ok then (insert(sds,key,upf ent)) else
272            (error_fun key;sds)
273   in
274      sds'
275   end;
276
277   fun unknown_def (type_def, error_fun:string->unit) s =
278       error_fun ("Undefined "^type_def^" '"^s^"'!");
279in
280
281fun update_data_store (allow_new,error_fun) (sds_thm,sds_term,sds_type) "Thm" key upf =
282   (update_data_substore (true, unknown_def ("Thm", error_fun)) sds_thm key upf,sds_term,sds_type)
283| update_data_store (allow_new,error_fun) (sds_thm,sds_term,sds_type) "Term" key upf =
284   (sds_thm, update_data_substore
285        (allow_new, unknown_def ("Term", error_fun)) sds_term key upf,sds_type)
286| update_data_store (allow_new,error_fun) (sds_thm,sds_term,sds_type) "Type" key upf =
287   (sds_thm, sds_term, update_data_substore
288       (allow_new, unknown_def ("Type", error_fun)) sds_type key upf)
289| update_data_store _ _ ty _ _ =
290   Feedback.failwith ("Unkwown entry_type '"^ty^"'!")
291
292end;
293
294
295
296
297
298
299
300
301
302
303
304
305type parse_entry =
306   {id          : (string * string),
307    label       : string option,
308    force_index : bool,
309    full_index  : bool option,
310    comment     : string option,
311    options     : string option,
312    latex       : string option,
313    content     : string option}
314
315fun mk_parse_entry id =
316   {id          = id,
317    label       = NONE,
318    force_index = false,
319    full_index  = NONE,
320    comment     = NONE,
321    latex       = NONE,
322    options     = NONE,
323    content     = NONE}:parse_entry
324
325fun mk_update_parse_entry id up =
326   (up (mk_parse_entry id)):parse_entry
327
328
329fun destruct_theory_thm s2 =
330    let
331       val ss2 = (Substring.full s2)
332       val (x1,x2) = Substring.splitl (fn c => not (c = #".")) ss2
333       val x2' = Substring.triml 1 x2
334    in
335       (Substring.string x1, Substring.string x2')
336    end
337
338
339fun mk_theorem_parse_entries ids up =
340   let
341      fun expand_theory_map id =
342      let
343          val (thy, thm) = destruct_theory_thm id
344      in
345          if not (String.isSuffix "*" thm) then [id] else
346          let
347             val thmL = List.map (snd o fst) (DB.thy thy);
348             val pre = String.substring (thm, 0, String.size thm - 1);
349             val thmL' = List.filter (String.isPrefix pre) thmL
350          in
351             List.map (fn s => String.concat [thy, ".",s]) thmL'
352          end
353      end;
354      val ids' = Lib.flatten (List.map expand_theory_map ids)
355   in
356      List.map (fn id => mk_update_parse_entry ("Thm", id) up) ids'
357   end;
358
359
360fun parse_entry___set_label l
361   ({id          = id,
362    label       = label_opt,
363    force_index = fi,
364    full_index  = full_index,
365    comment     = comment,
366    latex       = latex,
367    options     = options_opt,
368    content     = content_opt}:parse_entry) =
369   {id          = id,
370    label       = SOME l,
371    force_index = fi,
372    full_index  = full_index,
373    comment     = comment,
374    latex       = latex,
375    options     = options_opt,
376    content     = content_opt}:parse_entry;
377
378fun parse_entry___set_comment c
379   ({id          = id,
380    label       = label_opt,
381    force_index = fi,
382    full_index  = full_index,
383    comment     = comment,
384    latex       = latex,
385    options     = options_opt,
386    content     = content_opt}:parse_entry) =
387   {id          = id,
388    label       = label_opt,
389    force_index = fi,
390    full_index  = full_index,
391    comment     = SOME c,
392    latex       = latex,
393    options     = options_opt,
394    content     = content_opt}:parse_entry;
395
396fun parse_entry___set_latex l
397   ({id          = id,
398    label       = label_opt,
399    force_index = fi,
400    full_index  = full_index,
401    comment     = comment,
402    latex       = latex,
403    options     = options_opt,
404    content     = content_opt}:parse_entry) =
405   {id          = id,
406    label       = label_opt,
407    force_index = fi,
408    full_index  = full_index,
409    comment     = comment,
410    latex       = SOME l,
411    options     = options_opt,
412    content     = content_opt}:parse_entry;
413
414
415fun parse_entry___set_options new_opt
416   ({id          = id,
417    label       = label_opt,
418    latex       = latex,
419    force_index = fi,
420    full_index  = full_index,
421    comment     = comment,
422    options     = options_opt,
423    content     = content_opt}:parse_entry) =
424   {id          = id,
425    label       = label_opt,
426    force_index = fi,
427    full_index  = full_index,
428    comment     = comment,
429    latex       = latex,
430    options     = SOME new_opt,
431    content     = content_opt}:parse_entry;
432
433
434fun parse_entry___set_content new_cont
435   ({id          = id,
436    label       = label_opt,
437    force_index = fi,
438    full_index  = full_index,
439    comment     = comment,
440    latex       = latex,
441    options     = options_opt,
442    content     = content_opt}:parse_entry) =
443   {id          = id,
444    label       = label_opt,
445    force_index = fi,
446    full_index  = full_index,
447    comment     = comment,
448    latex       = latex,
449    options     = options_opt,
450    content     = SOME new_cont}:parse_entry;
451
452fun parse_entry___force_index
453   ({id          = id,
454    label       = label_opt,
455    force_index = fi,
456    full_index  = full_index,
457    options     = options_opt,
458    comment     = comment,
459    latex       = latex,
460    content     = content_opt}:parse_entry) =
461   {id          = id,
462    label       = label_opt,
463    force_index = true,
464    full_index  = full_index,
465    comment     = comment,
466    latex       = latex,
467    options     = options_opt,
468    content     = content_opt}:parse_entry;
469
470fun parse_entry___full_index b
471   ({id          = id,
472    label       = label_opt,
473    force_index = fi,
474    full_index  = full_index,
475    options     = options_opt,
476    comment     = comment,
477    latex       = latex,
478    content     = content_opt}:parse_entry) =
479   {id          = id,
480    label       = label_opt,
481    force_index = fi,
482    full_index  = SOME b,
483    comment     = comment,
484    latex       = latex,
485    options     = options_opt,
486    content     = content_opt}:parse_entry;
487
488
489
490fun parse_entry___add_to_data_store ds
491  ({id          = (ety, id_s),
492    label       = label_opt,
493    force_index = fi,
494    full_index  = full_i,
495    comment     = comment_opt,
496    latex       = latex_opt,
497    options     = options_opt,
498    content     = content_opt}:parse_entry) =
499let
500   fun update_fun ({label    = label,
501                    in_index = in_index,
502                    printed    = printed,
503                    full_index = full_index,
504                    comment    = comment,
505                    latex      = latex,
506                    pos_opt    = pos_opt,
507                    options  = options,
508                    content  = content,
509                    pages    = pages}:data_entry) =
510      ({label      = if isSome label_opt then label_opt else label,
511        in_index   = fi orelse in_index,
512        printed    = printed,
513        full_index = if isSome full_i then full_i else full_index,
514        comment    = if isSome comment_opt then comment_opt else comment,
515        latex      = if isSome latex_opt then latex_opt else latex,
516        pos_opt    = pos_opt,
517        options    = if isSome options_opt then valOf options_opt else options,
518        content    = if isSome content_opt then content_opt else content,
519        pages      = pages}:data_entry);
520in
521   update_data_store (true, K ()) ds ety id_s update_fun
522end;
523
524
525end
526