# HG changeset patch
# User haftmann
# Date 1283428696 -7200
# Node ID fa197571676baf9721c106c92990678f669f413e
# Parent  81e0368812adb57492b028038be250188c80bfba
formal markup of generated code for statements

diff -r 81e0368812ad -r fa197571676b src/Tools/Code/code_haskell.ML
--- 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))
diff -r 81e0368812ad -r fa197571676b src/Tools/Code/code_ml.ML
--- 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;
diff -r 81e0368812ad -r fa197571676b src/Tools/Code/code_printer.ML
--- 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 **)
diff -r 81e0368812ad -r fa197571676b src/Tools/Code/code_scala.ML
--- 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;
diff -r 81e0368812ad -r fa197571676b src/Tools/Code/code_target.ML
--- 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);