--- a/ProgTutorial/output_tutorial.ML Tue Nov 03 07:10:05 2009 +0100
+++ b/ProgTutorial/output_tutorial.ML Tue Nov 03 13:57:03 2009 +0100
@@ -69,9 +69,15 @@
then implode ["\\index{", get_indstring m, "}"]
else implode ["\\index{", get_indstring m, " (", get_indstring n, ")}"])
+fun get_str_index {main = m, minor = n} =
+ (case n of
+ Struct s => implode ["\\index[str]{{\\tt\\slshape{}", get_word s, "}!", get_indstring m, "}"]
+ | _ => "")
+
fun output_indexed ind txt =
txt |> output
|> prefix (get_index ind)
+ |> prefix (get_str_index ind)
fun boolean "" = true
| boolean "true" = true