# HG changeset patch
# User haftmann
# Date 1390690249 -3600
# Node ID 2bb3cd36bcf7ade02d9313f61716db7ff632b0b1
# Parent  de95c97efab348673e0ee28d09cab10cef2e0fb5
more abstract declaration of unqualified constant names in code printing context

diff -r de95c97efab3 -r 2bb3cd36bcf7 src/Tools/Code/code_haskell.ML
--- a/src/Tools/Code/code_haskell.ML	Sat Jan 25 22:18:20 2014 +0100
+++ b/src/Tools/Code/code_haskell.ML	Sat Jan 25 23:50:49 2014 +0100
@@ -136,10 +136,9 @@
               );
             fun print_eqn ((ts, t), (some_thm, _)) =
               let
-                val consts = fold Code_Thingol.add_constnames (t :: ts) [];
                 val vars = reserved
-                  |> intro_base_names
-                      (is_none o const_syntax) deresolve consts
+                  |> intro_base_names_for (is_none o const_syntax)
+                      deresolve (t :: ts)
                   |> intro_vars ((fold o Code_Thingol.fold_varnames)
                       (insert (op =)) ts []);
               in
diff -r de95c97efab3 -r 2bb3cd36bcf7 src/Tools/Code/code_ml.ML
--- a/src/Tools/Code/code_ml.ML	Sat Jan 25 22:18:20 2014 +0100
+++ b/src/Tools/Code/code_ml.ML	Sat Jan 25 23:50:49 2014 +0100
@@ -178,10 +178,9 @@
           let
             fun print_eqn definer ((ts, t), (some_thm, _)) =
               let
-                val consts = fold Code_Thingol.add_constnames (t :: ts) [];
                 val vars = reserved
-                  |> intro_base_names
-                       (is_none o const_syntax) deresolve consts
+                  |> intro_base_names_for (is_none o const_syntax)
+                       deresolve (t :: ts)
                   |> intro_vars ((fold o Code_Thingol.fold_varnames)
                        (insert (op =)) ts []);
                 val prolog = if needs_typ then
@@ -470,10 +469,9 @@
           let
             fun print_eqn ((ts, t), (some_thm, _)) =
               let
-                val consts = fold Code_Thingol.add_constnames (t :: ts) [];
                 val vars = reserved
-                  |> intro_base_names
-                      (is_none o const_syntax) deresolve consts
+                  |> intro_base_names_for (is_none o const_syntax)
+                      deresolve (t :: ts)
                   |> intro_vars ((fold o Code_Thingol.fold_varnames)
                       (insert (op =)) ts []);
               in concat [
@@ -484,10 +482,9 @@
               ] end;
             fun print_eqns is_pseudo [((ts, t), (some_thm, _))] =
                   let
-                    val consts = fold Code_Thingol.add_constnames (t :: ts) [];
                     val vars = reserved
-                      |> intro_base_names
-                          (is_none o const_syntax) deresolve consts
+                      |> intro_base_names_for (is_none o const_syntax)
+                          deresolve (t :: ts)
                       |> intro_vars ((fold o Code_Thingol.fold_varnames)
                           (insert (op =)) ts []);
                   in
@@ -510,10 +507,9 @@
                   )
               | print_eqns _ (eqs as eq :: eqs') =
                   let
-                    val consts = fold Code_Thingol.add_constnames (map (snd o fst) eqs) [];
                     val vars = reserved
-                      |> intro_base_names
-                          (is_none o const_syntax) deresolve consts;
+                      |> intro_base_names_for (is_none o const_syntax)
+                           deresolve (map (snd o fst) eqs)
                     val dummy_parms = (map str o aux_params vars o map (fst o fst)) eqs;
                   in
                     Pretty.block (
diff -r de95c97efab3 -r 2bb3cd36bcf7 src/Tools/Code/code_printer.ML
--- a/src/Tools/Code/code_printer.ML	Sat Jan 25 22:18:20 2014 +0100
+++ b/src/Tools/Code/code_printer.ML	Sat Jan 25 23:50:49 2014 +0100
@@ -36,6 +36,8 @@
   val lookup_var: var_ctxt -> string -> string
   val intro_base_names: (string -> bool) -> (string -> string)
     -> string list -> var_ctxt -> var_ctxt
+  val intro_base_names_for: (string -> bool) -> (string -> string)
+    -> iterm list -> var_ctxt -> var_ctxt
   val aux_params: var_ctxt -> iterm list list -> string list
 
   type literals
@@ -187,12 +189,17 @@
     val vars' = intro_vars fished3 vars;
   in map (lookup_var vars') fished3 end;
 
-fun intro_base_names no_syntax deresolve names = names
-  |> map_filter (fn name => if no_syntax name then
+fun intro_base_names no_syntax deresolve =
+  map_filter (fn name => if no_syntax name then
       let val name' = deresolve name in
         if Long_Name.is_qualified name' then NONE else SOME name'
       end else NONE)
-  |> intro_vars;
+  #> intro_vars;
+
+fun intro_base_names_for no_syntax deresolve ts =
+  []
+  |> fold Code_Thingol.add_constnames ts 
+  |> intro_base_names no_syntax deresolve;
 
 
 (** pretty literals **)
diff -r de95c97efab3 -r 2bb3cd36bcf7 src/Tools/Code/code_scala.ML
--- a/src/Tools/Code/code_scala.ML	Sat Jan 25 22:18:20 2014 +0100
+++ b/src/Tools/Code/code_scala.ML	Sat Jan 25 23:50:49 2014 +0100
@@ -167,11 +167,9 @@
             val simple = case eqs
              of [((ts, _), _)] => forall Code_Thingol.is_IVar ts
               | _ => false;
-            val consts = fold Code_Thingol.add_constnames
-              (map (snd o fst) eqs) [];
             val vars1 = reserved
-              |> intro_base_names
-                   (is_none o const_syntax) deresolve consts
+              |> intro_base_names_for (is_none o const_syntax)
+                   deresolve (map (snd o fst) eqs);
             val params = if simple
               then (map (fn IVar (SOME x) => x) o fst o fst o hd) eqs
               else aux_params vars1 (map (fst o fst) eqs);