--- 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