# HG changeset patch # User haftmann # Date 1283423422 -7200 # Node ID ebeb48fd653b54e2a751359972fe3935eb6265f1 # Parent e8b68ec3bb9ccb7a17a6be7895dbbaa887ccc0c4 formal framework for presentation of selected statements diff -r e8b68ec3bb9c -r ebeb48fd653b src/Tools/Code/code_haskell.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; diff -r e8b68ec3bb9c -r ebeb48fd653b src/Tools/Code/code_ml.ML --- 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 = diff -r e8b68ec3bb9c -r ebeb48fd653b src/Tools/Code/code_printer.ML --- 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 **) diff -r e8b68ec3bb9c -r ebeb48fd653b src/Tools/Code/code_scala.ML --- 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 = diff -r e8b68ec3bb9c -r ebeb48fd653b src/Tools/Code/code_target.ML --- 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);