equal
deleted
inserted
replaced
52 fun ml_exn (txt1, "") = "fn _ => (" ^ txt1 ^ ": exn);" |
52 fun ml_exn (txt1, "") = "fn _ => (" ^ txt1 ^ ": exn);" |
53 | ml_exn (txt1, txt2) = "fn _ => (" ^ txt1 ^ ": " ^ txt2 ^ " -> exn);"; |
53 | ml_exn (txt1, txt2) = "fn _ => (" ^ txt1 ^ ": " ^ txt2 ^ " -> exn);"; |
54 |
54 |
55 fun ml_structure (txt, _) = "functor XXX() = struct structure XX = " ^ txt ^ " end;"; |
55 fun ml_structure (txt, _) = "functor XXX() = struct structure XX = " ^ txt ^ " end;"; |
56 |
56 |
57 fun ml_functor _ = ""; (*no check!*) |
57 fun ml_functor (txt, _) = "ML_Env.check_functor " ^ ML_Syntax.print_string txt; |
58 |
58 |
59 fun index_ml name kind ml = ThyOutput.antiquotation name |
59 fun index_ml name kind ml = ThyOutput.antiquotation name |
60 (Scan.lift (Args.name -- Scan.optional (Args.colon |-- Args.name) "")) |
60 (Scan.lift (Args.name -- Scan.optional (Args.colon |-- Args.name) "")) |
61 (fn {context = ctxt, ...} => fn (txt1, txt2) => |
61 (fn {context = ctxt, ...} => fn (txt1, txt2) => |
62 let |
62 let |