diff -r ce0f60d0351e -r 03145998190b ProgTutorial/output_tutorial.ML --- 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