formal framework for presentation of selected statements
authorhaftmann
Thu Sep 02 12:30:22 2010 +0200 (2010-09-02)
changeset 39034ebeb48fd653b
parent 39033 e8b68ec3bb9c
child 39039 bef9e5dd0fd0
child 39055 81e0368812ad
formal framework for presentation of selected 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 11:42:50 2010 +0200
     1.2 +++ b/src/Tools/Code/code_haskell.ML	Thu Sep 02 12:30:22 2010 +0200
     1.3 @@ -386,13 +386,13 @@
     1.4              val _ = File.mkdir_leaf (Path.dir pathname);
     1.5            in File.write pathname
     1.6              ("{-# OPTIONS_GHC -fglasgow-exts #-}\n\n"
     1.7 -              ^ string_of_pretty width content)
     1.8 +              ^ format false width content)
     1.9            end
    1.10 -      | write_module width NONE (_, content) = writeln_pretty width content;
    1.11 +      | write_module width NONE (_, content) = writeln (format false width content);
    1.12    in
    1.13      Code_Target.serialization
    1.14        (fn width => fn destination => K () o map (write_module width destination))
    1.15 -      (fn width => rpair [] o cat_lines o map (string_of_pretty width o snd))
    1.16 +      (fn present => fn width => rpair [] o format present width o Pretty.chunks o map snd)
    1.17        (map (uncurry print_module) includes
    1.18          @ map serialize_module (Symtab.dest hs_program))
    1.19    end;
     2.1 --- a/src/Tools/Code/code_ml.ML	Thu Sep 02 11:42:50 2010 +0200
     2.2 +++ b/src/Tools/Code/code_ml.ML	Thu Sep 02 12:30:22 2010 +0200
     2.3 @@ -815,10 +815,10 @@
     2.4        |> (fn (decls, body) => (flat decls, body))
     2.5      val names' = map (try (deresolver [])) names;
     2.6      val p = Pretty.chunks2 (map snd includes @ snd (print_nodes [] ml_program));
     2.7 -    fun write width NONE = writeln_pretty width
     2.8 -      | write width (SOME p) = File.write p o string_of_pretty width;
     2.9 +    fun write width NONE = writeln o format false width
    2.10 +      | write width (SOME p) = File.write p o format false width;
    2.11    in
    2.12 -    Code_Target.serialization write (fn width => (rpair names' o string_of_pretty width)) p
    2.13 +    Code_Target.serialization write (rpair names' ooo format) p
    2.14    end;
    2.15  
    2.16  val serializer_sml : Code_Target.serializer =
     3.1 --- a/src/Tools/Code/code_printer.ML	Thu Sep 02 11:42:50 2010 +0200
     3.2 +++ b/src/Tools/Code/code_printer.ML	Thu Sep 02 12:30:22 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 string_of_pretty: int -> Pretty.T -> string
     3.8 -  val writeln_pretty: int -> Pretty.T -> unit
     3.9 +  val markup_stmt: string -> Pretty.T list -> Pretty.T
    3.10 +  val format: bool -> int -> Pretty.T -> string
    3.11  
    3.12    val first_upper: string -> string
    3.13    val first_lower: string -> string
    3.14 @@ -104,9 +104,16 @@
    3.15  
    3.16  open Code_Thingol;
    3.17  
    3.18 +(** generic nonsense *)
    3.19 +
    3.20  fun eqn_error (SOME thm) s = error (s ^ ",\nin equation " ^ Display.string_of_thm_without_context thm)
    3.21    | eqn_error NONE s = error s;
    3.22  
    3.23 +val code_presentationN = "code_presentation";
    3.24 +val _ = Output.add_mode code_presentationN;
    3.25 +val _ = Markup.add_mode code_presentationN YXML.output_markup;
    3.26 +
    3.27 +
    3.28  (** assembling and printing text pieces **)
    3.29  
    3.30  infixr 5 @@;
    3.31 @@ -125,8 +132,21 @@
    3.32  fun doublesemicolon ps = Pretty.block [concat ps, str ";;"];
    3.33  fun indent i = Print_Mode.setmp [] (Pretty.indent i);
    3.34  
    3.35 -fun string_of_pretty width p = Print_Mode.setmp [] (Pretty.string_of_margin width) p ^ "\n";
    3.36 -fun writeln_pretty width p = writeln (string_of_pretty width p);
    3.37 +val stmt_nameN = "stmt_name";
    3.38 +fun markup_stmt name = Pretty.markup (code_presentationN, [(stmt_nameN, name)]);
    3.39 +fun filter_presentation selected (XML.Elem ((name, _), xs)) =
    3.40 +      implode (map (filter_presentation (selected orelse name = code_presentationN)) xs)
    3.41 +  | filter_presentation selected (XML.Text s) =
    3.42 +      if selected then s else "";
    3.43 +
    3.44 +fun format presentation_only width p =
    3.45 +  if presentation_only then
    3.46 +    Print_Mode.setmp [code_presentationN] (Pretty.string_of_margin width) p
    3.47 +    |> YXML.parse_body
    3.48 +    |> map (filter_presentation false)
    3.49 +    |> implode
    3.50 +    |> suffix "\n"
    3.51 +  else Print_Mode.setmp [] (Pretty.string_of_margin width) p ^ "\n";
    3.52  
    3.53  
    3.54  (** names and variable name contexts **)
     4.1 --- a/src/Tools/Code/code_scala.ML	Thu Sep 02 11:42:50 2010 +0200
     4.2 +++ b/src/Tools/Code/code_scala.ML	Thu Sep 02 12:30:22 2010 +0200
     4.3 @@ -392,10 +392,10 @@
     4.4      (* serialization *)
     4.5      val p_includes = if null presentation_names then map snd includes else [];
     4.6      val p = Pretty.chunks2 (p_includes @ the_list (print_nodes [] sca_program));
     4.7 -    fun write width NONE = writeln_pretty width
     4.8 -      | write width (SOME p) = File.write p o string_of_pretty width;
     4.9 +    fun write width NONE = writeln o format false width
    4.10 +      | write width (SOME p) = File.write p o format false width;
    4.11    in
    4.12 -    Code_Target.serialization write (rpair [] oo string_of_pretty) p
    4.13 +    Code_Target.serialization write (rpair [] ooo format) p
    4.14    end;
    4.15  
    4.16  val serializer : Code_Target.serializer =
     5.1 --- a/src/Tools/Code/code_target.ML	Thu Sep 02 11:42:50 2010 +0200
     5.2 +++ b/src/Tools/Code/code_target.ML	Thu Sep 02 12:30:22 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 -    -> (int -> 'a -> string * string option list)
     5.8 +    -> (bool -> 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 width content)
    5.17 -  | serialization _ string content width (Present _) = SOME (string width content);
    5.18 +  | serialization _ string content width Produce = SOME (string false width content)
    5.19 +  | serialization _ string content width (Present _) = SOME (string false width content);
    5.20  
    5.21  fun export some_path f = (f (Export some_path); ());
    5.22  fun produce f = the (f Produce);