accomplish potentially case-insenstive file systems for Scala

--- a/src/HOL/Codegenerator_Test/Code_Test_Scala.thy	Thu Oct 02 22:33:45 2014 +0200
+++ b/src/HOL/Codegenerator_Test/Code_Test_Scala.thy	Thu Oct 02 17:51:04 2014 +0200
@@ -6,6 +6,8 @@
 
 theory Code_Test_Scala imports Code_Test begin 
 
+declare [[scala_case_insensitive]]
+
 test_code "14 + 7 * -12 = (140 div -2 :: integer)" in Scala
 
 value [Scala] "14 + 7 * -12 :: integer"

--- a/src/Tools/Code/code_namespace.ML	Thu Oct 02 22:33:45 2014 +0200
+++ b/src/Tools/Code/code_namespace.ML	Thu Oct 02 17:51:04 2014 +0200
@@ -6,6 +6,8 @@
 
 signature CODE_NAMESPACE =
 sig
+  val variant_case_insensitive: string -> Name.context -> string * Name.context
+
   datatype export = Private | Opaque | Public
   val is_public: export -> bool
   val not_private: export -> bool
@@ -47,6 +49,25 @@
 structure Code_Namespace : CODE_NAMESPACE =
 struct
 
+(** name handling on case-insensitive file systems **)
+
+fun restore_for cs =
+  if forall Symbol.is_ascii_upper cs then map Symbol.to_ascii_upper
+  else if Symbol.is_ascii_upper (nth cs 0) then nth_map 0 Symbol.to_ascii_upper
+  else I;
+
+fun variant_case_insensitive s ctxt =
+  let
+    val cs = Symbol.explode s;
+    val s_lower = implode (map Symbol.to_ascii_lower cs);
+    val restore = implode o restore_for cs o Symbol.explode;
+  in
+    ctxt
+    |> Name.variant s_lower
+    |>> restore
+  end;
+
+
 (** export **)
 
 datatype export = Private | Opaque | Public;

--- a/src/Tools/Code/code_scala.ML	Thu Oct 02 22:33:45 2014 +0200
+++ b/src/Tools/Code/code_scala.ML	Thu Oct 02 17:51:04 2014 +0200
@@ -7,6 +7,7 @@
 signature CODE_SCALA =
 sig
   val target: string
+  val case_insensitive: bool Config.T;
   val setup: theory -> theory
 end;
 
@@ -22,6 +23,10 @@
 infixr 5 @@;
 infixr 5 @|;
 
+(** preliminary: option to circumvent clashes on case-insensitive file systems **)
+
+val case_insensitive = Attrib.setup_config_bool @{binding "scala_case_insensitive"} (K false);
+
 
 (** Scala serializer **)
 
@@ -293,21 +298,24 @@
 
 fun scala_program_of_program ctxt module_name reserved identifiers exports program =
   let
+    val variant = if Config.get ctxt case_insensitive
+      then Code_Namespace.variant_case_insensitive
+      else Name.variant;
     fun namify_module name_fragment ((nsp_class, nsp_object), nsp_common) =
       let
         val declare = Name.declare name_fragment;
       in (name_fragment, ((declare nsp_class, declare nsp_object), declare nsp_common)) end;
     fun namify_class base ((nsp_class, nsp_object), nsp_common) =
       let
-        val (base', nsp_class') = Name.variant base nsp_class
+        val (base', nsp_class') = variant base nsp_class
       in (base', ((nsp_class', nsp_object), Name.declare base' nsp_common)) end;
     fun namify_object base ((nsp_class, nsp_object), nsp_common) =
       let
-        val (base', nsp_object') = Name.variant base nsp_object
+        val (base', nsp_object') = variant base nsp_object
       in (base', ((nsp_class, nsp_object'), Name.declare base' nsp_common)) end;
     fun namify_common base ((nsp_class, nsp_object), nsp_common) =
       let
-        val (base', nsp_common') = Name.variant base nsp_common
+        val (base', nsp_common') = variant base nsp_common
       in
         (base', ((Name.declare base' nsp_class, Name.declare base' nsp_object), nsp_common'))
       end;