diff -r 657386d94f14 -r 0ce5f53fc65d src/Tools/code/code_name.ML
--- a/src/Tools/code/code_name.ML	Mon May 11 09:39:53 2009 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,104 +0,0 @@
-(*  Title:      Tools/code/code_name.ML
-    Author:     Florian Haftmann, TU Muenchen
-
-Some code generator infrastructure concerning names.
-*)
-
-signature CODE_NAME =
-sig
-  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;
-
-structure Code_Name: CODE_NAME =
-struct
-
-(** purification **)
-
-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 "_"
-    #> explode
-    #> upper_lower
-    #> implode
-  end;
-
-fun purify_var "" = "x"
-  | purify_var v = purify_name false v;
-
-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);
-
-(*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 "*" = "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;
-
-
-(** misc **)
-
-fun read_const_exprs thy =
-  let
-    fun consts_of some_thyname =
-      let
-        val thy' = case some_thyname
-         of SOME thyname => ThyInfo.the_theory thyname thy
-          | NONE => thy;
-        val cs = Symtab.fold (fn (c, (_, NONE)) => cons c | _ => I)
-          ((snd o #constants o Consts.dest o #consts o Sign.rep_sg) thy') [];
-        fun belongs_here c =
-          not (exists (fn thy'' => Sign.declared_const thy'' c) (Theory.parents_of thy'))
-      in case some_thyname
-       of NONE => cs
-        | SOME thyname => filter belongs_here cs
-      end;
-    fun read_const_expr "*" = ([], consts_of NONE)
-      | read_const_expr s = if String.isSuffix ".*" s
-          then ([], consts_of (SOME (unsuffix ".*" s)))
-          else ([Code_Unit.read_const thy s], []);
-  in pairself flat o split_list o map read_const_expr end;
-
-end;