# HG changeset patch
# User haftmann
# Date 1283431009 -7200
# Node ID c6d146ed07aedb35a45c6c371a2f89e32f698e5a
# Parent  fa197571676baf9721c106c92990678f669f413e
manage statement selection for presentation wholly through markup

diff -r fa197571676b -r c6d146ed07ae src/Tools/Code/code_haskell.ML
--- a/src/Tools/Code/code_haskell.ML	Thu Sep 02 13:58:16 2010 +0200
+++ b/src/Tools/Code/code_haskell.ML	Thu Sep 02 14:36:49 2010 +0200
@@ -365,10 +365,10 @@
         content,
         str "}"
       ]);
-    fun serialize_module1 (module_name', (deps, (stmts, _))) =
+    fun serialize_module (module_name', (deps, (stmts, _))) =
       let
         val stmt_names = map fst stmts;
-        val qualified = null presentation_names;
+        val qualified = true;
         val imports = subtract (op =) stmt_names deps
           |> distinct (op =)
           |> map_filter (try deresolver)
@@ -385,14 +385,6 @@
                 | (_, (_, NONE)) => NONE) stmts
           );
       in print_module module_name' content end;
-    fun serialize_module2 (_, (_, (stmts, _))) = Pretty.chunks2 (map_filter
-        (fn (name, (_, SOME stmt)) => if null presentation_names
-              orelse member (op =) presentation_names name
-              then SOME (print_stmt false (name, stmt))
-              else NONE
-          | (_, (_, NONE)) => NONE) stmts);
-    val serialize_module =
-      if null presentation_names then serialize_module1 else pair "" o serialize_module2;
     fun write_module width (SOME destination) (modlname, content) =
           let
             val _ = File.check destination;
diff -r fa197571676b -r c6d146ed07ae src/Tools/Code/code_ml.ML
--- a/src/Tools/Code/code_ml.ML	Thu Sep 02 13:58:16 2010 +0200
+++ b/src/Tools/Code/code_ml.ML	Thu Sep 02 14:36:49 2010 +0200
@@ -790,7 +790,6 @@
   const_syntax, program, names, presentation_names } =
   let
     val is_cons = Code_Thingol.is_cons program;
-    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
@@ -798,15 +797,11 @@
     fun print_node _ (_, Code_Namespace.Dummy) =
           NONE
       | 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 (apsnd (markup_stmt name) (print_stmt (deresolver prefix_fragments) stmt))
+          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;
-            val p = if is_presentation then Pretty.chunks2 body
-              else print_module name_fragment
+            val p = print_module name_fragment
                 (if with_signatures then SOME decls else NONE) body;
           in SOME ([], p) end
     and print_nodes prefix_fragments nodes = (map_filter
diff -r fa197571676b -r c6d146ed07ae src/Tools/Code/code_printer.ML
--- a/src/Tools/Code/code_printer.ML	Thu Sep 02 13:58:16 2010 +0200
+++ b/src/Tools/Code/code_printer.ML	Thu Sep 02 14:36:49 2010 +0200
@@ -105,7 +105,7 @@
   | eqn_error NONE s = error s;
 
 val code_presentationN = "code_presentation";
-val _ = Output.add_mode code_presentationN;
+val stmt_nameN = "stmt_name";
 val _ = Markup.add_mode code_presentationN YXML.output_markup;
 
 
@@ -127,7 +127,6 @@
 fun doublesemicolon ps = Pretty.block [concat ps, str ";;"];
 fun indent i = Print_Mode.setmp [] (Pretty.indent i);
 
-val stmt_nameN = "stmt_name";
 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
@@ -136,12 +135,22 @@
   | filter_presentation presentation_names selected (XML.Text s) =
       if selected then s else "";
 
+fun maps_string s f [] = ""
+  | maps_string s f (x :: xs) =
+      let
+        val s1 = f x;
+        val s2 = maps_string s f xs;
+      in if s1 = "" then s2
+        else if s2 = "" then s1
+        else s1 ^ s ^ s2
+      end;
+
 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 presentation_names false)
-    |> implode
+    |> tap (fn ts => tracing (cat_lines (map XML.string_of ts)))
+    |> maps_string "\n\n" (filter_presentation presentation_names false)
     |> suffix "\n"
 
 
diff -r fa197571676b -r c6d146ed07ae src/Tools/Code/code_scala.ML
--- a/src/Tools/Code/code_scala.ML	Thu Sep 02 13:58:16 2010 +0200
+++ b/src/Tools/Code/code_scala.ML	Thu Sep 02 14:36:49 2010 +0200
@@ -368,21 +368,15 @@
       in if length (Long_Name.explode s) = 1 then NONE else SOME (str s) end;
     fun print_node _ (_, Code_Namespace.Dummy) = NONE
       | print_node prefix_fragments (name, Code_Namespace.Stmt stmt) =
-          if null presentation_names
-          orelse member (op =) presentation_names name
-          then SOME (markup_stmt name (print_stmt (deresolver prefix_fragments, deresolver []) (name, stmt)))
-          else NONE
+          SOME (markup_stmt name (print_stmt (deresolver prefix_fragments, deresolver []) (name, stmt)))
       | print_node prefix_fragments (name_fragment, Code_Namespace.Module (implicits, nodes)) =
-          if null presentation_names
-          then
-            let
-              val prefix_fragments' = prefix_fragments @ [name_fragment];
-            in
-              Option.map (print_module name_fragment
-                (map_filter (print_implicit prefix_fragments') implicits))
-                  (print_nodes prefix_fragments' nodes)
-            end
-          else print_nodes [] nodes
+          let
+            val prefix_fragments' = prefix_fragments @ [name_fragment];
+          in
+            Option.map (print_module name_fragment
+              (map_filter (print_implicit prefix_fragments') implicits))
+                (print_nodes prefix_fragments' nodes)
+          end
     and print_nodes prefix_fragments nodes = let
         val ps = map_filter (fn name => print_node prefix_fragments (name,
           snd (Graph.get_node nodes name)))
@@ -390,8 +384,7 @@
       in if null ps then NONE else SOME (Pretty.chunks2 ps) end;
 
     (* 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));
+    val p = Pretty.chunks2 (map snd includes @ the_list (print_nodes [] sca_program));
     fun write width NONE = writeln o format [] width
       | write width (SOME p) = File.write p o format [] width;
   in
diff -r fa197571676b -r c6d146ed07ae src/Tools/Code/code_target.ML
--- a/src/Tools/Code/code_target.ML	Thu Sep 02 13:58:16 2010 +0200
+++ b/src/Tools/Code/code_target.ML	Thu Sep 02 14:36:49 2010 +0200
@@ -8,6 +8,7 @@
 sig
   val cert_tyco: theory -> string -> string
   val read_tyco: theory -> string -> string
+  val read_const_exprs: theory -> string list -> string list
 
   val export_code_for: theory -> Path.T option -> string -> int option -> string -> Token.T list
     -> Code_Thingol.naming -> Code_Thingol.program -> string list -> unit
@@ -77,7 +78,7 @@
 
 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 (Present stmt_names) = SOME (string stmt_names width content);
 
 fun export some_path f = (f (Export some_path); ());
 fun produce f = the (f Produce);