src/Tools/Code/code_printer.ML
changeset 39056 fa197571676b
parent 39055 81e0368812ad
child 39057 c6d146ed07ae
equal deleted inserted replaced
39055:81e0368812ad 39056:fa197571676b
    23   val enum: string -> string -> string -> Pretty.T list -> Pretty.T
    23   val enum: string -> string -> string -> Pretty.T list -> Pretty.T
    24   val enum_default: string -> string -> string -> string -> Pretty.T list -> Pretty.T
    24   val enum_default: string -> string -> string -> string -> Pretty.T list -> Pretty.T
    25   val semicolon: Pretty.T list -> Pretty.T
    25   val semicolon: Pretty.T list -> Pretty.T
    26   val doublesemicolon: Pretty.T list -> Pretty.T
    26   val doublesemicolon: Pretty.T list -> Pretty.T
    27   val indent: int -> Pretty.T -> Pretty.T
    27   val indent: int -> Pretty.T -> Pretty.T
    28   val markup_stmt: string -> Pretty.T list -> Pretty.T
    28   val markup_stmt: string -> Pretty.T -> Pretty.T
    29   val format: bool -> int -> Pretty.T -> string
    29   val format: string list -> int -> Pretty.T -> string
    30 
    30 
    31   val first_upper: string -> string
    31   val first_upper: string -> string
    32   val first_lower: string -> string
    32   val first_lower: string -> string
    33   type var_ctxt
    33   type var_ctxt
    34   val make_vars: string list -> var_ctxt
    34   val make_vars: string list -> var_ctxt
   126 fun semicolon ps = Pretty.block [concat ps, str ";"];
   126 fun semicolon ps = Pretty.block [concat ps, str ";"];
   127 fun doublesemicolon ps = Pretty.block [concat ps, str ";;"];
   127 fun doublesemicolon ps = Pretty.block [concat ps, str ";;"];
   128 fun indent i = Print_Mode.setmp [] (Pretty.indent i);
   128 fun indent i = Print_Mode.setmp [] (Pretty.indent i);
   129 
   129 
   130 val stmt_nameN = "stmt_name";
   130 val stmt_nameN = "stmt_name";
   131 fun markup_stmt name = Pretty.markup (code_presentationN, [(stmt_nameN, name)]);
   131 fun markup_stmt name = Pretty.mark (code_presentationN, [(stmt_nameN, name)]);
   132 fun filter_presentation selected (XML.Elem ((name, _), xs)) =
   132 fun filter_presentation presentation_names selected (XML.Elem ((name, attrs), xs)) =
   133       implode (map (filter_presentation (selected orelse name = code_presentationN)) xs)
   133       implode (map (filter_presentation presentation_names
   134   | filter_presentation selected (XML.Text s) =
   134         (selected orelse (name = code_presentationN
       
   135           andalso member (op =) presentation_names (the (Properties.get attrs stmt_nameN))))) xs)
       
   136   | filter_presentation presentation_names selected (XML.Text s) =
   135       if selected then s else "";
   137       if selected then s else "";
   136 
   138 
   137 fun format presentation_only width p =
   139 fun format presentation_names width p =
   138   if presentation_only then
   140   if null presentation_names then Print_Mode.setmp [] (Pretty.string_of_margin width) p ^ "\n"
   139     Print_Mode.setmp [code_presentationN] (Pretty.string_of_margin width) p
   141   else Print_Mode.setmp [code_presentationN] (Pretty.string_of_margin width) p
   140     |> YXML.parse_body
   142     |> YXML.parse_body
   141     |> map (filter_presentation false)
   143     |> map (filter_presentation presentation_names false)
   142     |> implode
   144     |> implode
   143     |> suffix "\n"
   145     |> suffix "\n"
   144   else Print_Mode.setmp [] (Pretty.string_of_margin width) p ^ "\n";
       
   145 
   146 
   146 
   147 
   147 (** names and variable name contexts **)
   148 (** names and variable name contexts **)
   148 
   149 
   149 type var_ctxt = string Symtab.table * Name.context;
   150 type var_ctxt = string Symtab.table * Name.context;