Symbol.name_of and Name.desymbolize

--- a/src/Pure/General/symbol.ML	Tue Apr 28 13:34:48 2009 +0200
+++ b/src/Pure/General/symbol.ML	Tue Apr 28 18:42:26 2009 +0200
@@ -18,6 +18,7 @@
   val is_symbolic: symbol -> bool
   val is_printable: symbol -> bool
   val is_utf8_trailer: symbol -> bool
+  val name_of: symbol -> string
   val eof: symbol
   val is_eof: symbol -> bool
   val not_eof: symbol -> bool
@@ -135,6 +136,10 @@
 fun is_regular s =
   not_eof s andalso s <> sync andalso s <> malformed andalso s <> end_malformed;
 
+fun name_of s = if is_symbolic s
+  then (unsuffix ">" o unprefix "\\<") s
+  else error (malformed_msg s);
+
 
 (* ascii symbols *)
 

--- a/src/Pure/name.ML	Tue Apr 28 13:34:48 2009 +0200
+++ b/src/Pure/name.ML	Tue Apr 28 18:42:26 2009 +0200
@@ -28,6 +28,7 @@
   val variants: string list -> context -> string list * context
   val variant_list: string list -> string list -> string list
   val variant: string list -> string -> string
+  val desymbolize: string -> string
 end;
 
 structure Name: NAME =
@@ -144,4 +145,26 @@
 fun variant_list used names = #1 (make_context used |> variants names);
 fun variant used = singleton (variant_list used);
 
+
+(* names conforming to typical requirements of identifiers in the outside world *)
+
+fun desymbolize "" = "x"
+  | desymbolize s =
+      let
+        val xs = Symbol.explode s;
+        val ys = if Symbol.is_ascii_letter (hd xs) then xs
+          else "x" :: xs;
+        fun is_valid x =
+          Symbol.is_ascii_letter x orelse Symbol.is_ascii_digit x orelse x = "'";
+        fun sep [] = []
+          | sep (xs as "_" :: _) = xs
+          | sep xs = "_" :: xs;
+        fun desymb x xs = if is_valid x
+            then x :: xs
+          else if Symbol.is_symbolic x
+            then "_" :: Symbol.name_of x :: sep xs 
+          else
+            sep xs
+      in implode (fold_rev desymb ys []) end;
+
 end;

--- a/src/Tools/code/code_name.ML	Tue Apr 28 13:34:48 2009 +0200
+++ b/src/Tools/code/code_name.ML	Tue Apr 28 18:42:26 2009 +0200
@@ -6,10 +6,10 @@
 
 signature CODE_NAME =
 sig
+  val purify_name: bool -> string -> string
   val purify_var: string -> string
   val purify_tvar: string -> string
   val purify_base: string -> string
-  val check_modulename: string -> string
 
   val read_const_exprs: theory -> string list -> string list * string list
 end;
@@ -19,63 +19,33 @@
 
 (** purification **)
 
-fun purify_name upper =
+fun purify_name upper = 
   let
-    fun is_valid s = Symbol.is_ascii_letter s orelse Symbol.is_ascii_digit s orelse s = "'";
-    val is_junk = not o is_valid andf Symbol.is_regular;
-    val junk = Scan.many is_junk;
-    val scan_valids = Symbol.scanner "Malformed input"
-      ((junk |--
-        (Scan.optional (Scan.one Symbol.is_ascii_letter) "x" ^^ (Scan.many is_valid >> implode)
-        --| junk))
-      ::: Scan.repeat ((Scan.many1 is_valid >> implode) --| junk));
     fun upper_lower cs = if upper then nth_map 0 Symbol.to_ascii_upper cs
       else (if forall Symbol.is_ascii_upper cs
         then map else nth_map 0) Symbol.to_ascii_lower cs;
   in
-    explode
-    #> scan_valids
-    #> space_implode "_"
+    Name.desymbolize
     #> explode
     #> upper_lower
     #> implode
   end;
 
-fun purify_var "" = "x"
-  | purify_var v = purify_name false v;
+val purify_var = purify_name false;
 
 fun purify_tvar "" = "'a"
   | purify_tvar v =
-      (unprefix "'" #> explode #> filter Symbol.is_ascii_letter #> cons "'" #> implode) v;
-
-val purify_prefix =
-  explode
-  (*FIMXE should disappear as soon as hierarchical theory name spaces are available*)
-  #> Symbol.scanner "Malformed name"
-      (Scan.repeat ($$ "_" |-- $$ "_" >> (fn _ => ".") || Scan.one Symbol.is_regular))
-  #> implode
-  #> Long_Name.explode
-  #> map (purify_name true);
+      (unprefix "'" #> purify_name false #> prefix "'") v;
 
 (*FIMXE non-canonical function treating non-canonical names*)
 fun purify_base "op &" = "and"
   | purify_base "op |" = "or"
   | purify_base "op -->" = "implies"
   | purify_base "op :" = "member"
+  | purify_base "op =" = "eq"
   | purify_base "*" = "product"
   | purify_base "+" = "sum"
-  | purify_base s = if String.isPrefix "op =" s
-      then "eq" ^ purify_name false s
-      else purify_name false s;
-
-fun check_modulename mn =
-  let
-    val mns = Long_Name.explode mn;
-    val mns' = map (purify_name true) mns;
-  in
-    if mns' = mns then mn else error ("Invalid module name: " ^ quote mn ^ "\n"
-      ^ "perhaps try " ^ quote (Long_Name.implode mns'))
-  end;
+  | purify_base s = purify_name false s;
 
 
 (** misc **)

--- a/src/Tools/code/code_target.ML	Tue Apr 28 13:34:48 2009 +0200
+++ b/src/Tools/code/code_target.ML	Tue Apr 28 18:42:26 2009 +0200
@@ -323,8 +323,15 @@
 val add_include = gen_add_include Code_Unit.check_const;
 val add_include_cmd = gen_add_include Code_Unit.read_const;
 
-fun add_module_alias target =
-  map_module_alias target o Symtab.update o apsnd Code_Name.check_modulename;
+fun add_module_alias target (thyname, modlname) =
+  let
+    val xs = Long_Name.explode modlname;
+    val xs' = map (Code_Name.purify_name true) xs;
+  in if xs' = xs
+    then map_module_alias target (Symtab.update (thyname, modlname))
+    else error ("Invalid module name: " ^ quote modlname ^ "\n"
+      ^ "perhaps try " ^ quote (Long_Name.implode xs'))
+  end;
 
 fun gen_allow_abort prep_const raw_c thy =
   let