ProgTutorial/antiquote_setup.ML
changeset 311 ee864694315b
parent 303 05e6a33edef6
child 315 de49d5780f57
equal deleted inserted replaced
310:007922777ff1 311:ee864694315b
     4 struct
     4 struct
     5 
     5 
     6 open OutputTutorial
     6 open OutputTutorial
     7 
     7 
     8 (* functions for generating appropriate expressions *)
     8 (* functions for generating appropriate expressions *)
     9 fun ml_val_open ys istruc txt = 
     9 fun ml_val_open ys strct txt = 
    10 let 
    10 let 
    11   fun ml_val_open_aux ys txt = 
    11   fun ml_val_open_aux ys txt = 
    12           "fn " ^ (case ys of [] => "_" | _ => enclose "(" ")" (commas ys)) ^ " => (" ^ txt ^ ")";
    12     implode ["fn ", (case ys of [] => "_" | _ => enclose "(" ")" (commas ys)), " => (", txt, ")"];
    13 in
    13 in
    14  (case istruc of
    14  (case strct of
    15     NONE    => ml_val_open_aux ys txt
    15     NONE    => ml_val_open_aux ys txt
    16   | SOME st => ml_val_open_aux ys ("let open " ^ st ^ " in " ^ txt ^ " end"))
    16   | SOME st => ml_val_open_aux ys ("let open " ^ st ^ " in " ^ txt ^ " end"))
    17 end
    17 end
    18 
    18 
    19 fun ml_val txt = ml_val_open [] NONE txt;
    19 fun ml_val txt = ml_val_open [] NONE txt;