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