src/Tools/Code/code_printer.ML
changeset 55145 2bb3cd36bcf7
parent 52433 ec3a22e62b54
child 55147 bce3dbc11f95
     1.1 --- a/src/Tools/Code/code_printer.ML	Sat Jan 25 22:18:20 2014 +0100
     1.2 +++ b/src/Tools/Code/code_printer.ML	Sat Jan 25 23:50:49 2014 +0100
     1.3 @@ -36,6 +36,8 @@
     1.4    val lookup_var: var_ctxt -> string -> string
     1.5    val intro_base_names: (string -> bool) -> (string -> string)
     1.6      -> string list -> var_ctxt -> var_ctxt
     1.7 +  val intro_base_names_for: (string -> bool) -> (string -> string)
     1.8 +    -> iterm list -> var_ctxt -> var_ctxt
     1.9    val aux_params: var_ctxt -> iterm list list -> string list
    1.10  
    1.11    type literals
    1.12 @@ -187,12 +189,17 @@
    1.13      val vars' = intro_vars fished3 vars;
    1.14    in map (lookup_var vars') fished3 end;
    1.15  
    1.16 -fun intro_base_names no_syntax deresolve names = names
    1.17 -  |> map_filter (fn name => if no_syntax name then
    1.18 +fun intro_base_names no_syntax deresolve =
    1.19 +  map_filter (fn name => if no_syntax name then
    1.20        let val name' = deresolve name in
    1.21          if Long_Name.is_qualified name' then NONE else SOME name'
    1.22        end else NONE)
    1.23 -  |> intro_vars;
    1.24 +  #> intro_vars;
    1.25 +
    1.26 +fun intro_base_names_for no_syntax deresolve ts =
    1.27 +  []
    1.28 +  |> fold Code_Thingol.add_constnames ts 
    1.29 +  |> intro_base_names no_syntax deresolve;
    1.30  
    1.31  
    1.32  (** pretty literals **)