src/TeX/holindex.sml

218 (*val os = Portable.std_out*)
219 fun output_holtex_def_internal (definetype,id,cs) os  =
221    val _ = Portable.output (os, definetype);
222    val _ = Portable.output (os, id);
223    val _ = Portable.output (os, "}{");
224    val _ = Portable.output (os, cs);
225    val _ = Portable.output (os, "}\n");
233 fun output_holtex_def command definetype os (id,
245               output_holtex_def_internal (definetype,id,cs) os
254 fun process_type_defs os =
255    List.map (output_holtex_def mungeTools.Type "\\defineHOLty{" os)
258 fun process_term_defs os =
259    List.map (output_holtex_def mungeTools.Term "\\defineHOLtm{" os)
261 fun process_thm_defs os =
262    List.map (output_holtex_def mungeTools.Theorem "\\defineHOLthm{" os)
264 fun output_all_defs os (thmL, termL, typeL) =
266    val typeDefL = process_type_defs os typeL;
267    val termDefL = process_term_defs os termL;
268    val thmDefL = process_thm_defs os thmL;
398 fun output_holtex_index d (indextype,flagtype) os (id,
405    val _ = Portable.output (os, indextype);
406    val _ = Portable.output (os, id);
407    val _ = Portable.output (os, "}{");
408    val _ = Portable.output (os, label);
409    val _ = Portable.output (os, "}{");
410    val _ = Portable.output (os, process_index_pages pages);
411    val _ = Portable.output (os, "}{");
412    val _ = Portable.output (os, boolopt2latex full_index flagtype);
413    val _ = Portable.output (os, "}{");
414    val _ = Portable.output (os, bool2latex (not (Redblackset.isEmpty pages)));
415    val _ = Portable.output (os, "}{");
416    val _ = Portable.output (os, if isSome comment_opt then valOf comment_opt else "");
417    val _ = Portable.output (os, "}{");
418    val _ = Portable.output (os, Redblackmap.find (d,id));
419    val _ = Portable.output (os, "}\n");
427 fun process_type_index d os typeL =
433     val _ = Portable.output(os, "   \\begin{HOLTypeIndex}\n");
434     val _ = List.map (output_holtex_index d ("      \\HOLTypeIndexEntry{","holIndexLongTypeFlag") os) type_entryL'
435     val _ = Portable.output(os, "   \\end{HOLTypeIndex}\n");
441 fun process_term_index d os termL =
447     val _ = Portable.output(os, "   \\begin{HOLTermIndex}\n");
448     val _ = List.map (output_holtex_index d ("      \\HOLTermIndexEntry{","holIndexLongTermFlag") os) term_entryL'
449     val _ = Portable.output(os, "   \\end{HOLTermIndex}\n");
455 fun process_thm_index d os thmL =
479     val _ = Portable.output(os, "\\begin{HOLThmIndex}\n");
484                 (Portable.output(os, "   \\HOLThmIndexTheory{"^thy^"}\n"))
485             val _ = output_holtex_index d ("      \\HOLThmIndexEntry{","holIndexLongThmFlag") os (id, de);
490     val _ = Portable.output(os, "\\end{HOLThmIndex}\n");
498 fun output_all_index os (thmD,termD,typeD) (thmL, termL, typeL) =
500    val _ = process_type_index typeD os typeL;
501    val _ = process_term_index termD os termL;
502    val _ = process_thm_index thmD os thmL;
503    val _ = Portable.output (os, " \n");
527     val os = Portable.open_out (basename ^ ".tde")
528     val dd = output_all_defs os ds
529     val _  = Portable.close_out os;
530     val os = Portable.open_out (basename ^ ".tid")
531     val _ = output_all_index os dd ds;
532     val _  = Portable.close_out os;