ProgTutorial/output_tutorial.ML
changeset 373 28a49fe024c9
parent 351 f118240ab44a
child 438 d9a223c023f6
--- 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