reverted cs 07549694e2f1 -- use re-printing with current print mode instead after code assembly, avoid Latex.output_typewriter
authorhaftmann
Thu Sep 23 13:23:22 2010 +0200 (2010-09-23)
changeset 396616381d18507ef
parent 39660 6ab9781e6d11
child 39662 86595d7b59b5
reverted cs 07549694e2f1 -- use re-printing with current print mode instead after code assembly, avoid Latex.output_typewriter
src/Tools/Code/code_target.ML
     1.1 --- a/src/Tools/Code/code_target.ML	Thu Sep 23 13:23:21 2010 +0200
     1.2 +++ b/src/Tools/Code/code_target.ML	Thu Sep 23 13:23:22 2010 +0200
     1.3 @@ -73,21 +73,18 @@
     1.4  datatype destination = Export of Path.T option | Produce | Present of string list;
     1.5  type serialization = int -> destination -> (string * (string -> string option)) option;
     1.6  
     1.7 -fun using_plain_output f x = Print_Mode.setmp [] f x;
     1.8 -
     1.9  fun serialization output _ content width (Export some_path) =
    1.10 -      (using_plain_output (output width some_path) content; NONE)
    1.11 -  | serialization _ string content width Produce = 
    1.12 -      SOME (using_plain_output (string [] width) content)
    1.13 +      (output width some_path content; NONE)
    1.14 +  | serialization _ string content width Produce =
    1.15 +      string [] width content |> SOME
    1.16    | serialization _ string content width (Present stmt_names) =
    1.17 -      SOME (using_plain_output (string stmt_names width) content);
    1.18 +     string stmt_names width content
    1.19 +     |> apfst (Pretty.output (SOME width) o Pretty.str)
    1.20 +     |> SOME;
    1.21  
    1.22 -fun export some_path serializer naming program names =
    1.23 -  (using_plain_output (serializer naming program) names (Export some_path); ());
    1.24 -fun produce serializer naming program names =
    1.25 -  the (using_plain_output (serializer naming program) names Produce);
    1.26 -fun present stmt_names serializer naming program names =
    1.27 -  fst (the (using_plain_output (serializer naming program) names (Present stmt_names)));
    1.28 +fun export some_path f = (f (Export some_path); ());
    1.29 +fun produce f = the (f Produce);
    1.30 +fun present stmt_names f = fst (the (f (Present stmt_names)));
    1.31  
    1.32  
    1.33  (** theory data **)
    1.34 @@ -359,20 +356,20 @@
    1.35  in
    1.36  
    1.37  fun export_code_for thy some_path target some_width module_name args =
    1.38 -  export some_path (mount_serializer thy target some_width module_name args);
    1.39 +  export some_path ooo mount_serializer thy target some_width module_name args;
    1.40  
    1.41  fun produce_code_for thy target some_width module_name args =
    1.42    let
    1.43      val serializer = mount_serializer thy target some_width (assert_module_name module_name) args;
    1.44    in fn naming => fn program => fn names =>
    1.45 -    produce serializer naming program names |> apsnd (fn deresolve => map deresolve names)
    1.46 +    produce (serializer naming program names) |> apsnd (fn deresolve => map deresolve names)
    1.47    end;
    1.48  
    1.49  fun present_code_for thy target some_width module_name args =
    1.50    let
    1.51      val serializer = mount_serializer thy target some_width (assert_module_name module_name) args;
    1.52    in fn naming => fn program => fn (names, selects) =>
    1.53 -    present selects serializer naming program names
    1.54 +    present selects (serializer naming program names)
    1.55    end;
    1.56  
    1.57  fun check_code_for thy target strict args naming program names_cs =
    1.58 @@ -385,7 +382,7 @@
    1.59        let 
    1.60          val destination = make_destination p;
    1.61          val _ = export (SOME destination) (mount_serializer thy target (SOME 80)
    1.62 -          module_name args) naming program names_cs;
    1.63 +          module_name args naming program names_cs);
    1.64          val cmd = make_command env_param module_name;
    1.65        in if bash ("cd " ^ File.shell_path p ^ " && " ^ cmd ^ " 2>&1") <> 0
    1.66          then error ("Code check failed for " ^ target ^ ": " ^ cmd)
    1.67 @@ -483,7 +480,7 @@
    1.68        present_code thy (mk_cs thy)
    1.69          (fn naming => maps (fn f => f thy naming) mk_stmtss)
    1.70          target some_width "Example" []
    1.71 -      |> Latex.output_typewriter
    1.72 +      (*|> Latex.output_typewriter*)
    1.73      end);
    1.74  
    1.75  end;