equal
deleted
inserted
replaced
989 mk_app false (mk_term_of gr "Generated" false T) |
989 mk_app false (mk_term_of gr "Generated" false T) |
990 [Pretty.str s'], Pretty.str ")"]]) frees')) @ |
990 [Pretty.str s'], Pretty.str ")"]]) frees')) @ |
991 [Pretty.str "]"])]], |
991 [Pretty.str "]"])]], |
992 Pretty.brk 1, Pretty.str "end"]), Pretty.str ");"]) ^ |
992 Pretty.brk 1, Pretty.str "end"]), Pretty.str ");"]) ^ |
993 "\n\nend;\n") (); |
993 "\n\nend;\n") (); |
994 val _ = use_text Output.ml_output false s; |
994 val _ = use_text "" Output.ml_output false s; |
995 fun iter f k = if k > i then NONE |
995 fun iter f k = if k > i then NONE |
996 else (case (f () handle Match => |
996 else (case (f () handle Match => |
997 (warning "Exception Match raised in generated code"; NONE)) of |
997 (warning "Exception Match raised in generated code"; NONE)) of |
998 NONE => iter f (k+1) | SOME x => SOME x); |
998 NONE => iter f (k+1) | SOME x => SOME x); |
999 fun test k = if k > sz then NONE |
999 fun test k = if k > sz then NONE |
1041 Pretty.brk 1, |
1041 Pretty.brk 1, |
1042 mk_app false (mk_term_of gr "Generated" false (fastype_of t)) |
1042 mk_app false (mk_term_of gr "Generated" false (fastype_of t)) |
1043 [Pretty.str "result"], |
1043 [Pretty.str "result"], |
1044 Pretty.str ";"]) ^ |
1044 Pretty.str ";"]) ^ |
1045 "\n\nend;\n"; |
1045 "\n\nend;\n"; |
1046 val _ = use_text Output.ml_output false s |
1046 val _ = use_text "" Output.ml_output false s |
1047 in !eval_result end); |
1047 in !eval_result end); |
1048 |
1048 |
1049 fun print_evaluated_term s = Toplevel.keep (fn state => |
1049 fun print_evaluated_term s = Toplevel.keep (fn state => |
1050 let |
1050 let |
1051 val ctxt = Toplevel.context_of state; |
1051 val ctxt = Toplevel.context_of state; |
1148 (fn ((((mode', module), opt_fname), modules), xs) => Toplevel.theory (fn thy => |
1148 (fn ((((mode', module), opt_fname), modules), xs) => Toplevel.theory (fn thy => |
1149 let |
1149 let |
1150 val mode'' = (if lib then insert (op =) "library" else I) (remove (op =) "library" mode'); |
1150 val mode'' = (if lib then insert (op =) "library" else I) (remove (op =) "library" mode'); |
1151 val (code, gr) = setmp mode mode'' (generate_code thy modules module) xs |
1151 val (code, gr) = setmp mode mode'' (generate_code thy modules module) xs |
1152 in ((case opt_fname of |
1152 in ((case opt_fname of |
1153 NONE => use_text Output.ml_output false |
1153 NONE => use_text "" Output.ml_output false |
1154 (space_implode "\n" (map snd code)) |
1154 (space_implode "\n" (map snd code)) |
1155 | SOME fname => |
1155 | SOME fname => |
1156 if lib then |
1156 if lib then |
1157 app (fn (name, s) => File.write |
1157 app (fn (name, s) => File.write |
1158 (Path.append (Path.explode fname) (Path.basic (name ^ ".ML"))) s) |
1158 (Path.append (Path.explode fname) (Path.basic (name ^ ".ML"))) s) |