formal markup of generated code for statements
authorhaftmann
Thu Sep 02 13:58:16 2010 +0200 (2010-09-02)
changeset 39056fa197571676b
parent 39055 81e0368812ad
child 39057 c6d146ed07ae
formal markup of generated code for statements
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:43:38 2010 +0200
     1.2 +++ b/src/Tools/Code/code_haskell.ML	Thu Sep 02 13:58:16 2010 +0200
     1.3 @@ -381,7 +381,7 @@
     1.4          val import_ps = map print_import_include includes @ map print_import_module imports
     1.5          val content = Pretty.chunks2 ((if null import_ps then [] else [Pretty.chunks import_ps])
     1.6              @ map_filter
     1.7 -              (fn (name, (_, SOME stmt)) => SOME (print_stmt qualified (name, stmt))
     1.8 +              (fn (name, (_, SOME stmt)) => SOME (markup_stmt name (print_stmt qualified (name, stmt)))
     1.9                  | (_, (_, NONE)) => NONE) stmts
    1.10            );
    1.11        in print_module module_name' content end;
    1.12 @@ -404,9 +404,9 @@
    1.13              val _ = File.mkdir_leaf (Path.dir pathname);
    1.14            in File.write pathname
    1.15              ("{-# OPTIONS_GHC -fglasgow-exts #-}\n\n"
    1.16 -              ^ format false width content)
    1.17 +              ^ format [] width content)
    1.18            end
    1.19 -      | write_module width NONE (_, content) = writeln (format false width content);
    1.20 +      | write_module width NONE (_, content) = writeln (format [] width content);
    1.21    in
    1.22      Code_Target.serialization
    1.23        (fn width => fn destination => K () o map (write_module width destination))
     2.1 --- a/src/Tools/Code/code_ml.ML	Thu Sep 02 13:43:38 2010 +0200
     2.2 +++ b/src/Tools/Code/code_ml.ML	Thu Sep 02 13:58:16 2010 +0200
     2.3 @@ -793,14 +793,15 @@
     2.4      val is_presentation = not (null presentation_names);
     2.5      val { deresolver, hierarchical_program = ml_program } =
     2.6        ml_program_of_program labelled_name (Name.make_context reserved_syms) module_alias program;
     2.7 +    val print_stmt = print_stmt labelled_name tyco_syntax const_syntax
     2.8 +      (make_vars reserved_syms) is_cons;
     2.9      fun print_node _ (_, Code_Namespace.Dummy) =
    2.10            NONE
    2.11 -      | print_node prefix_fragments (_, Code_Namespace.Stmt stmt) =
    2.12 +      | print_node prefix_fragments (name, Code_Namespace.Stmt stmt) =
    2.13            if is_presentation andalso
    2.14              (null o filter (member (op =) presentation_names) o stmt_names_of) stmt
    2.15            then NONE
    2.16 -          else SOME (print_stmt labelled_name tyco_syntax const_syntax (make_vars reserved_syms)
    2.17 -            is_cons (deresolver prefix_fragments) stmt)
    2.18 +          else SOME (apsnd (markup_stmt name) (print_stmt (deresolver prefix_fragments) stmt))
    2.19        | print_node prefix_fragments (name_fragment, Code_Namespace.Module (_, nodes)) =
    2.20            let
    2.21              val (decls, body) = print_nodes (prefix_fragments @ [name_fragment]) nodes;
    2.22 @@ -815,8 +816,8 @@
    2.23        |> (fn (decls, body) => (flat decls, body))
    2.24      val names' = map (try (deresolver [])) names;
    2.25      val p = Pretty.chunks2 (map snd includes @ snd (print_nodes [] ml_program));
    2.26 -    fun write width NONE = writeln o format false width
    2.27 -      | write width (SOME p) = File.write p o format false width;
    2.28 +    fun write width NONE = writeln o format [] width
    2.29 +      | write width (SOME p) = File.write p o format [] width;
    2.30    in
    2.31      Code_Target.serialization write (rpair names' ooo format) p
    2.32    end;
     3.1 --- a/src/Tools/Code/code_printer.ML	Thu Sep 02 13:43:38 2010 +0200
     3.2 +++ b/src/Tools/Code/code_printer.ML	Thu Sep 02 13:58:16 2010 +0200
     3.3 @@ -25,8 +25,8 @@
     3.4    val semicolon: Pretty.T list -> Pretty.T
     3.5    val doublesemicolon: Pretty.T list -> Pretty.T
     3.6    val indent: int -> Pretty.T -> Pretty.T
     3.7 -  val markup_stmt: string -> Pretty.T list -> Pretty.T
     3.8 -  val format: bool -> int -> Pretty.T -> string
     3.9 +  val markup_stmt: string -> Pretty.T -> Pretty.T
    3.10 +  val format: string list -> int -> Pretty.T -> string
    3.11  
    3.12    val first_upper: string -> string
    3.13    val first_lower: string -> string
    3.14 @@ -128,20 +128,21 @@
    3.15  fun indent i = Print_Mode.setmp [] (Pretty.indent i);
    3.16  
    3.17  val stmt_nameN = "stmt_name";
    3.18 -fun markup_stmt name = Pretty.markup (code_presentationN, [(stmt_nameN, name)]);
    3.19 -fun filter_presentation selected (XML.Elem ((name, _), xs)) =
    3.20 -      implode (map (filter_presentation (selected orelse name = code_presentationN)) xs)
    3.21 -  | filter_presentation selected (XML.Text s) =
    3.22 +fun markup_stmt name = Pretty.mark (code_presentationN, [(stmt_nameN, name)]);
    3.23 +fun filter_presentation presentation_names selected (XML.Elem ((name, attrs), xs)) =
    3.24 +      implode (map (filter_presentation presentation_names
    3.25 +        (selected orelse (name = code_presentationN
    3.26 +          andalso member (op =) presentation_names (the (Properties.get attrs stmt_nameN))))) xs)
    3.27 +  | filter_presentation presentation_names selected (XML.Text s) =
    3.28        if selected then s else "";
    3.29  
    3.30 -fun format presentation_only width p =
    3.31 -  if presentation_only then
    3.32 -    Print_Mode.setmp [code_presentationN] (Pretty.string_of_margin width) p
    3.33 +fun format presentation_names width p =
    3.34 +  if null presentation_names then Print_Mode.setmp [] (Pretty.string_of_margin width) p ^ "\n"
    3.35 +  else Print_Mode.setmp [code_presentationN] (Pretty.string_of_margin width) p
    3.36      |> YXML.parse_body
    3.37 -    |> map (filter_presentation false)
    3.38 +    |> map (filter_presentation presentation_names false)
    3.39      |> implode
    3.40      |> suffix "\n"
    3.41 -  else Print_Mode.setmp [] (Pretty.string_of_margin width) p ^ "\n";
    3.42  
    3.43  
    3.44  (** names and variable name contexts **)
     4.1 --- a/src/Tools/Code/code_scala.ML	Thu Sep 02 13:43:38 2010 +0200
     4.2 +++ b/src/Tools/Code/code_scala.ML	Thu Sep 02 13:58:16 2010 +0200
     4.3 @@ -370,7 +370,7 @@
     4.4        | print_node prefix_fragments (name, Code_Namespace.Stmt stmt) =
     4.5            if null presentation_names
     4.6            orelse member (op =) presentation_names name
     4.7 -          then SOME (print_stmt (deresolver prefix_fragments, deresolver []) (name, stmt))
     4.8 +          then SOME (markup_stmt name (print_stmt (deresolver prefix_fragments, deresolver []) (name, stmt)))
     4.9            else NONE
    4.10        | print_node prefix_fragments (name_fragment, Code_Namespace.Module (implicits, nodes)) =
    4.11            if null presentation_names
    4.12 @@ -392,8 +392,8 @@
    4.13      (* serialization *)
    4.14      val p_includes = if null presentation_names then map snd includes else [];
    4.15      val p = Pretty.chunks2 (p_includes @ the_list (print_nodes [] sca_program));
    4.16 -    fun write width NONE = writeln o format false width
    4.17 -      | write width (SOME p) = File.write p o format false width;
    4.18 +    fun write width NONE = writeln o format [] width
    4.19 +      | write width (SOME p) = File.write p o format [] width;
    4.20    in
    4.21      Code_Target.serialization write (rpair [] ooo format) p
    4.22    end;
     5.1 --- a/src/Tools/Code/code_target.ML	Thu Sep 02 13:43:38 2010 +0200
     5.2 +++ b/src/Tools/Code/code_target.ML	Thu Sep 02 13:58:16 2010 +0200
     5.3 @@ -42,7 +42,7 @@
     5.4    type serialization
     5.5    val parse_args: 'a parser -> Token.T list -> 'a
     5.6    val serialization: (int -> Path.T option -> 'a -> unit)
     5.7 -    -> (bool -> int -> 'a -> string * string option list)
     5.8 +    -> (string list -> int -> 'a -> string * string option list)
     5.9      -> 'a -> serialization
    5.10    val set_default_code_width: int -> theory -> theory
    5.11  
    5.12 @@ -76,8 +76,8 @@
    5.13    | stmt_names_of_destination _ = [];
    5.14  
    5.15  fun serialization output _ content width (Export some_path) = (output width some_path content; NONE)
    5.16 -  | serialization _ string content width Produce = SOME (string false width content)
    5.17 -  | serialization _ string content width (Present _) = SOME (string false width content);
    5.18 +  | serialization _ string content width Produce = SOME (string [] width content)
    5.19 +  | serialization _ string content width (Present _) = SOME (string [] width content);
    5.20  
    5.21  fun export some_path f = (f (Export some_path); ());
    5.22  fun produce f = the (f Produce);