# HG changeset patch # User haftmann # Date 1285234162 -7200 # Node ID 07549694e2f1267b00fb7b43f681bd4a1b4b2629 # Parent 7bf0c7f0f24c5be6dab77a68eb7e82a6c7603c55 shifted abstraction over imperative print mode diff -r 7bf0c7f0f24c -r 07549694e2f1 src/Tools/Code/code_printer.ML --- a/src/Tools/Code/code_printer.ML Thu Sep 23 10:39:25 2010 +0200 +++ b/src/Tools/Code/code_printer.ML Thu Sep 23 11:29:22 2010 +0200 @@ -115,19 +115,19 @@ infixr 5 @|; fun x @@ y = [x, y]; fun xs @| y = xs @ [y]; -val str = Print_Mode.setmp [] Pretty.str; +val str = Print_Mode.with_modes [] Pretty.str; val concat = Pretty.block o Pretty.breaks; -val commas = Print_Mode.setmp [] Pretty.commas; -fun enclose l r = Print_Mode.setmp [] (Pretty.enclose l r); +val commas = Print_Mode.with_modes [] Pretty.commas; +fun enclose l r = Print_Mode.with_modes [] (Pretty.enclose l r); val brackets = enclose "(" ")" o Pretty.breaks; -fun enum sep l r = Print_Mode.setmp [] (Pretty.enum sep l r); +fun enum sep l r = Print_Mode.with_modes [] (Pretty.enum sep l r); fun enum_default default sep l r [] = str default | enum_default default sep l r xs = enum sep l r xs; fun semicolon ps = Pretty.block [concat ps, str ";"]; fun doublesemicolon ps = Pretty.block [concat ps, str ";;"]; -fun indent i = Print_Mode.setmp [] (Pretty.indent i); +fun indent i = Print_Mode.with_modes [] (Pretty.indent i); -fun markup_stmt name = Print_Mode.setmp [code_presentationN] +fun markup_stmt name = Print_Mode.with_modes [code_presentationN] (Pretty.mark (code_presentationN, [(stmt_nameN, name)])); fun filter_presentation [] tree = @@ -150,7 +150,7 @@ in snd (fold filter tree (true, Buffer.empty)) end; fun format presentation_names width = - Print_Mode.setmp [code_presentationN] (Pretty.string_of_margin width) + Print_Mode.with_modes [code_presentationN] (Pretty.string_of_margin width) #> YXML.parse_body #> filter_presentation presentation_names #> Buffer.content; diff -r 7bf0c7f0f24c -r 07549694e2f1 src/Tools/Code/code_target.ML --- a/src/Tools/Code/code_target.ML Thu Sep 23 10:39:25 2010 +0200 +++ b/src/Tools/Code/code_target.ML Thu Sep 23 11:29:22 2010 +0200 @@ -73,13 +73,21 @@ datatype destination = Export of Path.T option | Produce | Present of string list; type serialization = int -> destination -> (string * (string -> string option)) option; -fun serialization output _ content width (Export some_path) = (output width some_path content; NONE) - | serialization _ string content width Produce = SOME (string [] width content) - | serialization _ string content width (Present stmt_names) = SOME (string stmt_names width content); +fun using_plain_output f x = Print_Mode.setmp [] f x; -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))); +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) + | serialization _ string content width (Present stmt_names) = + SOME (using_plain_output (string stmt_names width) content); + +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))); (** theory data **) @@ -351,20 +359,20 @@ in fun export_code_for thy some_path target some_width module_name args = - export some_path ooo mount_serializer thy target some_width module_name args; + export some_path (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 = @@ -377,7 +385,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)