ProgTutorial/antiquote_setup.ML
changeset 426 d94755882e36
parent 367 643b1e1d7d29
child 438 d9a223c023f6
equal deleted inserted replaced
425:ce43c04d227d 426:d94755882e36
    39 fun output_ml {context = ctxt, ...} (txt, (vs, stru)) =
    39 fun output_ml {context = ctxt, ...} (txt, (vs, stru)) =
    40   (eval_fn ctxt (ml_val vs stru txt); 
    40   (eval_fn ctxt (ml_val vs stru txt); 
    41    output (split_lines txt))
    41    output (split_lines txt))
    42 
    42 
    43 val parser_ml = Scan.lift (Args.name --
    43 val parser_ml = Scan.lift (Args.name --
    44   (Scan.optional (Args.$$$ "for" |-- OuterParse.!!! (Scan.repeat1 Args.name)) [] --
    44   (Scan.optional (Args.$$$ "for" |-- Parse.!!! (Scan.repeat1 Args.name)) [] --
    45    Scan.option (Args.$$$ "in"  |-- OuterParse.!!! Args.name))) 
    45    Scan.option (Args.$$$ "in"  |-- Parse.!!! Args.name))) 
    46 
    46 
    47 (* checks and prints a single ML-item and produces an index entry *)
    47 (* checks and prints a single ML-item and produces an index entry *)
    48 fun output_ml_ind {context = ctxt, ...} (txt, stru) =
    48 fun output_ml_ind {context = ctxt, ...} (txt, stru) =
    49   (eval_fn ctxt (ml_val [] stru txt); 
    49   (eval_fn ctxt (ml_val [] stru txt); 
    50    case (stru, Long_Name.base_name txt, Long_Name.qualifier txt) of
    50    case (stru, Long_Name.base_name txt, Long_Name.qualifier txt) of
    51      (NONE, bn, "")  => output_indexed {main = Code txt, minor = NoString} (split_lines txt)
    51      (NONE, bn, "")  => output_indexed {main = Code txt, minor = NoString} (split_lines txt)
    52    | (NONE, bn, qn)  => output_indexed {main = Code bn,  minor = Struct qn} (split_lines txt)
    52    | (NONE, bn, qn)  => output_indexed {main = Code bn,  minor = Struct qn} (split_lines txt)
    53    | (SOME st, _, _) => output_indexed {main = Code txt, minor = Struct st} (split_lines txt))
    53    | (SOME st, _, _) => output_indexed {main = Code txt, minor = Struct st} (split_lines txt))
    54 
    54 
    55 val parser_ml_ind = Scan.lift (Args.name --
    55 val parser_ml_ind = Scan.lift (Args.name --
    56   Scan.option (Args.$$$ "in"  |-- OuterParse.!!! Args.name))
    56   Scan.option (Args.$$$ "in"  |-- Parse.!!! Args.name))
    57 
    57 
    58 (* checks and prints structures *)
    58 (* checks and prints structures *)
    59 fun gen_output_struct outfn {context = ctxt, ...} txt = 
    59 fun gen_output_struct outfn {context = ctxt, ...} txt = 
    60   (eval_fn ctxt (ml_struct txt); 
    60   (eval_fn ctxt (ml_struct txt); 
    61    outfn {main = Code txt, minor = Plain "structure"} (split_lines txt))
    61    outfn {main = Code txt, minor = Plain "structure"} (split_lines txt))