--- a/src/Tools/Code/code_haskell.ML Thu Sep 02 13:43:38 2010 +0200
+++ b/src/Tools/Code/code_haskell.ML Thu Sep 02 13:58:16 2010 +0200
@@ -381,7 +381,7 @@
val import_ps = map print_import_include includes @ map print_import_module imports
val content = Pretty.chunks2 ((if null import_ps then [] else [Pretty.chunks import_ps])
@ map_filter
- (fn (name, (_, SOME stmt)) => SOME (print_stmt qualified (name, stmt))
+ (fn (name, (_, SOME stmt)) => SOME (markup_stmt name (print_stmt qualified (name, stmt)))
| (_, (_, NONE)) => NONE) stmts
);
in print_module module_name' content end;
@@ -404,9 +404,9 @@
val _ = File.mkdir_leaf (Path.dir pathname);
in File.write pathname
("{-# OPTIONS_GHC -fglasgow-exts #-}\n\n"
- ^ format false width content)
+ ^ format [] width content)
end
- | write_module width NONE (_, content) = writeln (format false width content);
+ | write_module width NONE (_, content) = writeln (format [] width content);
in
Code_Target.serialization
(fn width => fn destination => K () o map (write_module width destination))
--- a/src/Tools/Code/code_ml.ML Thu Sep 02 13:43:38 2010 +0200
+++ b/src/Tools/Code/code_ml.ML Thu Sep 02 13:58:16 2010 +0200
@@ -793,14 +793,15 @@
val is_presentation = not (null presentation_names);
val { deresolver, hierarchical_program = ml_program } =
ml_program_of_program labelled_name (Name.make_context reserved_syms) module_alias program;
+ val print_stmt = print_stmt labelled_name tyco_syntax const_syntax
+ (make_vars reserved_syms) is_cons;
fun print_node _ (_, Code_Namespace.Dummy) =
NONE
- | print_node prefix_fragments (_, Code_Namespace.Stmt stmt) =
+ | print_node prefix_fragments (name, Code_Namespace.Stmt stmt) =
if is_presentation andalso
(null o filter (member (op =) presentation_names) o stmt_names_of) stmt
then NONE
- else SOME (print_stmt labelled_name tyco_syntax const_syntax (make_vars reserved_syms)
- is_cons (deresolver prefix_fragments) stmt)
+ else SOME (apsnd (markup_stmt name) (print_stmt (deresolver prefix_fragments) stmt))
| print_node prefix_fragments (name_fragment, Code_Namespace.Module (_, nodes)) =
let
val (decls, body) = print_nodes (prefix_fragments @ [name_fragment]) nodes;
@@ -815,8 +816,8 @@
|> (fn (decls, body) => (flat decls, body))
val names' = map (try (deresolver [])) names;
val p = Pretty.chunks2 (map snd includes @ snd (print_nodes [] ml_program));
- fun write width NONE = writeln o format false width
- | write width (SOME p) = File.write p o format false width;
+ fun write width NONE = writeln o format [] width
+ | write width (SOME p) = File.write p o format [] width;
in
Code_Target.serialization write (rpair names' ooo format) p
end;
--- a/src/Tools/Code/code_printer.ML Thu Sep 02 13:43:38 2010 +0200
+++ b/src/Tools/Code/code_printer.ML Thu Sep 02 13:58:16 2010 +0200
@@ -25,8 +25,8 @@
val semicolon: Pretty.T list -> Pretty.T
val doublesemicolon: Pretty.T list -> Pretty.T
val indent: int -> Pretty.T -> Pretty.T
- val markup_stmt: string -> Pretty.T list -> Pretty.T
- val format: bool -> int -> Pretty.T -> string
+ val markup_stmt: string -> Pretty.T -> Pretty.T
+ val format: string list -> int -> Pretty.T -> string
val first_upper: string -> string
val first_lower: string -> string
@@ -128,20 +128,21 @@
fun indent i = Print_Mode.setmp [] (Pretty.indent i);
val stmt_nameN = "stmt_name";
-fun markup_stmt name = Pretty.markup (code_presentationN, [(stmt_nameN, name)]);
-fun filter_presentation selected (XML.Elem ((name, _), xs)) =
- implode (map (filter_presentation (selected orelse name = code_presentationN)) xs)
- | filter_presentation selected (XML.Text s) =
+fun markup_stmt name = Pretty.mark (code_presentationN, [(stmt_nameN, name)]);
+fun filter_presentation presentation_names selected (XML.Elem ((name, attrs), xs)) =
+ implode (map (filter_presentation presentation_names
+ (selected orelse (name = code_presentationN
+ andalso member (op =) presentation_names (the (Properties.get attrs stmt_nameN))))) xs)
+ | filter_presentation presentation_names selected (XML.Text s) =
if selected then s else "";
-fun format presentation_only width p =
- if presentation_only then
- Print_Mode.setmp [code_presentationN] (Pretty.string_of_margin width) p
+fun format presentation_names width p =
+ if null presentation_names then Print_Mode.setmp [] (Pretty.string_of_margin width) p ^ "\n"
+ else Print_Mode.setmp [code_presentationN] (Pretty.string_of_margin width) p
|> YXML.parse_body
- |> map (filter_presentation false)
+ |> map (filter_presentation presentation_names false)
|> implode
|> suffix "\n"
- else Print_Mode.setmp [] (Pretty.string_of_margin width) p ^ "\n";
(** names and variable name contexts **)
--- a/src/Tools/Code/code_scala.ML Thu Sep 02 13:43:38 2010 +0200
+++ b/src/Tools/Code/code_scala.ML Thu Sep 02 13:58:16 2010 +0200
@@ -370,7 +370,7 @@
| print_node prefix_fragments (name, Code_Namespace.Stmt stmt) =
if null presentation_names
orelse member (op =) presentation_names name
- then SOME (print_stmt (deresolver prefix_fragments, deresolver []) (name, stmt))
+ then SOME (markup_stmt name (print_stmt (deresolver prefix_fragments, deresolver []) (name, stmt)))
else NONE
| print_node prefix_fragments (name_fragment, Code_Namespace.Module (implicits, nodes)) =
if null presentation_names
@@ -392,8 +392,8 @@
(* serialization *)
val p_includes = if null presentation_names then map snd includes else [];
val p = Pretty.chunks2 (p_includes @ the_list (print_nodes [] sca_program));
- fun write width NONE = writeln o format false width
- | write width (SOME p) = File.write p o format false width;
+ fun write width NONE = writeln o format [] width
+ | write width (SOME p) = File.write p o format [] width;
in
Code_Target.serialization write (rpair [] ooo format) p
end;
--- a/src/Tools/Code/code_target.ML Thu Sep 02 13:43:38 2010 +0200
+++ b/src/Tools/Code/code_target.ML Thu Sep 02 13:58:16 2010 +0200
@@ -42,7 +42,7 @@
type serialization
val parse_args: 'a parser -> Token.T list -> 'a
val serialization: (int -> Path.T option -> 'a -> unit)
- -> (bool -> int -> 'a -> string * string option list)
+ -> (string list -> int -> 'a -> string * string option list)
-> 'a -> serialization
val set_default_code_width: int -> theory -> theory
@@ -76,8 +76,8 @@
| stmt_names_of_destination _ = [];
fun serialization output _ content width (Export some_path) = (output width some_path content; NONE)
- | serialization _ string content width Produce = SOME (string false width content)
- | serialization _ string content width (Present _) = SOME (string false width content);
+ | serialization _ string content width Produce = SOME (string [] width content)
+ | serialization _ string content width (Present _) = SOME (string [] width content);
fun export some_path f = (f (Export some_path); ());
fun produce f = the (f Produce);