manage statement selection for presentation wholly through markup
authorhaftmann
Thu Sep 02 14:36:49 2010 +0200 (2010-09-02)
changeset 39057c6d146ed07ae
parent 39056 fa197571676b
child 39058 551fe1af03b0
manage statement selection for presentation wholly through markup
src/Tools/Code/code_haskell.ML
src/Tools/Code/code_ml.ML
src/Tools/Code/code_printer.ML
src/Tools/Code/code_scala.ML
src/Tools/Code/code_target.ML
     1.1 --- a/src/Tools/Code/code_haskell.ML	Thu Sep 02 13:58:16 2010 +0200
     1.2 +++ b/src/Tools/Code/code_haskell.ML	Thu Sep 02 14:36:49 2010 +0200
     1.3 @@ -365,10 +365,10 @@
     1.4          content,
     1.5          str "}"
     1.6        ]);
     1.7 -    fun serialize_module1 (module_name', (deps, (stmts, _))) =
     1.8 +    fun serialize_module (module_name', (deps, (stmts, _))) =
     1.9        let
    1.10          val stmt_names = map fst stmts;
    1.11 -        val qualified = null presentation_names;
    1.12 +        val qualified = true;
    1.13          val imports = subtract (op =) stmt_names deps
    1.14            |> distinct (op =)
    1.15            |> map_filter (try deresolver)
    1.16 @@ -385,14 +385,6 @@
    1.17                  | (_, (_, NONE)) => NONE) stmts
    1.18            );
    1.19        in print_module module_name' content end;
    1.20 -    fun serialize_module2 (_, (_, (stmts, _))) = Pretty.chunks2 (map_filter
    1.21 -        (fn (name, (_, SOME stmt)) => if null presentation_names
    1.22 -              orelse member (op =) presentation_names name
    1.23 -              then SOME (print_stmt false (name, stmt))
    1.24 -              else NONE
    1.25 -          | (_, (_, NONE)) => NONE) stmts);
    1.26 -    val serialize_module =
    1.27 -      if null presentation_names then serialize_module1 else pair "" o serialize_module2;
    1.28      fun write_module width (SOME destination) (modlname, content) =
    1.29            let
    1.30              val _ = File.check destination;
     2.1 --- a/src/Tools/Code/code_ml.ML	Thu Sep 02 13:58:16 2010 +0200
     2.2 +++ b/src/Tools/Code/code_ml.ML	Thu Sep 02 14:36:49 2010 +0200
     2.3 @@ -790,7 +790,6 @@
     2.4    const_syntax, program, names, presentation_names } =
     2.5    let
     2.6      val is_cons = Code_Thingol.is_cons program;
     2.7 -    val is_presentation = not (null presentation_names);
     2.8      val { deresolver, hierarchical_program = ml_program } =
     2.9        ml_program_of_program labelled_name (Name.make_context reserved_syms) module_alias program;
    2.10      val print_stmt = print_stmt labelled_name tyco_syntax const_syntax
    2.11 @@ -798,15 +797,11 @@
    2.12      fun print_node _ (_, Code_Namespace.Dummy) =
    2.13            NONE
    2.14        | print_node prefix_fragments (name, Code_Namespace.Stmt stmt) =
    2.15 -          if is_presentation andalso
    2.16 -            (null o filter (member (op =) presentation_names) o stmt_names_of) stmt
    2.17 -          then NONE
    2.18 -          else SOME (apsnd (markup_stmt name) (print_stmt (deresolver prefix_fragments) stmt))
    2.19 +          SOME (apsnd (markup_stmt name) (print_stmt (deresolver prefix_fragments) stmt))
    2.20        | print_node prefix_fragments (name_fragment, Code_Namespace.Module (_, nodes)) =
    2.21            let
    2.22              val (decls, body) = print_nodes (prefix_fragments @ [name_fragment]) nodes;
    2.23 -            val p = if is_presentation then Pretty.chunks2 body
    2.24 -              else print_module name_fragment
    2.25 +            val p = print_module name_fragment
    2.26                  (if with_signatures then SOME decls else NONE) body;
    2.27            in SOME ([], p) end
    2.28      and print_nodes prefix_fragments nodes = (map_filter
     3.1 --- a/src/Tools/Code/code_printer.ML	Thu Sep 02 13:58:16 2010 +0200
     3.2 +++ b/src/Tools/Code/code_printer.ML	Thu Sep 02 14:36:49 2010 +0200
     3.3 @@ -105,7 +105,7 @@
     3.4    | eqn_error NONE s = error s;
     3.5  
     3.6  val code_presentationN = "code_presentation";
     3.7 -val _ = Output.add_mode code_presentationN;
     3.8 +val stmt_nameN = "stmt_name";
     3.9  val _ = Markup.add_mode code_presentationN YXML.output_markup;
    3.10  
    3.11  
    3.12 @@ -127,7 +127,6 @@
    3.13  fun doublesemicolon ps = Pretty.block [concat ps, str ";;"];
    3.14  fun indent i = Print_Mode.setmp [] (Pretty.indent i);
    3.15  
    3.16 -val stmt_nameN = "stmt_name";
    3.17  fun markup_stmt name = Pretty.mark (code_presentationN, [(stmt_nameN, name)]);
    3.18  fun filter_presentation presentation_names selected (XML.Elem ((name, attrs), xs)) =
    3.19        implode (map (filter_presentation presentation_names
    3.20 @@ -136,12 +135,22 @@
    3.21    | filter_presentation presentation_names selected (XML.Text s) =
    3.22        if selected then s else "";
    3.23  
    3.24 +fun maps_string s f [] = ""
    3.25 +  | maps_string s f (x :: xs) =
    3.26 +      let
    3.27 +        val s1 = f x;
    3.28 +        val s2 = maps_string s f xs;
    3.29 +      in if s1 = "" then s2
    3.30 +        else if s2 = "" then s1
    3.31 +        else s1 ^ s ^ s2
    3.32 +      end;
    3.33 +
    3.34  fun format presentation_names width p =
    3.35    if null presentation_names then Print_Mode.setmp [] (Pretty.string_of_margin width) p ^ "\n"
    3.36    else Print_Mode.setmp [code_presentationN] (Pretty.string_of_margin width) p
    3.37      |> YXML.parse_body
    3.38 -    |> map (filter_presentation presentation_names false)
    3.39 -    |> implode
    3.40 +    |> tap (fn ts => tracing (cat_lines (map XML.string_of ts)))
    3.41 +    |> maps_string "\n\n" (filter_presentation presentation_names false)
    3.42      |> suffix "\n"
    3.43  
    3.44  
     4.1 --- a/src/Tools/Code/code_scala.ML	Thu Sep 02 13:58:16 2010 +0200
     4.2 +++ b/src/Tools/Code/code_scala.ML	Thu Sep 02 14:36:49 2010 +0200
     4.3 @@ -368,21 +368,15 @@
     4.4        in if length (Long_Name.explode s) = 1 then NONE else SOME (str s) end;
     4.5      fun print_node _ (_, Code_Namespace.Dummy) = NONE
     4.6        | print_node prefix_fragments (name, Code_Namespace.Stmt stmt) =
     4.7 -          if null presentation_names
     4.8 -          orelse member (op =) presentation_names name
     4.9 -          then SOME (markup_stmt name (print_stmt (deresolver prefix_fragments, deresolver []) (name, stmt)))
    4.10 -          else NONE
    4.11 +          SOME (markup_stmt name (print_stmt (deresolver prefix_fragments, deresolver []) (name, stmt)))
    4.12        | print_node prefix_fragments (name_fragment, Code_Namespace.Module (implicits, nodes)) =
    4.13 -          if null presentation_names
    4.14 -          then
    4.15 -            let
    4.16 -              val prefix_fragments' = prefix_fragments @ [name_fragment];
    4.17 -            in
    4.18 -              Option.map (print_module name_fragment
    4.19 -                (map_filter (print_implicit prefix_fragments') implicits))
    4.20 -                  (print_nodes prefix_fragments' nodes)
    4.21 -            end
    4.22 -          else print_nodes [] nodes
    4.23 +          let
    4.24 +            val prefix_fragments' = prefix_fragments @ [name_fragment];
    4.25 +          in
    4.26 +            Option.map (print_module name_fragment
    4.27 +              (map_filter (print_implicit prefix_fragments') implicits))
    4.28 +                (print_nodes prefix_fragments' nodes)
    4.29 +          end
    4.30      and print_nodes prefix_fragments nodes = let
    4.31          val ps = map_filter (fn name => print_node prefix_fragments (name,
    4.32            snd (Graph.get_node nodes name)))
    4.33 @@ -390,8 +384,7 @@
    4.34        in if null ps then NONE else SOME (Pretty.chunks2 ps) end;
    4.35  
    4.36      (* serialization *)
    4.37 -    val p_includes = if null presentation_names then map snd includes else [];
    4.38 -    val p = Pretty.chunks2 (p_includes @ the_list (print_nodes [] sca_program));
    4.39 +    val p = Pretty.chunks2 (map snd includes @ the_list (print_nodes [] sca_program));
    4.40      fun write width NONE = writeln o format [] width
    4.41        | write width (SOME p) = File.write p o format [] width;
    4.42    in
     5.1 --- a/src/Tools/Code/code_target.ML	Thu Sep 02 13:58:16 2010 +0200
     5.2 +++ b/src/Tools/Code/code_target.ML	Thu Sep 02 14:36:49 2010 +0200
     5.3 @@ -8,6 +8,7 @@
     5.4  sig
     5.5    val cert_tyco: theory -> string -> string
     5.6    val read_tyco: theory -> string -> string
     5.7 +  val read_const_exprs: theory -> string list -> string list
     5.8  
     5.9    val export_code_for: theory -> Path.T option -> string -> int option -> string -> Token.T list
    5.10      -> Code_Thingol.naming -> Code_Thingol.program -> string list -> unit
    5.11 @@ -77,7 +78,7 @@
    5.12  
    5.13  fun serialization output _ content width (Export some_path) = (output width some_path content; NONE)
    5.14    | serialization _ string content width Produce = SOME (string [] width content)
    5.15 -  | serialization _ string content width (Present _) = SOME (string [] width content);
    5.16 +  | serialization _ string content width (Present stmt_names) = SOME (string stmt_names width content);
    5.17  
    5.18  fun export some_path f = (f (Export some_path); ());
    5.19  fun produce f = the (f Produce);