diff -r 6ab9781e6d11 -r 6381d18507ef src/Tools/Code/code_target.ML --- a/src/Tools/Code/code_target.ML Thu Sep 23 13:23:21 2010 +0200 +++ b/src/Tools/Code/code_target.ML Thu Sep 23 13:23:22 2010 +0200 @@ -73,21 +73,18 @@ datatype destination = Export of Path.T option | Produce | Present of string list; type serialization = int -> destination -> (string * (string -> string option)) option; -fun using_plain_output f x = Print_Mode.setmp [] f x; - fun serialization output _ content width (Export some_path) = - (using_plain_output (output width some_path) content; NONE) - | serialization _ string content width Produce = - SOME (using_plain_output (string [] width) content) + (output width some_path content; NONE) + | serialization _ string content width Produce = + string [] width content |> SOME | serialization _ string content width (Present stmt_names) = - SOME (using_plain_output (string stmt_names width) content); + string stmt_names width content + |> apfst (Pretty.output (SOME width) o Pretty.str) + |> SOME; -fun export some_path serializer naming program names = - (using_plain_output (serializer naming program) names (Export some_path); ()); -fun produce serializer naming program names = - the (using_plain_output (serializer naming program) names Produce); -fun present stmt_names serializer naming program names = - fst (the (using_plain_output (serializer naming program) names (Present stmt_names))); +fun export some_path f = (f (Export some_path); ()); +fun produce f = the (f Produce); +fun present stmt_names f = fst (the (f (Present stmt_names))); (** theory data **) @@ -359,20 +356,20 @@ in fun export_code_for thy some_path target some_width module_name args = - export some_path (mount_serializer thy target some_width module_name args); + export some_path ooo mount_serializer thy target some_width module_name args; fun produce_code_for thy target some_width module_name args = let val serializer = mount_serializer thy target some_width (assert_module_name module_name) args; in fn naming => fn program => fn names => - produce serializer naming program names |> apsnd (fn deresolve => map deresolve names) + produce (serializer naming program names) |> apsnd (fn deresolve => map deresolve names) end; fun present_code_for thy target some_width module_name args = let val serializer = mount_serializer thy target some_width (assert_module_name module_name) args; in fn naming => fn program => fn (names, selects) => - present selects serializer naming program names + present selects (serializer naming program names) end; fun check_code_for thy target strict args naming program names_cs = @@ -385,7 +382,7 @@ let val destination = make_destination p; val _ = export (SOME destination) (mount_serializer thy target (SOME 80) - module_name args) naming program names_cs; + module_name args naming program names_cs); val cmd = make_command env_param module_name; in if bash ("cd " ^ File.shell_path p ^ " && " ^ cmd ^ " 2>&1") <> 0 then error ("Code check failed for " ^ target ^ ": " ^ cmd) @@ -483,7 +480,7 @@ present_code thy (mk_cs thy) (fn naming => maps (fn f => f thy naming) mk_stmtss) target some_width "Example" [] - |> Latex.output_typewriter + (*|> Latex.output_typewriter*) end); end;