--- a/ProgTutorial/FirstSteps.thy	Sat May 30 23:58:05 2009 +0200
+++ b/ProgTutorial/FirstSteps.thy	Sun May 31 00:39:17 2009 +0200
@@ -1009,8 +1009,8 @@
   (FIXME: Explain the following better.)
 
   Occasionally you have to calculate what the ``base'' name of a given
-  constant is. For this you can use the function @{ML [index] extern_const in Sign} or
-  @{ML base_name in Long_Name}. For example:
+  constant is. For this you can use the function @{ML [index] "Sign.extern_const"} or
+  @{ML [index] Long_Name.base_name}. For example:
 
   @{ML_response [display,gray] "Sign.extern_const @{theory} \"List.list.Nil\"" "\"Nil\""}
 

--- a/ProgTutorial/Parsing.thy	Sat May 30 23:58:05 2009 +0200
+++ b/ProgTutorial/Parsing.thy	Sun May 31 00:39:17 2009 +0200
@@ -288,7 +288,6 @@
   where the function @{ML [index] not_eof in Symbol} ensures that we do not read beyond the 
   end of the input string (i.e.~stopper symbol).
 
-  \indexdef{unless@ {\tt\slshape{unless}}}{in {\tt\slshape Scan}}
   The function @{ML "Scan.unless p q" for p q} takes two parsers: if the first one can 
   parse the input, then the whole parser fails; if not, then the second is tried. Therefore
   

--- a/ProgTutorial/antiquote_setup.ML	Sat May 30 23:58:05 2009 +0200
+++ b/ProgTutorial/antiquote_setup.ML	Sun May 31 00:39:17 2009 +0200
@@ -6,16 +6,17 @@
 open OutputTutorial
 
 (* functions for generating appropriate expressions *)
-fun ml_val_open ys xs txt = 
-  let fun ml_val_open_aux ys txt = 
+fun ml_val_open ys istruc txt = 
+let 
+  fun ml_val_open_aux ys txt = 
           "fn " ^ (case ys of [] => "_" | _ => enclose "(" ")" (commas ys)) ^ " => (" ^ txt ^ ")";
-  in
-    (case xs of
-       [] => ml_val_open_aux ys txt
-     | _  => ml_val_open_aux ys ("let open " ^ (space_implode " " xs) ^ " in " ^ txt ^ " end"))
-  end;
+in
+ (case istruc of
+    NONE    => ml_val_open_aux ys txt
+  | SOME st => ml_val_open_aux ys ("let open " ^ st ^ " in " ^ txt ^ " end"))
+end
 
-fun ml_val txt = ml_val_open [] [] txt;
+fun ml_val txt = ml_val_open [] NONE txt;
 
 fun ml_pat (lhs, pat) =
   let 
@@ -41,26 +42,26 @@
   #> implode 
   #> string_explode ""
 
-(* checks and prints open expressions *)
-fun output_ml {context = ctxt, ...} (txt, (ovars, structs)) =
-  (eval_fn ctxt (ml_val_open ovars structs txt);
-   if structs = []
-   then output_indexed (transform_cmts_str txt) {main = Code txt, minor = ""}
-   else output_indexed (transform_cmts_str txt) 
-             {main = Code txt, minor = ("in {\\tt\\slshape{}" ^ (implode structs) ^ "}")})
+(* checks and prints open expressions, calculates index entry *)
+fun output_ml {context = ctxt, ...} (txt, (ovars, istruc)) =
+  (eval_fn ctxt (ml_val_open ovars istruc txt);
+   case (istruc, Long_Name.base_name txt, Long_Name.qualifier txt)  of
+     (NONE, bn, "")  => output_indexed (transform_cmts_str txt) {main = Code txt, minor = NoString}
+   | (NONE, bn, qn)  => output_indexed (transform_cmts_str txt) {main = Code bn, minor = IStruc qn}
+   | (SOME st, _, _) => output_indexed (transform_cmts_str txt) {main = Code txt, minor = IStruc st})
 
 val parser_ml = Scan.lift (Args.name --
   (Scan.optional (Args.$$$ "for" |-- OuterParse.!!! (Scan.repeat1 Args.name)) [] --
-   Scan.optional (Args.$$$ "in"  |-- OuterParse.!!! (Scan.repeat1 Args.name)) [])) 
+   Scan.option (Args.$$$ "in"  |-- OuterParse.!!! Args.name))) 
 
 (* checks and prints types and structures *)
 fun output_struct {context = ctxt, ...} txt = 
   (eval_fn ctxt (ml_struct txt);
-   output_indexed (string_explode "" txt) {main = Code txt, minor = "structure"})
+   output_indexed (string_explode "" txt) {main = Code txt, minor = Plain "structure"})
 
 fun output_type {context = ctxt, ...} txt = 
   (eval_fn ctxt (ml_type txt);
-   output_indexed (string_explode "" txt) {main = Code txt, minor = "type"})
+   output_indexed (string_explode "" txt) {main = Code txt, minor = Plain "type"})
 
 (* checks and expression agains a result pattern *)
 fun output_response {context = ctxt, ...} (lhs, pat) = 

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

Binary file progtutorial.pdf has changed