--- a/src/Tools/Code/code_haskell.ML Thu Sep 02 11:42:50 2010 +0200
+++ b/src/Tools/Code/code_haskell.ML Thu Sep 02 12:30:22 2010 +0200
@@ -386,13 +386,13 @@
val _ = File.mkdir_leaf (Path.dir pathname);
in File.write pathname
("{-# OPTIONS_GHC -fglasgow-exts #-}\n\n"
- ^ string_of_pretty width content)
+ ^ format false width content)
end
- | write_module width NONE (_, content) = writeln_pretty width content;
+ | write_module width NONE (_, content) = writeln (format false width content);
in
Code_Target.serialization
(fn width => fn destination => K () o map (write_module width destination))
- (fn width => rpair [] o cat_lines o map (string_of_pretty width o snd))
+ (fn present => fn width => rpair [] o format present width o Pretty.chunks o map snd)
(map (uncurry print_module) includes
@ map serialize_module (Symtab.dest hs_program))
end;
--- a/src/Tools/Code/code_ml.ML Thu Sep 02 11:42:50 2010 +0200
+++ b/src/Tools/Code/code_ml.ML Thu Sep 02 12:30:22 2010 +0200
@@ -815,10 +815,10 @@
|> (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_pretty width
- | write width (SOME p) = File.write p o string_of_pretty width;
+ fun write width NONE = writeln o format false width
+ | write width (SOME p) = File.write p o format false width;
in
- Code_Target.serialization write (fn width => (rpair names' o string_of_pretty width)) p
+ Code_Target.serialization write (rpair names' ooo format) p
end;
val serializer_sml : Code_Target.serializer =
--- a/src/Tools/Code/code_printer.ML Thu Sep 02 11:42:50 2010 +0200
+++ b/src/Tools/Code/code_printer.ML Thu Sep 02 12:30:22 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 string_of_pretty: int -> Pretty.T -> string
- val writeln_pretty: int -> Pretty.T -> unit
+ val markup_stmt: string -> Pretty.T list -> Pretty.T
+ val format: bool -> int -> Pretty.T -> string
val first_upper: string -> string
val first_lower: string -> string
@@ -104,9 +104,16 @@
open Code_Thingol;
+(** generic nonsense *)
+
fun eqn_error (SOME thm) s = error (s ^ ",\nin equation " ^ Display.string_of_thm_without_context thm)
| eqn_error NONE s = error s;
+val code_presentationN = "code_presentation";
+val _ = Output.add_mode code_presentationN;
+val _ = Markup.add_mode code_presentationN YXML.output_markup;
+
+
(** assembling and printing text pieces **)
infixr 5 @@;
@@ -125,8 +132,21 @@
fun doublesemicolon ps = Pretty.block [concat ps, str ";;"];
fun indent i = Print_Mode.setmp [] (Pretty.indent i);
-fun string_of_pretty width p = Print_Mode.setmp [] (Pretty.string_of_margin width) p ^ "\n";
-fun writeln_pretty width p = writeln (string_of_pretty width p);
+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) =
+ 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
+ |> YXML.parse_body
+ |> map (filter_presentation 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 11:42:50 2010 +0200
+++ b/src/Tools/Code/code_scala.ML Thu Sep 02 12:30:22 2010 +0200
@@ -392,10 +392,10 @@
(* 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_pretty width
- | write width (SOME p) = File.write p o string_of_pretty width;
+ fun write width NONE = writeln o format false width
+ | write width (SOME p) = File.write p o format false width;
in
- Code_Target.serialization write (rpair [] oo string_of_pretty) p
+ Code_Target.serialization write (rpair [] ooo format) p
end;
val serializer : Code_Target.serializer =
--- a/src/Tools/Code/code_target.ML Thu Sep 02 11:42:50 2010 +0200
+++ b/src/Tools/Code/code_target.ML Thu Sep 02 12:30:22 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)
- -> (int -> 'a -> string * string option list)
+ -> (bool -> 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 width content)
- | serialization _ string content width (Present _) = SOME (string width content);
+ | serialization _ string content width Produce = SOME (string false width content)
+ | serialization _ string content width (Present _) = SOME (string false width content);
fun export some_path f = (f (Export some_path); ());
fun produce f = the (f Produce);