formal framework for presentation of selected statements
authorhaftmann
Thu, 02 Sep 2010 12:30:22 +0200
changeset 39034 ebeb48fd653b
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
--- a/src/Tools/Code/code_haskell.ML	Thu Sep 02 11:42:50 2010 +0200
+++ b/src/Tools/Code/code_haskell.ML	Thu Sep 02 12:30:22 2010 +0200
@@ -386,13 +386,13 @@
             val _ = File.mkdir_leaf (Path.dir pathname);
           in File.write pathname
             ("{-# OPTIONS_GHC -fglasgow-exts #-}\n\n"
-              ^ string_of_pretty width content)
+              ^ format false width content)
           end
-      | write_module width NONE (_, content) = writeln_pretty width content;
+      | write_module width NONE (_, content) = writeln (format false width content);
   in
     Code_Target.serialization
       (fn width => fn destination => K () o map (write_module width destination))
-      (fn width => rpair [] o cat_lines o map (string_of_pretty width o snd))
+      (fn present => fn width => rpair [] o format present width o Pretty.chunks o map snd)
       (map (uncurry print_module) includes
         @ map serialize_module (Symtab.dest hs_program))
   end;
--- a/src/Tools/Code/code_ml.ML	Thu Sep 02 11:42:50 2010 +0200
+++ b/src/Tools/Code/code_ml.ML	Thu Sep 02 12:30:22 2010 +0200
@@ -815,10 +815,10 @@
       |> (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_pretty width
-      | write width (SOME p) = File.write p o string_of_pretty width;
+    fun write width NONE = writeln o format false width
+      | write width (SOME p) = File.write p o format false width;
   in
-    Code_Target.serialization write (fn width => (rpair names' o string_of_pretty width)) p
+    Code_Target.serialization write (rpair names' ooo format) p
   end;
 
 val serializer_sml : Code_Target.serializer =
--- a/src/Tools/Code/code_printer.ML	Thu Sep 02 11:42:50 2010 +0200
+++ b/src/Tools/Code/code_printer.ML	Thu Sep 02 12:30:22 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 string_of_pretty: int -> Pretty.T -> string
-  val writeln_pretty: int -> Pretty.T -> unit
+  val markup_stmt: string -> Pretty.T list -> Pretty.T
+  val format: bool -> int -> Pretty.T -> string
 
   val first_upper: string -> string
   val first_lower: string -> string
@@ -104,9 +104,16 @@
 
 open Code_Thingol;
 
+(** generic nonsense *)
+
 fun eqn_error (SOME thm) s = error (s ^ ",\nin equation " ^ Display.string_of_thm_without_context thm)
   | eqn_error NONE s = error s;
 
+val code_presentationN = "code_presentation";
+val _ = Output.add_mode code_presentationN;
+val _ = Markup.add_mode code_presentationN YXML.output_markup;
+
+
 (** assembling and printing text pieces **)
 
 infixr 5 @@;
@@ -125,8 +132,21 @@
 fun doublesemicolon ps = Pretty.block [concat ps, str ";;"];
 fun indent i = Print_Mode.setmp [] (Pretty.indent i);
 
-fun string_of_pretty width p = Print_Mode.setmp [] (Pretty.string_of_margin width) p ^ "\n";
-fun writeln_pretty width p = writeln (string_of_pretty width p);
+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) =
+      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
+    |> YXML.parse_body
+    |> map (filter_presentation false)
+    |> implode
+    |> suffix "\n"
+  else Print_Mode.setmp [] (Pretty.string_of_margin width) p ^ "\n";
 
 
 (** names and variable name contexts **)
--- a/src/Tools/Code/code_scala.ML	Thu Sep 02 11:42:50 2010 +0200
+++ b/src/Tools/Code/code_scala.ML	Thu Sep 02 12:30:22 2010 +0200
@@ -392,10 +392,10 @@
     (* 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_pretty width
-      | write width (SOME p) = File.write p o string_of_pretty width;
+    fun write width NONE = writeln o format false width
+      | write width (SOME p) = File.write p o format false width;
   in
-    Code_Target.serialization write (rpair [] oo string_of_pretty) p
+    Code_Target.serialization write (rpair [] ooo format) p
   end;
 
 val serializer : Code_Target.serializer =
--- a/src/Tools/Code/code_target.ML	Thu Sep 02 11:42:50 2010 +0200
+++ b/src/Tools/Code/code_target.ML	Thu Sep 02 12:30:22 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)
-    -> (int -> 'a -> string * string option list)
+    -> (bool -> 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 width content)
-  | serialization _ string content width (Present _) = SOME (string width content);
+  | serialization _ string content width Produce = SOME (string false width content)
+  | serialization _ string content width (Present _) = SOME (string false width content);
 
 fun export some_path f = (f (Export some_path); ());
 fun produce f = the (f Produce);