60 in |
62 in |
61 if (only_letters (Symbol.explode str)) then (clean_string str) |
63 if (only_letters (Symbol.explode str)) then (clean_string str) |
62 else error ("Underspecified index entry only for single words allowed! Error with " ^ quote str) |
64 else error ("Underspecified index entry only for single words allowed! Error with " ^ quote str) |
63 end |
65 end |
64 |
66 |
65 fun get_qstring (Plain s) = get_word s |
67 fun get_qstring NoString = "" |
|
68 | get_qstring (Plain s) = get_word s |
66 | get_qstring (Code s) = let val w = get_word s in (w ^ "@{\\tt\\slshape{}" ^ w ^ "}") end |
69 | get_qstring (Code s) = let val w = get_word s in (w ^ "@{\\tt\\slshape{}" ^ w ^ "}") end |
|
70 | get_qstring (IStruc s) = "in {\\tt\\slshape{}" ^ (get_word s) ^ "}" |
67 |
71 |
68 fun is_empty_qstr (Plain "") = true |
72 fun is_empty_qstr (Plain "") = true |
69 | is_empty_qstr (Code "") = true |
73 | is_empty_qstr (Code "") = true |
70 | is_empty_qstr _ = false |
74 | is_empty_qstr _ = false |
71 |
75 |
72 fun get_index_info {main = m, minor = n} = |
76 fun get_index_info {main = m, minor = n} = |
73 (if n = "" |
77 (if n = NoString |
74 then "\\index{" ^ (get_qstring m) ^ "}" |
78 then "\\index{" ^ (get_qstring m) ^ "}" |
75 else "\\indexdef{" ^ (get_qstring m) ^ "}{" ^ n ^ "}") |
79 else "\\indexdef{" ^ (get_qstring m) ^ "}{" ^ (get_qstring n) ^ "}") |
76 |
80 |
77 fun index_entry entry index_info = |
81 fun index_entry entry index_info = |
78 case entry of |
82 case entry of |
79 No_Entry => I |
83 No_Entry => I |
80 | Explicit s => prefix s |
84 | Explicit s => prefix s |