34 (if ! ThyOutput.source then str_of_source src else txt) |
34 (if ! ThyOutput.source then str_of_source src else txt) |
35 |> (if ! ThyOutput.quotes then quote else I) |
35 |> (if ! ThyOutput.quotes then quote else I) |
36 |> ThyOutput.output (fn _ => fn s => Pretty.str s) src ctxt |
36 |> ThyOutput.output (fn _ => fn s => Pretty.str s) src ctxt |
37 end; |
37 end; |
38 |
38 |
39 fun output_ml ml = output_verbatim |
39 fun output_ml_old ml = output_verbatim |
40 (fn ctxt => fn ((txt, p), pos) => |
40 (fn ctxt => fn ((txt, p), pos) => |
41 (ML_Context.eval_in (SOME ctxt) false pos (ml p txt); |
41 (ML_Context.eval_in (SOME ctxt) false pos (ml p txt); |
42 txt |> Source.of_string |> ML_Lex.source |> Source.exhaust |> |
42 txt |> Source.of_string |> ML_Lex.source |> Source.exhaust |> |
43 Chunks.transform_cmts |> implode)); |
43 Chunks.transform_cmts |> implode)); |
44 |
44 |
45 fun output_ml_response ml = output_verbatim |
45 fun output_ml ml src ctxt txt = |
46 (fn ctxt => fn ((x as (rhs, pat), p), pos) => |
46 (ML_Context.eval_in (SOME ctxt) false Position.none (ml txt); |
47 (ML_Context.eval_in (SOME ctxt) false pos (ml p x); |
47 ThyOutput.output (fn _ => fn s => Pretty.str s) src ctxt txt) |
48 rhs ^ "\n" ^ |
|
49 space_implode "\n" (map (fn s => "> " ^ s) |
|
50 (space_explode "\n" pat)))); |
|
51 |
48 |
52 fun output_ml_checked ml src ctxt (txt, pos) = |
49 fun add_response_indicator txt = |
53 (ML_Context.eval_in (SOME ctxt) false pos (ml txt); |
50 space_implode "\n" (map (fn s => "> " ^ s) (space_explode "\n" txt)) |
54 (if ! ThyOutput.source then str_of_source src else SymbolPos.content (SymbolPos.explode (txt, pos))) |
51 |
55 |> (if ! ThyOutput.quotes then quote else I) |
52 fun output_ml_response ml src ctxt (lhs,pat) = |
56 |> ThyOutput.output (fn _ => fn s => Pretty.str s) src ctxt) |
53 (ML_Context.eval_in (SOME ctxt) false Position.none (ml (lhs,pat)); |
|
54 let val txt = lhs ^ "\n" ^ (add_response_indicator pat) |
|
55 in ThyOutput.output (fn _ => fn s => Pretty.str s) src ctxt txt end) |
|
56 |
|
57 fun output_ml_response_fake ml src ctxt (lhs,pat) = |
|
58 (ML_Context.eval_in (SOME ctxt) false Position.none (ml lhs); |
|
59 let val txt = lhs ^ "\n" ^ (add_response_indicator pat) |
|
60 in ThyOutput.output (fn _ => fn s => Pretty.str s) src ctxt txt end) |
57 |
61 |
58 fun check_file_exists ctxt name = |
62 fun check_file_exists ctxt name = |
59 if File.exists (Path.append (Path.explode ("~~/src")) (Path.explode name)) then () |
63 if File.exists (Path.append (Path.explode ("~~/src")) (Path.explode name)) then () |
60 else error ("Source file " ^ quote name ^ " does not exist.") |
64 else error ("Source file " ^ quote name ^ " does not exist.") |
61 |
65 |
|
66 |
|
67 |
62 val _ = ThyOutput.add_commands |
68 val _ = ThyOutput.add_commands |
63 [("ML_open", ThyOutput.args (Scan.lift (OuterParse.position (Args.name -- |
69 [("ML_open", ThyOutput.args (Scan.lift (OuterParse.position (Args.name -- |
64 (Scan.optional (Args.$$$ "for" |-- OuterParse.!!! (Scan.repeat1 Args.name)) [] -- |
70 (Scan.optional (Args.$$$ "for" |-- OuterParse.!!! (Scan.repeat1 Args.name)) [] -- |
65 Scan.optional (Args.parens (OuterParse.list1 Args.name)) [])))) (output_ml ml_val_open)), |
71 Scan.optional (Args.parens (OuterParse.list1 Args.name)) [])))) (output_ml_old ml_val_open)), |
66 ("ML_response", ThyOutput.args (Scan.lift (OuterParse.position |
|
67 ((Args.name -- Args.name) >> rpair ()))) (output_ml_response (K ml_pat))), |
|
68 ("ML_file", ThyOutput.args (Scan.lift Args.name) |
72 ("ML_file", ThyOutput.args (Scan.lift Args.name) |
69 (ThyOutput.output (fn _ => fn name => (check_file_exists name; Pretty.str name)))), |
73 (ThyOutput.output (fn _ => fn s => (check_file_exists s; Pretty.str s)))), |
70 ("ML_text", ThyOutput.args (Scan.lift Args.name) |
74 ("ML_text", ThyOutput.args (Scan.lift Args.name) |
71 (ThyOutput.output (fn _ => fn s => Pretty.str s))), |
75 (ThyOutput.output (fn _ => fn s => Pretty.str s))), |
72 ("ML", ThyOutput.args (Scan.lift Args.name_source_position) (output_ml_checked ml_val)), |
76 ("ML", ThyOutput.args (Scan.lift Args.name) (output_ml ml_val)), |
73 ("ML_struct", ThyOutput.args (Scan.lift Args.name_source_position) (output_ml_checked ml_struct)), |
77 ("ML_response", ThyOutput.args (Scan.lift (Args.name -- Args.name)) (output_ml_response ml_pat)), |
74 ("ML_type", ThyOutput.args (Scan.lift Args.name_source_position) (output_ml_checked ml_type))]; |
78 ("ML_response_fake", |
|
79 ThyOutput.args (Scan.lift (Args.name -- Args.name)) (output_ml_response_fake ml_val)), |
|
80 ("ML_struct", ThyOutput.args (Scan.lift Args.name) (output_ml ml_struct)), |
|
81 ("ML_type", ThyOutput.args (Scan.lift Args.name) (output_ml ml_type))]; |
75 |
82 |
76 end; |
83 end; |