1.1 --- a/src/Tools/Code/code_target.ML	Tue Aug 31 16:51:29 2010 +0200
     1.2 +++ b/src/Tools/Code/code_target.ML	Tue Aug 31 16:51:29 2010 +0200
     1.3 @@ -9,21 +9,21 @@
     1.4    val cert_tyco: theory -> string -> string
     1.5    val read_tyco: theory -> string -> string
     1.6  
     1.7 -  val export_code_for: theory -> Path.T option -> string -> int option -> string option -> Token.T list
     1.8 +  val export_code_for: theory -> Path.T option -> string -> int option -> string -> Token.T list
     1.9      -> Code_Thingol.naming -> Code_Thingol.program -> string list -> unit
    1.10 -  val produce_code_for: theory -> string -> int option -> string option -> Token.T list
    1.11 +  val produce_code_for: theory -> string -> int option -> string -> Token.T list
    1.12      -> Code_Thingol.naming -> Code_Thingol.program -> string list -> string * string option list
    1.13 -  val present_code_for: theory -> string -> int option -> string option -> Token.T list
    1.14 +  val present_code_for: theory -> string -> int option -> string -> Token.T list
    1.15      -> Code_Thingol.naming -> Code_Thingol.program -> string list * string list -> string
    1.16    val check_code_for: theory -> string -> bool -> Token.T list
    1.17      -> Code_Thingol.naming -> Code_Thingol.program -> string list -> unit
    1.18  
    1.19    val export_code: theory -> string list
    1.20 -    -> (((string * string option) * Path.T option) * Token.T list) list -> unit
    1.21 +    -> (((string * string) * Path.T option) * Token.T list) list -> unit
    1.22    val produce_code: theory -> string list
    1.23 -    -> string -> int option -> string option -> Token.T list -> string * string option list
    1.24 +    -> string -> int option -> string -> Token.T list -> string * string option list
    1.25    val present_code: theory -> string list -> (Code_Thingol.naming -> string list)
    1.26 -    -> string -> int option -> string option -> Token.T list -> string
    1.27 +    -> string -> int option -> string -> Token.T list -> string
    1.28    val check_code: theory -> string list
    1.29      -> ((string * bool) * Token.T list) list -> unit
    1.30  
    1.31 @@ -319,7 +319,7 @@
    1.32        labelled_name = Code_Thingol.labelled_name thy proto_program,
    1.33        reserved_syms = reserved,
    1.34        includes = includes,
    1.35 -      module_alias = if is_some module_name then K module_name else Symtab.lookup module_alias,
    1.36 +      module_alias = if module_name = "" then Symtab.lookup module_alias else K (SOME module_name),
    1.37        class_syntax = Symtab.lookup class_syntax,
    1.38        tyco_syntax = Symtab.lookup tyco_syntax,
    1.39        const_syntax = Symtab.lookup const_syntax,
    1.40 @@ -336,7 +336,7 @@
    1.41       of Fundamental seri => #serializer seri;
    1.42      val presentation_names = stmt_names_of_destination destination;
    1.43      val module_name = if null presentation_names
    1.44 -      then raw_module_name else SOME "Code";
    1.45 +      then raw_module_name else "Code";
    1.46      val reserved = the_reserved data;
    1.47      fun select_include names_all (name, (content, cs)) =
    1.48        if null cs then SOME (name, content)
    1.49 @@ -356,20 +356,23 @@
    1.50          naming program (names, presentation_names) width destination
    1.51    end;
    1.52  
    1.53 +fun assert_module_name "" = error ("Empty module name not allowed.")
    1.54 +  | assert_module_name module_name = module_name;
    1.55 +
    1.56  in
    1.57  
    1.58  fun export_code_for thy some_path target some_width some_module_name args naming program names =
    1.59    export some_path (mount_serializer thy target some_width some_module_name args naming program names);
    1.60  
    1.61 -fun produce_code_for thy target some_width some_module_name args naming program names =
    1.62 -  produce (mount_serializer thy target some_width some_module_name args naming program names);
    1.63 +fun produce_code_for thy target some_width module_name args naming program names =
    1.64 +  produce (mount_serializer thy target some_width (assert_module_name module_name) args naming program names);
    1.65  
    1.66 -fun present_code_for thy target some_width some_module_name args naming program (names, selects) =
    1.67 -  present selects (mount_serializer thy target some_width some_module_name args naming program names);
    1.68 +fun present_code_for thy target some_width module_name args naming program (names, selects) =
    1.69 +  present selects (mount_serializer thy target some_width (assert_module_name module_name) args naming program names);
    1.70  
    1.71  fun check_code_for thy target strict args naming program names_cs =
    1.72    let
    1.73 -    val module_name = "Code_Test";
    1.74 +    val module_name = "Code";
    1.75      val { env_var, make_destination, make_command } =
    1.76        (#check o the_fundamental thy) target;
    1.77      val env_param = getenv env_var;
    1.78 @@ -377,7 +380,7 @@
    1.79        let 
    1.80          val destination = make_destination p;
    1.81          val _ = export (SOME destination) (mount_serializer thy target (SOME 80)
    1.82 -          (SOME module_name) args naming program names_cs);
    1.83 +          module_name args naming program names_cs);
    1.84          val cmd = make_command env_param module_name;
    1.85        in if bash ("cd " ^ File.shell_path p ^ " && " ^ cmd ^ " 2>&1") <> 0
    1.86          then error ("Code check failed for " ^ target ^ ": " ^ cmd)
    1.87 @@ -518,15 +521,17 @@
    1.88  val add_include = gen_add_include (K I);
    1.89  val add_include_cmd = gen_add_include Code.read_const;
    1.90  
    1.91 -fun add_module_alias target (thyname, modlname) =
    1.92 -  let
    1.93 -    val xs = Long_Name.explode modlname;
    1.94 -    val xs' = map (Name.desymbolize true) xs;
    1.95 -  in if xs' = xs
    1.96 -    then map_module_alias target (Symtab.update (thyname, modlname))
    1.97 -    else error ("Invalid module name: " ^ quote modlname ^ "\n"
    1.98 -      ^ "perhaps try " ^ quote (Long_Name.implode xs'))
    1.99 -  end;
   1.100 +fun add_module_alias target (thyname, "") =
   1.101 +      map_module_alias target (Symtab.delete thyname)
   1.102 +  | add_module_alias target (thyname, modlname) =
   1.103 +      let
   1.104 +        val xs = Long_Name.explode modlname;
   1.105 +        val xs' = map (Name.desymbolize true) xs;
   1.106 +      in if xs' = xs
   1.107 +        then map_module_alias target (Symtab.update (thyname, modlname))
   1.108 +        else error ("Invalid module name: " ^ quote modlname ^ "\n"
   1.109 +          ^ "perhaps try " ^ quote (Long_Name.implode xs'))
   1.110 +      end;
   1.111  
   1.112  fun gen_allow_abort prep_const raw_c thy =
   1.113    let
   1.114 @@ -585,7 +590,7 @@
   1.115        -- ((Parse.$$$ "?" |-- Scan.succeed false) || Scan.succeed true) -- code_expr_argsP))
   1.116        >> (fn seris => check_code_cmd raw_cs seris)
   1.117      || Scan.repeat (Parse.$$$ inK |-- Parse.name
   1.118 -       -- Scan.option (Parse.$$$ module_nameK |-- Parse.name)
   1.119 +       -- Scan.optional (Parse.$$$ module_nameK |-- Parse.name) ""
   1.120         -- Scan.optional (Parse.$$$ fileK |-- Parse.name) ""
   1.121         -- code_expr_argsP) >> (fn seris => export_code_cmd raw_cs seris)));
   1.122