--- a/ProgTutorial/output_tutorial.ML	Thu Aug 20 14:19:39 2009 +0200
+++ b/ProgTutorial/output_tutorial.ML	Thu Aug 20 22:30:20 2009 +0200
@@ -3,7 +3,7 @@
 struct
 
 (* rebuilding the output function from ThyOutput in order to *)
-(* enable the options [gray, linenos, index]                 *)
+(* enable the options [gray, linenos]                        *)
 
 val gray = ref false
 val linenos = ref false
@@ -27,22 +27,15 @@
     #> enclose "\\isa{" "}")
 end
 
-datatype qstring =
+datatype indstring =
   NoString
 | Plain   of string
 | Code    of string
-| IStruct of string
+| Struct  of string
 
-datatype entry = 
-   No_Entry
- | Default 
- | Explicit of string
+fun translate_string f = Symbol.explode #> map f #> implode;
 
-val index = ref No_Entry
-
-fun translate f = Symbol.explode #> map f #> implode;
-
-val clean_string = translate
+val clean_string = translate_string
   (fn "_" => "\\_"
     | "#" => "\\#"
     | "<" => "\\isacharless"
@@ -53,7 +46,7 @@
     | "$" => "\\isachardollar"
     | "!" => "\\isacharbang"
     | "\<dash>" => "-"
-    | c => c);
+    | c => c)
 
 fun get_word str =
 let 
@@ -61,47 +54,32 @@
     | only_letters (x::xs) = 
         if (Symbol.is_ascii_blank x) then false else only_letters xs
 in
-  if (only_letters (Symbol.explode str)) then (clean_string str)
-  else error ("Underspecified index entry only for single words allowed! Error with " ^ quote str)
+  if only_letters (Symbol.explode str) 
+  then clean_string str
+  else error ("Only single word allowed! Error with " ^ quote str)
 end  
 
-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 (IStruct s) =  "in {\\tt\\slshape{}" ^ (get_word s) ^ "}"
+fun get_indstring NoString = ""
+  | get_indstring (Plain s) = get_word s
+  | get_indstring (Code s) = let val w = get_word s in implode[w, "@{\\tt\\slshape{}", w, "}"] end
+  | get_indstring (Struct s) =  implode ["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} = 
+fun get_index {main = m, minor = n} = 
  (if n = NoString
-  then "\\index{" ^ (get_qstring m) ^ "}"  
-  else "\\indexdef{" ^ (get_qstring m) ^ "}{" ^ (get_qstring n) ^ "}")  
+  then implode ["\\index{", get_indstring m, "}"]  
+  else implode ["\\index{", get_indstring m, " (", get_indstring n, ")}"])  
     
-fun index_entry entry index_info  =
- case entry of
-   No_Entry => I
- | Explicit s => prefix s
- | Default => prefix (get_index_info index_info)
-
-fun output_indexed txt index_info =
+fun output_indexed ind txt =
  txt |> output
-     |> index_entry (!index) index_info
+     |> prefix (get_index ind)
 
 fun boolean "" = true
   | boolean "true" = true
   | boolean "false" = false
   | boolean s = error ("Bad boolean value: " ^ quote s);
 
-fun explicit "" = Default
-  | explicit s  = Explicit s
-
-
 val _ = ThyOutput.add_options
  [("gray", Library.setmp gray o boolean),
-  ("linenos", Library.setmp linenos o boolean),
-  ("index", Library.setmp index o explicit)]
-
+  ("linenos", Library.setmp linenos o boolean)]
 
 end
\ No newline at end of file