# HG changeset patch
# User haftmann
# Date 1160751169 -7200
# Node ID 3b0c2641f740c5cccd324d16b1668e4b2ebff8d3
# Parent  b9321724c2ccbe2551debb675ad51bffa86d66a6
refined

diff -r b9321724c2cc -r 3b0c2641f740 src/Pure/Tools/codegen_names.ML
--- a/src/Pure/Tools/codegen_names.ML	Fri Oct 13 16:52:48 2006 +0200
+++ b/src/Pure/Tools/codegen_names.ML	Fri Oct 13 16:52:49 2006 +0200
@@ -23,6 +23,7 @@
   val const_rev: theory -> const -> CodegenConsts.const option
   val const_force: CodegenConsts.const * const -> theory -> theory
   val purify_var: string -> string
+  val check_modulename: string -> string
   val has_nsp: string -> string -> bool
   val nsp_module: string
   val nsp_class: string
@@ -221,9 +222,24 @@
            (Scan.repeat (Scan.some rep_op || Scan.one Symbol.not_eof));
       in (explode #> scan_valids #> implode) s end;
 
-val purify_lower = explode #> nth_map 0 Symbol.to_ascii_lower #> implode;
+val purify_lower =
+  explode
+  #> (fn cs => (if forall Symbol.is_ascii_upper cs
+        then map else nth_map 0) Symbol.to_ascii_lower cs)
+  #> implode;
+
 val purify_upper = explode #> nth_map 0 Symbol.to_ascii_upper #> implode;
 
+fun check_modulename mn =
+  let
+    val mns = NameSpace.unpack mn;
+    val mns' = map purify_upper mns;
+  in
+    if mns' = mns then mn else error ("Invalid module name: " ^ quote mn ^ "n"
+      ^ "perhaps try " ^ NameSpace.pack mns')
+  end
+
+
 fun purify_var "" = "x"
   | purify_var v =
       if nth (explode v) 0 = "'"