ProgTutorial/antiquote_setup.ML
changeset 302 0cbd34857b9e
parent 261 358f325f4db6
child 303 05e6a33edef6
equal deleted inserted replaced
301:2728e8daebc0 302:0cbd34857b9e
    45 (* checks and prints open expressions, calculates index entry *)
    45 (* checks and prints open expressions, calculates index entry *)
    46 fun output_ml {context = ctxt, ...} (txt, (ovars, istruc)) =
    46 fun output_ml {context = ctxt, ...} (txt, (ovars, istruc)) =
    47   (eval_fn ctxt (ml_val_open ovars istruc txt);
    47   (eval_fn ctxt (ml_val_open ovars istruc txt);
    48    case (istruc, Long_Name.base_name txt, Long_Name.qualifier txt)  of
    48    case (istruc, Long_Name.base_name txt, Long_Name.qualifier txt)  of
    49      (NONE, bn, "")  => output_indexed (transform_cmts_str txt) {main = Code txt, minor = NoString}
    49      (NONE, bn, "")  => output_indexed (transform_cmts_str txt) {main = Code txt, minor = NoString}
    50    | (NONE, bn, qn)  => output_indexed (transform_cmts_str txt) {main = Code bn, minor = IStruc qn}
    50    | (NONE, bn, qn)  => output_indexed (transform_cmts_str txt) {main = Code bn, minor = IStruct qn}
    51    | (SOME st, _, _) => output_indexed (transform_cmts_str txt) {main = Code txt, minor = IStruc st})
    51    | (SOME st, _, _) => output_indexed (transform_cmts_str txt) {main = Code txt, minor = IStruct st})
    52 
    52 
    53 val parser_ml = Scan.lift (Args.name --
    53 val parser_ml = Scan.lift (Args.name --
    54   (Scan.optional (Args.$$$ "for" |-- OuterParse.!!! (Scan.repeat1 Args.name)) [] --
    54   (Scan.optional (Args.$$$ "for" |-- OuterParse.!!! (Scan.repeat1 Args.name)) [] --
    55    Scan.option (Args.$$$ "in"  |-- OuterParse.!!! Args.name))) 
    55    Scan.option (Args.$$$ "in"  |-- OuterParse.!!! Args.name))) 
    56 
    56