ProgTutorial/output_tutorial.ML
changeset 258 03145998190b
parent 256 1fb8d62c88a0
child 261 358f325f4db6
--- a/ProgTutorial/output_tutorial.ML	Sat May 30 23:58:05 2009 +0200
+++ b/ProgTutorial/output_tutorial.ML	Sun May 31 00:39:17 2009 +0200
@@ -27,8 +27,10 @@
 end
 
 datatype qstring =
-  Plain of string
-| Code  of string
+  NoString
+| Plain  of string
+| Code   of string
+| IStruc of string
 
 datatype entry = 
    No_Entry
@@ -62,17 +64,19 @@
   else error ("Underspecified index entry only for single words allowed! Error with " ^ quote str)
 end  
 
-fun get_qstring (Plain s) = get_word s
+fun get_qstring NoString = ""
+  | get_qstring (Plain s) = get_word s
   | get_qstring (Code s) = let val w = get_word s in  (w ^ "@{\\tt\\slshape{}" ^ w ^ "}") end
+  | get_qstring (IStruc s) =  "in {\\tt\\slshape{}" ^ (get_word s) ^ "}"
 
 fun is_empty_qstr (Plain "") = true
   | is_empty_qstr (Code "") = true
   | is_empty_qstr _ = false
 
 fun get_index_info {main = m, minor = n} = 
- (if n = ""
+ (if n = NoString
   then "\\index{" ^ (get_qstring m) ^ "}"  
-  else "\\indexdef{" ^ (get_qstring m) ^ "}{" ^ n ^ "}")  
+  else "\\indexdef{" ^ (get_qstring m) ^ "}{" ^ (get_qstring n) ^ "}")  
     
 fun index_entry entry index_info  =
  case entry of