33 Chunks.output_list (fn _ => fn s => Pretty.str s) src ctxt) |
33 Chunks.output_list (fn _ => fn s => Pretty.str s) src ctxt) |
34 |
34 |
35 fun output_ml_aux ml src ctxt (txt,pos) = |
35 fun output_ml_aux ml src ctxt (txt,pos) = |
36 output_ml (K ml) src ctxt ((txt,()),pos) |
36 output_ml (K ml) src ctxt ((txt,()),pos) |
37 |
37 |
38 fun add_response_indicator txt = |
38 fun string_explode str txt = |
39 map (fn s => "> " ^ s) (space_explode "\n" txt) |
39 map (fn s => str ^ s) (space_explode "\n" txt) |
40 |
40 |
41 fun output_ml_response ml src ctxt ((lhs,pat),pos) = |
41 fun output_ml_response ml src ctxt ((lhs,pat),pos) = |
42 (ML_Context.eval_in (SOME ctxt) false pos (ml (lhs,pat)); |
42 (ML_Context.eval_in (SOME ctxt) false pos (ml (lhs,pat)); |
43 let |
43 let |
44 val txt = (space_explode "\n" lhs) @ (add_response_indicator pat) |
44 val txt = (string_explode "" lhs) @ (string_explode "> " pat) |
45 in Chunks.output_list (fn _ => fn s => Pretty.str s) src ctxt txt end) |
45 in Chunks.output_list (fn _ => fn s => Pretty.str s) src ctxt txt end) |
46 |
46 |
47 fun output_ml_response_fake ml src ctxt ((lhs,pat),pos) = |
47 fun output_ml_response_fake ml src ctxt ((lhs,pat),pos) = |
48 (ML_Context.eval_in (SOME ctxt) false pos (ml lhs); |
48 (ML_Context.eval_in (SOME ctxt) false pos (ml lhs); |
49 let val txt = (space_explode "\n" lhs) @ (add_response_indicator pat) |
49 let val txt = (string_explode "" lhs) @ (string_explode "> " pat) |
50 in Chunks.output_list (fn _ => fn s => Pretty.str s) src ctxt txt end) |
50 in Chunks.output_list (fn _ => fn s => Pretty.str s) src ctxt txt end) |
51 |
51 |
52 fun output_ml_response_fake_both ml src ctxt ((lhs,pat),pos) = |
52 fun output_ml_response_fake_both src node = |
53 let val txt = (space_explode "\n" lhs) @ (add_response_indicator pat) |
53 let |
54 in Chunks.output_list (fn _ => fn s => Pretty.str s) src ctxt txt end |
54 fun ouput src ctxt (lhs,pat) = |
|
55 Chunks.output_list (fn _ => fn s => Pretty.str s) src ctxt |
|
56 ((string_explode "" lhs) @ (string_explode "> " pat)) |
|
57 in |
|
58 ThyOutput.args (Scan.lift (Args.name -- Args.name)) ouput src node |
|
59 end |
55 |
60 |
56 fun check_file_exists src node = |
61 fun check_file_exists src node = |
57 let |
62 let |
58 fun check txt = |
63 fun check txt = |
59 if File.exists (Path.append (Path.explode ("~~/src")) (Path.explode txt)) then () |
64 if File.exists (Path.append (Path.explode ("~~/src")) (Path.explode txt)) then () |
98 ("ML_file", check_file_exists), |
103 ("ML_file", check_file_exists), |
99 ("ML_response", ThyOutput.args (Scan.lift (OuterParse.position (Args.name -- Args.name))) |
104 ("ML_response", ThyOutput.args (Scan.lift (OuterParse.position (Args.name -- Args.name))) |
100 (output_ml_response ml_pat)), |
105 (output_ml_response ml_pat)), |
101 ("ML_response_fake", ThyOutput.args (Scan.lift (OuterParse.position (Args.name -- Args.name))) |
106 ("ML_response_fake", ThyOutput.args (Scan.lift (OuterParse.position (Args.name -- Args.name))) |
102 (output_ml_response_fake ml_val)), |
107 (output_ml_response_fake ml_val)), |
103 ("ML_response_fake_both", ThyOutput.args (Scan.lift (OuterParse.position (Args.name -- Args.name))) |
108 ("ML_response_fake_both", output_ml_response_fake_both), |
104 (output_ml_response_fake_both ml_val)), |
|
105 ("ML_struct", ThyOutput.args (Scan.lift (OuterParse.position Args.name)) (output_ml_aux ml_struct)), |
109 ("ML_struct", ThyOutput.args (Scan.lift (OuterParse.position Args.name)) (output_ml_aux ml_struct)), |
106 ("ML_type", ThyOutput.args (Scan.lift (OuterParse.position Args.name)) (output_ml_aux ml_type)), |
110 ("ML_type", ThyOutput.args (Scan.lift (OuterParse.position Args.name)) (output_ml_aux ml_type)), |
107 ("subgoals", output_goals)]; |
111 ("subgoals", output_goals)]; |
108 |
112 |
109 end; |
113 end; |