shifted abstraction over imperative print mode
authorhaftmann
Thu Sep 23 11:29:22 2010 +0200 (2010-09-23)
changeset 3965907549694e2f1
parent 39647 7bf0c7f0f24c
child 39660 6ab9781e6d11
shifted abstraction over imperative print mode
src/Tools/Code/code_printer.ML
src/Tools/Code/code_target.ML
     1.1 --- a/src/Tools/Code/code_printer.ML	Thu Sep 23 10:39:25 2010 +0200
     1.2 +++ b/src/Tools/Code/code_printer.ML	Thu Sep 23 11:29:22 2010 +0200
     1.3 @@ -115,19 +115,19 @@
     1.4  infixr 5 @|;
     1.5  fun x @@ y = [x, y];
     1.6  fun xs @| y = xs @ [y];
     1.7 -val str = Print_Mode.setmp [] Pretty.str;
     1.8 +val str = Print_Mode.with_modes [] Pretty.str;
     1.9  val concat = Pretty.block o Pretty.breaks;
    1.10 -val commas = Print_Mode.setmp [] Pretty.commas;
    1.11 -fun enclose l r = Print_Mode.setmp [] (Pretty.enclose l r);
    1.12 +val commas = Print_Mode.with_modes [] Pretty.commas;
    1.13 +fun enclose l r = Print_Mode.with_modes [] (Pretty.enclose l r);
    1.14  val brackets = enclose "(" ")" o Pretty.breaks;
    1.15 -fun enum sep l r = Print_Mode.setmp [] (Pretty.enum sep l r);
    1.16 +fun enum sep l r = Print_Mode.with_modes [] (Pretty.enum sep l r);
    1.17  fun enum_default default sep l r [] = str default
    1.18    | enum_default default sep l r xs = enum sep l r xs;
    1.19  fun semicolon ps = Pretty.block [concat ps, str ";"];
    1.20  fun doublesemicolon ps = Pretty.block [concat ps, str ";;"];
    1.21 -fun indent i = Print_Mode.setmp [] (Pretty.indent i);
    1.22 +fun indent i = Print_Mode.with_modes [] (Pretty.indent i);
    1.23  
    1.24 -fun markup_stmt name = Print_Mode.setmp [code_presentationN]
    1.25 +fun markup_stmt name = Print_Mode.with_modes [code_presentationN]
    1.26    (Pretty.mark (code_presentationN, [(stmt_nameN, name)]));
    1.27  
    1.28  fun filter_presentation [] tree =
    1.29 @@ -150,7 +150,7 @@
    1.30        in snd (fold filter tree (true, Buffer.empty)) end;
    1.31  
    1.32  fun format presentation_names width =
    1.33 -  Print_Mode.setmp [code_presentationN] (Pretty.string_of_margin width)
    1.34 +  Print_Mode.with_modes [code_presentationN] (Pretty.string_of_margin width)
    1.35    #> YXML.parse_body
    1.36    #> filter_presentation presentation_names
    1.37    #> Buffer.content;
     2.1 --- a/src/Tools/Code/code_target.ML	Thu Sep 23 10:39:25 2010 +0200
     2.2 +++ b/src/Tools/Code/code_target.ML	Thu Sep 23 11:29:22 2010 +0200
     2.3 @@ -73,13 +73,21 @@
     2.4  datatype destination = Export of Path.T option | Produce | Present of string list;
     2.5  type serialization = int -> destination -> (string * (string -> string option)) option;
     2.6  
     2.7 -fun serialization output _ content width (Export some_path) = (output width some_path content; NONE)
     2.8 -  | serialization _ string content width Produce = SOME (string [] width content)
     2.9 -  | serialization _ string content width (Present stmt_names) = SOME (string stmt_names width content);
    2.10 +fun using_plain_output f x = Print_Mode.setmp [] f x;
    2.11  
    2.12 -fun export some_path f = (f (Export some_path); ());
    2.13 -fun produce f = the (f Produce);
    2.14 -fun present stmt_names f = fst (the (f (Present stmt_names)));
    2.15 +fun serialization output _ content width (Export some_path) =
    2.16 +      (using_plain_output (output width some_path) content; NONE)
    2.17 +  | serialization _ string content width Produce = 
    2.18 +      SOME (using_plain_output (string [] width) content)
    2.19 +  | serialization _ string content width (Present stmt_names) =
    2.20 +      SOME (using_plain_output (string stmt_names width) content);
    2.21 +
    2.22 +fun export some_path serializer naming program names =
    2.23 +  (using_plain_output (serializer naming program) names (Export some_path); ());
    2.24 +fun produce serializer naming program names =
    2.25 +  the (using_plain_output (serializer naming program) names Produce);
    2.26 +fun present stmt_names serializer naming program names =
    2.27 +  fst (the (using_plain_output (serializer naming program) names (Present stmt_names)));
    2.28  
    2.29  
    2.30  (** theory data **)
    2.31 @@ -351,20 +359,20 @@
    2.32  in
    2.33  
    2.34  fun export_code_for thy some_path target some_width module_name args =
    2.35 -  export some_path ooo mount_serializer thy target some_width module_name args;
    2.36 +  export some_path (mount_serializer thy target some_width module_name args);
    2.37  
    2.38  fun produce_code_for thy target some_width module_name args =
    2.39    let
    2.40      val serializer = mount_serializer thy target some_width (assert_module_name module_name) args;
    2.41    in fn naming => fn program => fn names =>
    2.42 -    produce (serializer naming program names) |> apsnd (fn deresolve => map deresolve names)
    2.43 +    produce serializer naming program names |> apsnd (fn deresolve => map deresolve names)
    2.44    end;
    2.45  
    2.46  fun present_code_for thy target some_width module_name args =
    2.47    let
    2.48      val serializer = mount_serializer thy target some_width (assert_module_name module_name) args;
    2.49    in fn naming => fn program => fn (names, selects) =>
    2.50 -    present selects (serializer naming program names)
    2.51 +    present selects serializer naming program names
    2.52    end;
    2.53  
    2.54  fun check_code_for thy target strict args naming program names_cs =
    2.55 @@ -377,7 +385,7 @@
    2.56        let 
    2.57          val destination = make_destination p;
    2.58          val _ = export (SOME destination) (mount_serializer thy target (SOME 80)
    2.59 -          module_name args naming program names_cs);
    2.60 +          module_name args) naming program names_cs;
    2.61          val cmd = make_command env_param module_name;
    2.62        in if bash ("cd " ^ File.shell_path p ^ " && " ^ cmd ^ " 2>&1") <> 0
    2.63          then error ("Code check failed for " ^ target ^ ": " ^ cmd)