20 in "val " ^ pat' ^ " = " ^ rhs end; |
20 in "val " ^ pat' ^ " = " ^ rhs end; |
21 |
21 |
22 fun ml_struct txt = "functor DUMMY_FUNCTOR() = struct structure DUMMY = " ^ txt ^ " end"; |
22 fun ml_struct txt = "functor DUMMY_FUNCTOR() = struct structure DUMMY = " ^ txt ^ " end"; |
23 fun ml_type txt = "val _ = NONE : (" ^ txt ^ ") option"; |
23 fun ml_type txt = "val _ = NONE : (" ^ txt ^ ") option"; |
24 |
24 |
25 fun output_ml_open ml src ctxt ((txt,ovars),pos) = |
25 fun output_ml ml src ctxt ((txt,ovars),pos) = |
26 (ML_Context.eval_in (SOME ctxt) false pos (ml ovars txt); |
26 (ML_Context.eval_in (SOME ctxt) false pos (ml ovars txt); |
27 ThyOutput.output_list (fn _ => fn s => Pretty.str s) src ctxt (space_explode "\n" txt)) |
27 ThyOutput.output_list (fn _ => fn s => Pretty.str s) src ctxt (space_explode "\n" txt)) |
28 |
28 |
29 fun output_ml ml src ctxt (txt,pos) = |
29 fun output_ml_aux ml src ctxt (txt,pos) = |
30 output_ml_open (K ml) src ctxt ((txt,()),pos) |
30 output_ml (K ml) src ctxt ((txt,()),pos) |
31 |
31 |
32 fun add_response_indicator txt = |
32 fun add_response_indicator txt = |
33 map (fn s => "> " ^ s) (space_explode "\n" txt) |
33 map (fn s => "> " ^ s) (space_explode "\n" txt) |
34 |
34 |
35 fun output_ml_response ml src ctxt ((lhs,pat),pos) = |
35 fun output_ml_response ml src ctxt ((lhs,pat),pos) = |
46 fun check_file_exists ctxt txt = |
46 fun check_file_exists ctxt txt = |
47 if File.exists (Path.append (Path.explode ("~~/src")) (Path.explode txt)) then () |
47 if File.exists (Path.append (Path.explode ("~~/src")) (Path.explode txt)) then () |
48 else error ("Source file " ^ quote txt ^ " does not exist.") |
48 else error ("Source file " ^ quote txt ^ " does not exist.") |
49 |
49 |
50 val _ = ThyOutput.add_commands |
50 val _ = ThyOutput.add_commands |
51 [("ML_open", ThyOutput.args (Scan.lift (OuterParse.position (Args.name -- |
51 [("ML", ThyOutput.args (Scan.lift (OuterParse.position (Args.name -- |
52 (Scan.optional (Args.$$$ "for" |-- OuterParse.!!! (Scan.repeat1 Args.name)) [] -- |
52 (Scan.optional (Args.$$$ "for" |-- OuterParse.!!! (Scan.repeat1 Args.name)) [] -- |
53 Scan.optional (Args.parens (OuterParse.list1 Args.name)) [])))) (output_ml_open ml_val_open)), |
53 Scan.optional (Args.$$$ "in" |-- OuterParse.!!! (Scan.repeat1 Args.name)) [])))) |
|
54 (output_ml ml_val_open)), |
54 ("ML_file", ThyOutput.args (Scan.lift Args.name) |
55 ("ML_file", ThyOutput.args (Scan.lift Args.name) |
55 (ThyOutput.output (fn _ => fn s => (check_file_exists s; Pretty.str s)))), |
56 (ThyOutput.output (fn _ => fn s => (check_file_exists s; Pretty.str s)))), |
56 ("ML_text", ThyOutput.args (Scan.lift Args.name) |
57 ("ML_text", ThyOutput.args (Scan.lift Args.name) |
57 (ThyOutput.output (fn _ => fn s => Pretty.str s))), |
58 (ThyOutput.output (fn _ => fn s => Pretty.str s))), |
58 ("ML", ThyOutput.args (Scan.lift (OuterParse.position Args.name)) (output_ml ml_val)), |
|
59 ("ML_response", ThyOutput.args (Scan.lift (OuterParse.position (Args.name -- Args.name))) |
59 ("ML_response", ThyOutput.args (Scan.lift (OuterParse.position (Args.name -- Args.name))) |
60 (output_ml_response ml_pat)), |
60 (output_ml_response ml_pat)), |
61 ("ML_response_fake", ThyOutput.args (Scan.lift (OuterParse.position (Args.name -- Args.name))) |
61 ("ML_response_fake", ThyOutput.args (Scan.lift (OuterParse.position (Args.name -- Args.name))) |
62 (output_ml_response_fake ml_val)), |
62 (output_ml_response_fake ml_val)), |
63 ("ML_struct", ThyOutput.args (Scan.lift (OuterParse.position Args.name)) (output_ml ml_struct)), |
63 ("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 ml_type))]; |
64 ("ML_type", ThyOutput.args (Scan.lift (OuterParse.position Args.name)) (output_ml_aux ml_type))]; |
65 |
65 |
66 end; |
66 end; |