# HG changeset patch
# User haftmann
# Date 1283427818 -7200
# Node ID 81e0368812adb57492b028038be250188c80bfba
# Parent  ebeb48fd653b54e2a751359972fe3935eb6265f1
removed namespace stuff from code_printer

diff -r ebeb48fd653b -r 81e0368812ad src/Tools/Code/code_haskell.ML
--- a/src/Tools/Code/code_haskell.ML	Thu Sep 02 12:30:22 2010 +0200
+++ b/src/Tools/Code/code_haskell.ML	Thu Sep 02 13:43:38 2010 +0200
@@ -261,13 +261,31 @@
           end;
   in print_stmt end;
 
+fun mk_name_module reserved module_prefix module_alias program =
+  let
+    fun mk_alias name = case module_alias name
+     of SOME name' => name'
+      | NONE => name
+          |> Long_Name.explode
+          |> map (fn name => (the_single o fst) (Name.variants [name] reserved))
+          |> Long_Name.implode;
+    fun mk_prefix name = case module_prefix
+     of SOME module_prefix => Long_Name.append module_prefix name
+      | NONE => name;
+    val tab =
+      Symtab.empty
+      |> Graph.fold ((fn name => Symtab.default (name, (mk_alias #> mk_prefix) name))
+           o fst o Code_Namespace.dest_name o fst)
+             program
+  in the o Symtab.lookup tab end;
+
 fun haskell_program_of_program labelled_name module_prefix reserved module_alias program =
   let
     val reserved = Name.make_context reserved;
     val mk_name_module = mk_name_module reserved module_prefix module_alias program;
     fun add_stmt (name, (stmt, deps)) =
       let
-        val (module_name, base) = dest_name name;
+        val (module_name, base) = Code_Namespace.dest_name name;
         val module_name' = mk_name_module module_name;
         val mk_name_stmt = yield_singleton Name.variants;
         fun add_fun upper (nsp_fun, nsp_typ) =
@@ -309,7 +327,7 @@
       (Graph.get_node program name, Graph.imm_succs program name))
       (Graph.strong_conn program |> flat)) Symtab.empty;
     fun deresolver name = (fst o the o AList.lookup (op =) ((fst o snd o the
-      o Symtab.lookup hs_program) ((mk_name_module o fst o dest_name) name))) name
+      o Symtab.lookup hs_program) ((mk_name_module o fst o Code_Namespace.dest_name) name))) name
       handle Option => error ("Unknown statement name: " ^ labelled_name name);
   in (deresolver, hs_program) end;
 
diff -r ebeb48fd653b -r 81e0368812ad src/Tools/Code/code_namespace.ML
--- a/src/Tools/Code/code_namespace.ML	Thu Sep 02 12:30:22 2010 +0200
+++ b/src/Tools/Code/code_namespace.ML	Thu Sep 02 13:43:38 2010 +0200
@@ -6,6 +6,7 @@
 
 signature CODE_NAMESPACE =
 sig
+  val dest_name: string -> string * string
   datatype ('a, 'b) node =
       Dummy
     | Stmt of 'a
@@ -23,7 +24,13 @@
 structure Code_Namespace : CODE_NAMESPACE =
 struct
 
-(* hierarchical program structure *)
+(** splitting names in module and base part **)
+
+val dest_name =
+  apfst Long_Name.implode o split_last o fst o split_last o Long_Name.explode;
+
+
+(** hierarchical program structure **)
 
 datatype ('a, 'b) node =
     Dummy
@@ -46,10 +53,10 @@
      of SOME name' => Long_Name.explode name'
       | NONE => map (fn name => fst (yield_singleton Name.variants name reserved))
           (Long_Name.explode name);
-    val module_names = Graph.fold (insert (op =) o fst o Code_Printer.dest_name o fst) program [];
+    val module_names = Graph.fold (insert (op =) o fst o dest_name o fst) program [];
     val fragments_tab = fold (fn name => Symtab.update
       (name, alias_fragments name)) module_names Symtab.empty;
-    val dest_name = Code_Printer.dest_name #>> (the o Symtab.lookup fragments_tab);
+    val dest_name = dest_name #>> (the o Symtab.lookup fragments_tab);
 
     (* building empty module hierarchy *)
     val empty_module = (empty_data, Graph.empty);
diff -r ebeb48fd653b -r 81e0368812ad src/Tools/Code/code_printer.ML
--- a/src/Tools/Code/code_printer.ML	Thu Sep 02 12:30:22 2010 +0200
+++ b/src/Tools/Code/code_printer.ML	Thu Sep 02 13:43:38 2010 +0200
@@ -70,7 +70,6 @@
   val applify: string -> string -> ('a -> Pretty.T) -> fixity -> Pretty.T -> 'a list -> Pretty.T
   val tuplify: (fixity -> 'a -> Pretty.T) -> fixity -> 'a list -> Pretty.T option
 
-
   type tyco_syntax
   type simple_const_syntax
   type complex_const_syntax
@@ -93,10 +92,6 @@
   val gen_print_bind: (thm option -> var_ctxt -> fixity -> iterm -> Pretty.T)
     -> thm option -> fixity
     -> iterm -> var_ctxt -> Pretty.T * var_ctxt
-
-  val mk_name_module: Name.context -> string option -> (string -> string option)
-    -> 'a Graph.T -> string -> string
-  val dest_name: string -> string * string
 end;
 
 structure Code_Printer : CODE_PRINTER =
@@ -395,28 +390,4 @@
 
 val parse_const_syntax = parse_syntax plain_const_syntax simple_const_syntax fst;
 
-
-(** module name spaces **)
-
-val dest_name =
-  apfst Long_Name.implode o split_last o fst o split_last o Long_Name.explode;
-
-fun mk_name_module reserved module_prefix module_alias program =
-  let
-    fun mk_alias name = case module_alias name
-     of SOME name' => name'
-      | NONE => name
-          |> Long_Name.explode
-          |> map (fn name => (the_single o fst) (Name.variants [name] reserved))
-          |> Long_Name.implode;
-    fun mk_prefix name = case module_prefix
-     of SOME module_prefix => Long_Name.append module_prefix name
-      | NONE => name;
-    val tab =
-      Symtab.empty
-      |> Graph.fold ((fn name => Symtab.default (name, (mk_alias #> mk_prefix) name))
-           o fst o dest_name o fst)
-             program
-  in the o Symtab.lookup tab end;
-
 end; (*struct*)