--- a/src/Pure/Tools/codegen_package.ML Tue Dec 06 16:07:25 2005 +0100
+++ b/src/Pure/Tools/codegen_package.ML Tue Dec 06 17:11:40 2005 +0100
@@ -88,6 +88,13 @@
fun devarify_term t = (fst o Type.freeze_thaw) t;
fun devarify_type ty = (fst o Type.freeze_thaw_type) ty;
+fun newline_correct s =
+ s
+ |> space_explode "\n"
+ |> map (implode o (fn [] => []
+ | (" "::xs) => xs
+ | xs => xs) o explode)
+ |> space_implode "\n";
(* code generator instantiation, part 1 *)
@@ -1159,7 +1166,7 @@
(* syntax *)
-fun gen_add_syntax_tyco prep_tyco prep_mfx prep_primname serial_name ((raw_tyco, raw_mfx), primdef) thy =
+fun gen_add_syntax_tyco prep_tyco prep_mfx prep_primname prep_primdef serial_name ((raw_tyco, raw_mfx), primdef) thy =
let
val tyco = prep_tyco thy raw_tyco;
val _ = if member (op =) prims tyco
@@ -1167,7 +1174,7 @@
else ()
fun add_primdef NONE = I
| add_primdef (SOME (name, (def, deps))) =
- CodegenSerializer.add_prim (prep_primname thy tyco name, (def, deps))
+ CodegenSerializer.add_prim (prep_primname thy tyco name, (prep_primdef def, deps))
in
thy
|> prep_mfx raw_mfx
@@ -1183,7 +1190,7 @@
logic_data)))
end;
-val add_syntax_tyco_i = gen_add_syntax_tyco (K I) pair ((K o K) I);
+val add_syntax_tyco_i = gen_add_syntax_tyco (K I) pair ((K o K) I) I;
val add_syntax_tyco =
let
fun mk_name _ _ (SOME name) = name
@@ -1208,10 +1215,10 @@
end;
in
gen_add_syntax_tyco (fn thy => idf_of_tname thy o Sign.intern_type thy)
- prep_mfx mk_name
+ prep_mfx mk_name (newline_correct o Symbol.strip_blanks)
end;
-fun gen_add_syntax_const prep_const prep_mfx prep_primname serial_name ((raw_f, raw_mfx), primdef) thy =
+fun gen_add_syntax_const prep_const prep_mfx prep_primname prep_primdef serial_name ((raw_f, raw_mfx), primdef) thy =
let
val f = prep_const thy raw_f;
val _ = if member (op =) prims f
@@ -1219,7 +1226,7 @@
else ()
fun add_primdef NONE = I
| add_primdef (SOME (name, (def, deps))) =
- CodegenSerializer.add_prim (prep_primname thy f name, (def, deps))
+ CodegenSerializer.add_prim (prep_primname thy f name, (prep_primdef def, deps))
in
thy
|> prep_mfx raw_mfx
@@ -1235,7 +1242,7 @@
logic_data)))
end;
-val add_syntax_const_i = gen_add_syntax_const (K I) pair ((K o K) I);
+val add_syntax_const_i = gen_add_syntax_const (K I) pair ((K o K) I) I;
val add_syntax_const =
let
fun prep_const thy (raw_f, raw_ty) =
@@ -1268,7 +1275,7 @@
|-> (fn es => pair (Codegen.replace_quotes es proto_mfx))
end;
in
- gen_add_syntax_const prep_const prep_mfx mk_name
+ gen_add_syntax_const prep_const prep_mfx mk_name (newline_correct o Symbol.strip_blanks)
end;
--- a/src/Pure/Tools/codegen_serializer.ML Tue Dec 06 16:07:25 2005 +0100
+++ b/src/Pure/Tools/codegen_serializer.ML Tue Dec 06 17:11:40 2005 +0100
@@ -644,7 +644,7 @@
|> eliminate_classes
|> debug 3 (fn _ => "generating...")
|> serialize (ml_from_defs tyco_syntax const_syntax) ml_from_module ml_validator nspgrp name_root
- |> (fn p => Pretty.chunks [(Pretty.str o mk_prims) prims, p])
+ |> (fn p => Pretty.chunks [setmp print_mode [] (Pretty.str o mk_prims) prims, p])
end;
fun ml_from_thingol' nspgrp name_root =
@@ -664,8 +664,6 @@
local
-val bslash = "\\";
-
fun haskell_from_defs tyco_syntax const_syntax is_cons resolv defs =
let
val resolv = fn s =>
@@ -822,7 +820,7 @@
val (vs, body) = unfold_abs e
in
brackify (eval_br br BR) (
- Pretty.str bslash
+ Pretty.str "\\"
:: map (Pretty.str o lower_first o fst) vs @ [
Pretty.str "->",
haskell_from_expr NOBR body
@@ -958,7 +956,6 @@
end;
fun haskell_from_classes defs =
let
- val _ = writeln ("IDS: " ^ (commas o map fst) defs)
fun mk_member (f, ty) =
Pretty.block [
Pretty.str (f ^ " ::"),
@@ -1092,7 +1089,7 @@
|> eta_expand eta_expander
|> debug 3 (fn _ => "generating...")
|> serialize (haskell_from_defs tyco_syntax const_syntax is_cons) haskell_from_module haskell_validator nspgrp name_root
- |> (fn p => Pretty.chunks [(Pretty.str o mk_prims) prims, p])
+ |> (fn p => Pretty.chunks [setmp print_mode [] (Pretty.str o mk_prims) prims, p])
end;
end; (* local *)
--- a/src/Pure/Tools/codegen_thingol.ML Tue Dec 06 16:07:25 2005 +0100
+++ b/src/Pure/Tools/codegen_thingol.ML Tue Dec 06 17:11:40 2005 +0100
@@ -1311,8 +1311,8 @@
| seri prfx ds =
s_def (resolver prfx) (map (fn (name, Def def) => (resolver prfx (prfx @ [name] |> NameSpace.pack), def)) ds)
in
- setmp print_mode [] s_module (name_root, (map (seri [])
- ((map (AList.make (Graph.get_node module)) o rev o Graph.strong_conn) module)))
+ setmp print_mode [] (fn _ => s_module (name_root, (map (seri [])
+ ((map (AList.make (Graph.get_node module)) o rev o Graph.strong_conn) module)))) ()
end;
end; (* struct *)