equal
deleted
inserted
replaced
41 fun output_ml_response_fake ml src ctxt ((lhs,pat),pos) = |
41 fun output_ml_response_fake ml src ctxt ((lhs,pat),pos) = |
42 (ML_Context.eval_in (SOME ctxt) false pos (ml lhs); |
42 (ML_Context.eval_in (SOME ctxt) false pos (ml lhs); |
43 let val txt = (space_explode "\n" lhs) @ (add_response_indicator pat) |
43 let val txt = (space_explode "\n" lhs) @ (add_response_indicator pat) |
44 in ThyOutput.output_list (fn _ => fn s => Pretty.str s) src ctxt txt end) |
44 in ThyOutput.output_list (fn _ => fn s => Pretty.str s) src ctxt txt end) |
45 |
45 |
|
46 fun output_ml_response_fake_both ml src ctxt ((lhs,pat),pos) = |
|
47 let val txt = (space_explode "\n" lhs) @ (add_response_indicator pat) |
|
48 in ThyOutput.output_list (fn _ => fn s => Pretty.str s) src ctxt txt end |
|
49 |
46 fun check_file_exists ctxt txt = |
50 fun check_file_exists ctxt txt = |
47 if File.exists (Path.append (Path.explode ("~~/src")) (Path.explode txt)) then () |
51 if File.exists (Path.append (Path.explode ("~~/src")) (Path.explode txt)) then () |
48 else error ("Source file " ^ quote txt ^ " does not exist.") |
52 else error ("Source file " ^ quote txt ^ " does not exist.") |
49 |
53 |
50 val _ = ThyOutput.add_commands |
54 val _ = ThyOutput.add_commands |
58 (ThyOutput.output (fn _ => fn s => Pretty.str s))), |
62 (ThyOutput.output (fn _ => fn s => Pretty.str s))), |
59 ("ML_response", ThyOutput.args (Scan.lift (OuterParse.position (Args.name -- Args.name))) |
63 ("ML_response", ThyOutput.args (Scan.lift (OuterParse.position (Args.name -- Args.name))) |
60 (output_ml_response ml_pat)), |
64 (output_ml_response ml_pat)), |
61 ("ML_response_fake", ThyOutput.args (Scan.lift (OuterParse.position (Args.name -- Args.name))) |
65 ("ML_response_fake", ThyOutput.args (Scan.lift (OuterParse.position (Args.name -- Args.name))) |
62 (output_ml_response_fake ml_val)), |
66 (output_ml_response_fake ml_val)), |
|
67 ("ML_response_fake_both", ThyOutput.args (Scan.lift (OuterParse.position (Args.name -- Args.name))) |
|
68 (output_ml_response_fake_both ml_val)), |
63 ("ML_struct", ThyOutput.args (Scan.lift (OuterParse.position Args.name)) (output_ml_aux ml_struct)), |
69 ("ML_struct", ThyOutput.args (Scan.lift (OuterParse.position Args.name)) (output_ml_aux ml_struct)), |
64 ("ML_type", ThyOutput.args (Scan.lift (OuterParse.position Args.name)) (output_ml_aux ml_type))]; |
70 ("ML_type", ThyOutput.args (Scan.lift (OuterParse.position Args.name)) (output_ml_aux ml_type))]; |
65 |
71 |
66 end; |
72 end; |