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